internlm/Lean-Github huggingface dataset:
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Tactic:
have fc : f c ≠ 0 := Complex.slitPlane_ne_zero m
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Tactic:
have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝 c] fun z ↦ Complex.exp (Complex.log (f z) * g z) := by
  refine (fa.continuousAt.eventually_ne fc).mp (Filter.eventually_of_forall ?_)
  intro z fz; simp only [fz, Complex.cpow_def, if_false]
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => f z ^ g z) c
Tactic:
rw [analyticAt_congr e]
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => ((f z).log * g z).exp) c
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
e : (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
⊢ AnalyticAt ℂ (fun z => ((f z).log * g z).exp) c
Tactic:
exact AnalyticAt.exp.comp ((fa.log m).mul ga)
Proof state after:
no goals
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ (𝓝 c).EventuallyEq (fun z => f z ^ g z) fun z => ((f z).log * g z).exp
Tactic:
refine (fa.continuousAt.eventually_ne fc).mp (Filter.eventually_of_forall ?_)
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ ∀ (x : E), f x ≠ 0 → (fun z => f z ^ g z) x = (fun z => ((f z).log * g z).exp) x
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
⊢ ∀ (x : E), f x ≠ 0 → (fun z => f z ^ g z) x = (fun z => ((f z).log * g z).exp) x
Tactic:
intro z fz
Proof state after:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
z : E
fz : f z ≠ 0
⊢ (fun z => f z ^ g z) z = (fun z => ((f z).log * g z).exp) z
Theorem: AnalyticAt.cpow
Proof state before:
E : Type
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
inst✝³ : CompleteSpace E
F : Type
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : E → ℂ
c : E
fa : AnalyticAt ℂ f c
ga : AnalyticAt ℂ g c
m : f c ∈ Complex.slitPlane
fc : f c ≠ 0
z : E
fz : f z ≠ 0
⊢ (fun z => f z ^ g z) z = (fun z => ((f z).log * g z).exp) z
Tactic:
simp only [fz, Complex.cpow_def, if_false]
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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⟩
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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⟩
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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]
Proof 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
Theorem: exist_root_of_unity
Proof 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]
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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]
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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]
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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]
Proof state after:
no goals
Theorem: exist_root_of_unity
Proof 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
Proof 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
Theorem: exist_root_of_unity
Proof 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]
Proof state after:
no goals
Theorem: SuperAt.not_local_inj
Proof 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
f : ℂ → ℂ
d : ℕ
s : SuperAt f d
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases s.superNear with ⟨t, s⟩
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have ba : AnalyticAt ℂ (bottcherNear f d) 0 := bottcherNear_analytic_z s _ s.t0
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
have nc : mfderiv I I (bottcherNear f d) 0 ≠ 0 := by
  rw [mfderiv_eq_fderiv, ← deriv_fderiv, (bottcherNear_monic s).deriv]
  exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases complex_inverse_fun' (ba.holomorphicAt I I) nc with ⟨i, ia, ib, bi⟩
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i (bottcherNear f d 0)
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 (bottcherNear f d 0), bottcherNear f d (i x) = x
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Theorem: SuperAt.not_local_inj
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i (bottcherNear f d 0)
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 (bottcherNear f d 0), bottcherNear f d (i x) = x
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z
Tactic:
rw [bottcherNear_zero] at bi ia
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : ℂ → ℂ
d : ℕ
s✝ : SuperAt f d
t : Set ℂ
s : SuperNear f d t
ba : AnalyticAt ℂ (bottcherNear f d) 0
nc : mfderiv I I (bottcherNear f d) 0 ≠ 0
i : ℂ → ℂ
ia : HolomorphicAt I I i 0
ib : ∀ᶠ (x : ℂ) in 𝓝 0, i (bottcherNear f d x) = x
bi : ∀ᶠ (x : ℂ) in 𝓝 0, bottcherNear f d (i x) = x
⊢ ∃ g, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, g z ≠ z ∧ f (g z) = f z