How to use my own proposition

Stream: new members

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Data.Real.Basic
import Mathlib.SetTheory.Cardinal.Basic
import Mathlib.SetTheory.Cardinal.Finite
import Mathlib.Data.Complex.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Algebra.Hom.Group
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Init.Function
import Mathlib.GroupTheory.OrderOfElement

/-- have h1 : ∃ n : Nat , ‖(x : ℂ) ^ n‖ = 1 := by
    by_contra h'
    simp at h'
    apply?
  have h2 :∃ n : Nat , ‖(x : ℂ)‖^n = 1 := by
    sorry
  have h3 :‖(x : ℂ)‖ = 1 := by
    sorry
  exact h3
  -/
example (G : Type _ ) [Group G] (finite_g : Finite G) (f: (G →* (Units ℂ))) (x: G) :
  ‖((f x) : ℂ)‖ = 1 := by

  have h0 (u:ℂ) : (Complex.normSq u) = (‖u‖ ^ 2) := by
    simp
    exact Complex.normSq_eq_abs u

  have h1 (v:ℝ) (n:ℕ) (j0 : v ≥ 0) (j1: n>0) (j2:v^n = 1) : v=1 := by
    by_contra h
    rcases lt_or_gt_of_ne h with hlt | hgt
    have h_pow_lt_one : v ^ n < 1 := by
      rw [←one_pow n]
      exact pow_lt_pow_of_lt_left hlt j0 j1
    have h_neq_one : v ^ n ≠ 1 := by
      exact LT.lt.ne h_pow_lt_one
    exact h_neq_one j2
    have one_lt_v: 1 < v := by
      exact hgt

    have h_pow_gt_one : 1 < v ^ n := by
      rw [←one_pow n]
      apply pow_lt_pow_of_lt_left one_lt_v
      exact zero_le_one
      exact j1

    rw [j2] at h_pow_gt_one
    apply ne_of_lt h_pow_gt_one
    rfl

  have h2 (u:ℂ) : ((Complex.normSq u = 1) → (‖u‖ = 1)) := by
    rw [h0]
    intro u2_1
    apply h1 ‖u‖ 2
    exact norm_nonneg u
    exact Nat.succ_pos 1
    apply u2_1
  apply h2

  have h3 (u:G) (v:G) : f (u*v) = f (u) * f (v) := by
    exact MonoidHom.map_mul f u v

  have h4 (u:ℂ) (v:ℂ) : Complex.normSq (u*v) = Complex.normSq (u) * Complex.normSq (v) := by
    exact Complex.normSq_mul u v

  have h5 (u:G) (v:G) : Complex.normSq (f (u*v): ℂ) = Complex.normSq (f (u): ℂ) * Complex.normSq (f (v): ℂ) := by
    rw [h3]
    simp

  have h6: Complex.normSq ((f (1:G)): ℂ) = 1 := by
    simp

  have h8: IsOfFinOrder x := by
    exact exists_pow_eq_one x

  have h9: ∃ (n: ℕ), ((n>0) ∧  x^n = 1) := by
    exact Iff.mp (isOfFinOrder_iff_pow_eq_one x) h8

  have h10 (n: ℕ): (Complex.normSq ((f x^n):ℂ)) = (Complex.normSq ((f x):ℂ)) ^ n := by
    induction n
    simp
    simp
  apply h9 at h10
  apply h6 at h10
  apply h1 at h10
  exact h10

The last four commands I wrote are wrong, does anyone know how to correctly use those propositions I wrote earlier?

[Niels Voss]

apply is used only in the highly specific case where the goal is of the form B and h has type A → B (or something similar to it). So apply h2 works because it is an implication, but the rest of the applys would not work.

To use a hypothesis of the form h : a = b you should do rw [h] or rw [←h] or rw [h] at something (I think this would apply to h1 and h6 in your example.)

Using h9 is a bit more difficult but you could first do rcases h9 with ⟨k, hk⟩ to go from ∃ (n : ℕ), ((n>0) ∧ x^n = 1) to an actual number k : ℕ and a proof that k > 0 ∧ x ^ k = 1 (This might not be the most idiomatic way to do it in Lean 4). Then you can do specialize h10 k to go from ∀ (n : ℕ), ↑Complex.normSq ↑(↑f x ^ n) = ↑Complex.normSq ↑(↑f x) ^ n to ↑Complex.normSq ↑(↑f x ^ k) = ↑Complex.normSq ↑(↑f x) ^ k

[tsuki hao]

Niels Voss said:

apply is used only in the highly specific case where the goal is of the form B and h has type A → B (or something similar to it). So apply h2 works because it is an implication, but the rest of the applys would not work.

To use a hypothesis of the form h : a = b you should do rw [h] or rw [←h] or rw [h] at something (I think this would apply to h1 and h6 in your example.)

Using h9 is a bit more difficult but you could first do rcases h9 with ⟨k, hk⟩ to go from ∃ (n : ℕ), ((n>0) ∧ x^n = 1) to an actual number k : ℕ and a proof that k > 0 ∧ x ^ k = 1 (This might not be the most idiomatic way to do it in Lean 4). Then you can do specialize h10 k to go from ∀ (n : ℕ), ↑Complex.normSq ↑(↑f x ^ n) = ↑Complex.normSq ↑(↑f x) ^ n to ↑Complex.normSq ↑(↑f x ^ k) = ↑Complex.normSq ↑(↑f x) ^ k

I changed the last four sentences of code to this according to your prompt, but I encountered a difficulty that I couldn’t execute rw. I would like to ask if my rw syntax is wrong or should I use other strategies here?

rcases h9 with ⟨ n, ⟨ npos, xpoweq⟩ ⟩
  specialize h10 n
  rw[xpoweq] at h10

[Mario Carneiro]

are your tactics aligned? That will be misinterpreted otherwise

[Niels Voss]

rcases doesn't create new goals in this case (because Exists has only one constructor) so specialize and rw should be indented to the same level as rcases

[tsuki hao]

Niels Voss said:

rcases doesn't create new goals in this case (because Exists has only one constructor) so specialize and rw should be indented to the same level as rcases

They have been indented to the same level but still error

[Niels Voss]

I don't think h10 contains x ^ n anywhere, which would explain why your rewrite is failing. I see that h10 is ↑Complex.normSq ↑(↑f x ^ n) = ↑Complex.normSq ↑(↑f x) ^ n. If you wanted to rewrite at ↑f x ^ n, it won't work because it is interpreted as (↑f x) ^ n (I've made this mistake many times).

[tsuki hao]

Niels Voss said:

I don't think h10 contains x ^ n anywhere, which would explain why your rewrite is failing. I see that h10 is ↑Complex.normSq ↑(↑f x ^ n) = ↑Complex.normSq ↑(↑f x) ^ n. If you wanted to rewrite at ↑f x ^ n, it won't work because it is interpreted as (↑f x) ^ n (I've made this mistake many times).

Thank you, I'm shocked that this is the reason, if so my proof may need to be greatly revised :smiling_face_with_tear:

[Niels Voss]

Adding parenthesis to the line where h10 is declared (changing ((f x^n):ℂ) to ((f (x^n)):ℂ)) seems to make the rw work.

[tsuki hao]

Niels Voss said:

Adding parenthesis to the line where h10 is declared (changing ((f x^n):ℂ) to ((f (x^n)):ℂ)) seems to make the rw work.

Thank you very much!