internlm/Lean-Github huggingface dataset:
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case neg.intro.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
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {⟨z, m✝⟩}
Tactic:
use t, o
Proof state after:
case right
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
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ Subtype.val ⁻¹' t = {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right
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
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ Subtype.val ⁻¹' t = {⟨z, m✝⟩}
Tactic:
apply Set.ext
Proof state after:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ ∀ (x : ↑(s ∩ f ⁻¹' {a})), x ∈ Subtype.val ⁻¹' t ↔ x ∈ {⟨z, m✝⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
⊢ ∀ (x : ↑(s ∩ f ⁻¹' {a})), x ∈ Subtype.val ⁻¹' t ↔ x ∈ {⟨z, m✝⟩}
Tactic:
intro ⟨w, m⟩
Proof state after:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∩ f ⁻¹' {a}
⊢ ⟨w, m⟩ ∈ Subtype.val ⁻¹' t ↔ ⟨w, m⟩ ∈ {⟨z, m✝¹⟩}
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∩ f ⁻¹' {a}
⊢ ⟨w, m⟩ ∈ Subtype.val ⁻¹' t ↔ ⟨w, m⟩ ∈ {⟨z, m✝¹⟩}
Tactic:
simp only [Set.mem_preimage, Subtype.coe_mk, Set.mem_singleton_iff, Subtype.mk_eq_mk]
Proof state after:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∩ f ⁻¹' {a}
⊢ w ∈ t ↔ w = z
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∩ f ⁻¹' {a}
⊢ w ∈ t ↔ w = z
Tactic:
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff] at m
Proof state after:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
⊢ w ∈ t ↔ w = z
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
t0 : ∀ x ∈ t, x ≠ z → ¬f x = a
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
⊢ w ∈ t ↔ w = z
Tactic:
specialize t0 w
Proof state after:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w ≠ z → ¬f w = a
⊢ w ∈ t ↔ w = z
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w ≠ z → ¬f w = a
⊢ w ∈ t ↔ w = z
Tactic:
simp only [m.2, imp_false, eq_self_iff_true, not_true, not_not] at t0
Proof state after:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
⊢ w ∈ t ↔ w = z
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case right.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 : NontrivialAnalyticOn f s
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
⊢ w ∈ t ↔ w = z
Tactic:
use t0
Proof state after:
case mpr
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
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
⊢ w = z → w ∈ t
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case mpr
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
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
⊢ w = z → w ∈ t
Tactic:
intro wz
Proof state after:
case mpr
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
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
wz : w = z
⊢ w ∈ t
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case mpr
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
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
wz : w = z
⊢ w ∈ t
Tactic:
rw [wz]
Proof state after:
case mpr
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
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
wz : w = z
⊢ z ∈ t
Theorem: NontrivialAnalyticOn.discreteTopology
Proof state before:
case mpr
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
a z : ℂ
m✝¹ : z ∈ s ∩ f ⁻¹' {a}
m✝ : z ∈ s ∧ f z = a
h : ∀ᶠ (x : ℂ) in 𝓝 z, x ≠ z → ¬f x = a
t : Set ℂ
o : IsOpen t
tz : z ∈ t
w : ℂ
m : w ∈ s ∧ f w = a
t0 : w ∈ t → w = z
wz : w = z
⊢ z ∈ t
Tactic:
exact tz
Proof state after:
no goals
Theorem: powNontrivial
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 ℂ
d : ℕ
dp : 0 < d
⊢ NontrivialAnalyticOn (fun z => z ^ d) univ
Tactic:
apply Entire.nontrivialAnalyticOn fun _ _ ↦ (analyticAt_id _ _).pow _
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 ℂ
d : ℕ
dp : 0 < d
⊢ ∃ a b, id a ^ d ≠ id b ^ d
Theorem: powNontrivial
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 ℂ
d : ℕ
dp : 0 < d
⊢ ∃ a b, id a ^ d ≠ id b ^ d
Tactic:
use 0, 1
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 ℂ
d : ℕ
dp : 0 < d
⊢ id 0 ^ d ≠ id 1 ^ d
Theorem: powNontrivial
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 ℂ
d : ℕ
dp : 0 < d
⊢ id 0 ^ d ≠ id 1 ^ d
Tactic:
simp only [id, one_pow, zero_pow (Nat.pos_iff_ne_zero.mp dp), Pi.pow_def]
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 ℂ
d : ℕ
dp : 0 < d
⊢ 0 ≠ 1
Theorem: powNontrivial
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 ℂ
d : ℕ
dp : 0 < d
⊢ 0 ≠ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: allRootsOfUnity.ne_zero
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 ℂ
z : ℂ
m : z ∈ allRootsOfUnity
⊢ z ≠ 0
Tactic:
rcases m with ⟨n, n0, 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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : z ^ n = 1
⊢ z ≠ 0
Theorem: allRootsOfUnity.ne_zero
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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : z ^ n = 1
⊢ z ≠ 0
Tactic:
contrapose 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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : ¬z ≠ 0
⊢ ¬z ^ n = 1
Theorem: allRootsOfUnity.ne_zero
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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : ¬z ≠ 0
⊢ ¬z ^ n = 1
Tactic:
simp only [not_not] at 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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : z = 0
⊢ ¬z ^ n = 1
Theorem: allRootsOfUnity.ne_zero
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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : z = 0
⊢ ¬z ^ n = 1
Tactic:
simp only [z1, zero_pow n0]
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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : z = 0
⊢ ¬0 = 1
Theorem: allRootsOfUnity.ne_zero
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 ℂ
z : ℂ
n : ℕ
n0 : n ≠ 0
z1 : z = 0
⊢ ¬0 = 1
Tactic:
exact zero_ne_one
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 ℂ
⊢ IsTotallyDisconnected _root_.allRootsOfUnity
Tactic:
apply IsCountable.isTotallyDisconnected
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 ℂ
⊢ _root_.allRootsOfUnity.Countable
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 ℂ
⊢ _root_.allRootsOfUnity.Countable
Tactic:
simp only [_root_.allRootsOfUnity, setOf_exists]
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 ℂ
⊢ (⋃ i, {x | i ≠ 0 ∧ x ^ i = 1}).Countable
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 ℂ
⊢ (⋃ i, {x | i ≠ 0 ∧ x ^ i = 1}).Countable
Tactic:
apply countable_iUnion
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 ℂ
⊢ ∀ (i : ℕ), {x | i ≠ 0 ∧ x ^ i = 1}.Countable