# Zulip Chat Archive

## 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 `apply`

s 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`apply`

s 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