Theorem: exist_root_of_unity (Ray/Dynamics/Multiple.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
set n : ℕ+ := ⟨d, lt_of_lt_of_le (by norm_num) d2⟩
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
have two : Nontrivial (rootsOfUnity n ℂ) := by
  rw [← Fintype.one_lt_card_iff_nontrivial, Complex.card_rootsOfUnity]
  simp only [PNat.mk_coe, n]; exact lt_of_lt_of_le (by norm_num) d2
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
two : Nontrivial ↥(rootsOfUnity n ℂ)
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
two : Nontrivial ↥(rootsOfUnity n ℂ)
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
rcases two with ⟨⟨a, am⟩, ⟨b, bm⟩, ab⟩
State after:
case mk.intro.mk.intro.mk
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a : ℂˣ
am : a ∈ rootsOfUnity n ℂ
b : ℂˣ
bm : b ∈ rootsOfUnity n ℂ
ab : ⟨a, am⟩ ≠ ⟨b, bm⟩
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1

State before:
case mk.intro.mk.intro.mk
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a : ℂˣ
am : a ∈ rootsOfUnity n ℂ
b : ℂˣ
bm : b ∈ rootsOfUnity n ℂ
ab : ⟨a, am⟩ ≠ ⟨b, bm⟩
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
simp only [Ne, Subtype.mk_eq_mk, mem_rootsOfUnity, PNat.mk_coe] at am bm ab
State after:
case mk.intro.mk.intro.mk
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1

State before:
case mk.intro.mk.intro.mk
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
by_cases a1 : a = 1
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : a = 1
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ Nontrivial ↥(rootsOfUnity n ℂ)
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, Complex.card_rootsOfUnity]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ 1 < ↑n

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ 1 < ↑n
Tactic:
simp only [PNat.mk_coe, n]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ 1 < d

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ 1 < d
Tactic:
exact lt_of_lt_of_le (by norm_num) d2
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : a = 1
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
use b
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : a = 1
⊢ ↑b ≠ 1 ∧ ↑b ^ d = 1

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : a = 1
⊢ ↑b ≠ 1 ∧ ↑b ^ d = 1
Tactic:
rw [a1] at ab
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ≠ 1 ∧ ↑b ^ d = 1

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ≠ 1 ∧ ↑b ^ d = 1
Tactic:
constructor
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ≠ 1

case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ^ d = 1

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ≠ 1
Tactic:
simp only [ne_eq, Units.val_eq_one, Ne.symm ab, not_false_eq_true]
State after:
no goals

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ^ d = 1
Tactic:
simp only [PNat.mk_coe, n] at bm
State after:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ d = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ^ d = 1

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ d = 1
ab : ¬1 = b
a1 : a = 1
⊢ ↑b ^ d = 1
Tactic:
rw [← Units.val_pow_eq_pow_val, bm, Units.val_one]
State after:
no goals

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ∃ a, a ≠ 1 ∧ a ^ d = 1
Tactic:
use a
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ≠ 1 ∧ ↑a ^ d = 1

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ≠ 1 ∧ ↑a ^ d = 1
Tactic:
constructor
State after:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ≠ 1

case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ^ d = 1

State before:
case h.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ≠ 1
Tactic:
simp only [ne_eq, Units.val_eq_one, a1, not_false_eq_true]
State after:
no goals

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ ↑n = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ^ d = 1
Tactic:
simp only [PNat.mk_coe, n] at am
State after:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ d = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ^ d = 1

State before:
case h.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
d : ℕ
d2 : 2 ≤ d
n : ℕ+ := ⟨d, ⋯⟩
a b : ℂˣ
am : a ^ d = 1
bm : b ^ ↑n = 1
ab : ¬a = b
a1 : ¬a = 1
⊢ ↑a ^ d = 1
Tactic:
rw [← Units.val_pow_eq_pow_val, am, Units.val_one]
State after:
no goals