## Stream: new members

### Topic: How to use my own proposition

#### tsuki hao (Jul 24 2023 at 02:23):

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 (Jul 24 2023 at 03:01):

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 (Jul 24 2023 at 03:21):

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 (Jul 24 2023 at 03:24):

are your tactics aligned? That will be misinterpreted otherwise

#### Niels Voss (Jul 24 2023 at 03:30):

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 (Jul 24 2023 at 03:33):

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 (Jul 24 2023 at 03:35):

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 (Jul 24 2023 at 03:42):

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 (Jul 24 2023 at 03:59):

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 (Jul 24 2023 at 06:48):

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!

Last updated: Dec 20 2023 at 11:08 UTC