internlm/Lean-Github huggingface dataset:
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case h.ht
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
⊢ ∀ (i : ℕ), {x | i ≠ 0 ∧ x ^ i = 1}.Countable
Tactic:
intro n
Proof state after:
case h.ht
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case h.ht
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable
Tactic:
by_cases n0 : n = 0
Proof state after:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : n = 0
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable

case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : n = 0
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable

case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable
Tactic:
simp only [n0, Ne, eq_self_iff_true, not_true, false_and_iff, setOf_false, countable_empty]
Proof state after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
⊢ {x | n ≠ 0 ∧ x ^ n = 1}.Countable
Tactic:
simp only [Ne, n0, not_false_iff, true_and_iff]
Proof state after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
⊢ {x | x ^ n = 1}.Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
⊢ {x | x ^ n = 1}.Countable
Tactic:
have np : 0 < n := Nat.pos_of_ne_zero n0
Proof state after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
⊢ {x | x ^ n = 1}.Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
⊢ {x | x ^ n = 1}.Countable
Tactic:
generalize hn' : (⟨n, np⟩ : ℕ+) = n'
Proof state after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ {x | x ^ n = 1}.Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
e : {z | z ^ n = 1} ⊆ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
⊢ {x | x ^ n = 1}.Countable
Tactic:
apply Set.Countable.mono e
Proof state after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
e : {z | z ^ n = 1} ⊆ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
⊢ ((fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)).Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
e : {z | z ^ n = 1} ⊆ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
⊢ ((fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)).Countable
Tactic:
clear e
Proof state after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ ((fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)).Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ ((fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)).Countable
Tactic:
apply Countable.image
Proof state after:
case neg.hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ (↑(rootsOfUnity n' ℂ)).Countable
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg.hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ (↑(rootsOfUnity n' ℂ)).Countable
Tactic:
apply Set.Finite.countable
Proof state after:
case neg.hs.hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ (↑(rootsOfUnity n' ℂ)).Finite
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg.hs.hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ (↑(rootsOfUnity n' ℂ)).Finite
Tactic:
rw [Set.finite_def]
Proof state after:
case neg.hs.hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ Nonempty (Fintype ↑↑(rootsOfUnity n' ℂ))
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg.hs.hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ Nonempty (Fintype ↑↑(rootsOfUnity n' ℂ))
Tactic:
exact ⟨_root_.rootsOfUnity.fintype ℂ n'⟩
Proof state after:
no goals
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
⊢ {z | z ^ n = 1} ⊆ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
Tactic:
intro z e
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ∈ {z | z ^ n = 1}
⊢ z ∈ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ∈ {z | z ^ n = 1}
⊢ z ∈ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
Tactic:
simp only [mem_setOf] at e
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
⊢ z ∈ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
⊢ z ∈ (fun x => ↑x) '' ↑(rootsOfUnity n' ℂ)
Tactic:
simp only [mem_image, SetLike.mem_coe, mem_rootsOfUnity, PNat.mk_coe]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
⊢ ∃ x, x ^ ↑n' = 1 ∧ ↑x = z
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
⊢ ∃ x, x ^ ↑n' = 1 ∧ ↑x = z
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
z0 : z = 0
⊢ ∃ x, x ^ ↑n' = 1 ∧ ↑x = z

case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
z0 : ¬z = 0
⊢ ∃ x, x ^ ↑n' = 1 ∧ ↑x = z
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
z0 : z = 0
⊢ ∃ x, x ^ ↑n' = 1 ∧ ↑x = z
Tactic:
simp only [z0, zero_pow n0, zero_ne_one] at e
Proof state after:
no goals
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
z0 : ¬z = 0
⊢ ∃ x, x ^ ↑n' = 1 ∧ ↑x = z
Tactic:
use Units.mk0 z z0
Proof state after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
z0 : ¬z = 0
⊢ Units.mk0 z z0 ^ ↑n' = 1 ∧ ↑(Units.mk0 z z0) = z
Theorem: IsTotallyDisconnected.allRootsOfUnity
Proof state before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : ℕ
n0 : ¬n = 0
np : 0 < n
n' : { n // 0 < n }
hn' : ⟨n, np⟩ = n'
z : ℂ
e : z ^ n = 1
z0 : ¬z = 0
⊢ Units.mk0 z z0 ^ ↑n' = 1 ∧ ↑(Units.mk0 z z0) = z
Tactic:
simp only [← hn', PNat.mk_coe, ← Units.eq_iff, Units.val_pow_eq_pow_val, Units.val_mk0, e,
  Units.val_one, and_self]
Proof state after:
no goals
Theorem: NontrivialAnalyticOn.const
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
p1 : ∃ x ∈ t, p x = a
fp : ∀ x ∈ t, f (p x) = b
⊢ ∀ x ∈ t, p x = a
Tactic:
have disc : DiscreteTopology (↥(s ∩ f ⁻¹' {b})) := n.discreteTopology b
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
p1 : ∃ x ∈ t, p x = a
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
⊢ ∀ x ∈ t, p x = a
Theorem: NontrivialAnalyticOn.const
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
p1 : ∃ x ∈ t, p x = a
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
⊢ ∀ x ∈ t, p x = a
Tactic:
rcases p1 with ⟨z, zt, z1⟩
Proof state after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = a
Theorem: NontrivialAnalyticOn.const
Proof state before:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = a
Tactic:
simp only [← z1]
Proof state after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
p : X → ℂ
t : Set X
tc : IsPreconnected t
pc : ContinuousOn p t
ps : MapsTo p t s
a b : ℂ
fp : ∀ x ∈ t, f (p x) = b
disc : DiscreteTopology ↑(s ∩ f ⁻¹' {b})
z : X
zt : z ∈ t
z1 : p z = a
⊢ ∀ x ∈ t, p x = p z