Theorem: NontrivialAnalyticOn.discreteTopology (Ray/AnalyticManifold/Nontrivial.lean)

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
a : ℂ
⊢ DiscreteTopology ↑(s ∩ f ⁻¹' {a})
Tactic:
rw [← singletons_open_iff_discrete]
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
a : ℂ
⊢ ∀ (a_1 : ↑(s ∩ f ⁻¹' {a})), IsOpen {a_1}

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
a : ℂ
⊢ ∀ (a_1 : ↑(s ∩ f ⁻¹' {a})), IsOpen {a_1}
Tactic:
intro ⟨z, m⟩
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
a z : ℂ
m : z ∈ s ∩ f ⁻¹' {a}
⊢ IsOpen {⟨z, m⟩}

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
a z : ℂ
m : z ∈ s ∩ f ⁻¹' {a}
⊢ IsOpen {⟨z, m⟩}
Tactic:
simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff] at m
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
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
⊢ IsOpen {⟨z, m✝⟩}

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
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
by_cases h : ∃ᶠ z in 𝓝[{z}ᶜ] z, f z = a
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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}

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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ¬∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}

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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
have i := (n.isolated' m.1 a).and_frequently h
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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
i : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x ≠ a ∧ f x = a
⊢ IsOpen {⟨z, m✝⟩}

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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
i : ∃ᶠ (x : ℂ) in 𝓝[≠] z, f x ≠ a ∧ f x = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
simp only [not_and_self_iff, Filter.frequently_const] at i
State after:
no goals

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 : NontrivialAnalyticOn f s
a z : ℂ
m✝ : z ∈ s ∩ f ⁻¹' {a}
m : z ∈ s ∧ f z = a
h : ¬∃ᶠ (z : ℂ) in 𝓝[≠] z, f z = a
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
simp only [Filter.not_frequently, eventually_nhdsWithin_iff, Set.mem_compl_singleton_iff] at h
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 : 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
⊢ IsOpen {⟨z, m✝⟩}

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 : 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
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
rcases eventually_nhds_iff.mp h with ⟨t, t0, o, tz⟩
State after:
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
⊢ IsOpen {⟨z, m✝⟩}

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
⊢ IsOpen {⟨z, m✝⟩}
Tactic:
simp only [isOpen_induced_iff]
State after:
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✝⟩}

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
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✝⟩}

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
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✝⟩}

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⟩
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✝¹⟩}

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]
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

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
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

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
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

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
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

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
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

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
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

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]
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

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
State after:
no goals