Theorem: AnalyticManifold.nonseparating_singleton (Ray/AnalyticManifold/Nonseparating.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : S
⊢ Nonseparating {a}
Tactic:
apply Nonseparating.complexManifold
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : S
⊢ ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : S
⊢ ∀ (z : S), Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
intro z
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
by_cases az : a ∈ (extChartAt I z).source
State after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})

State before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
convert Complex.nonseparating_singleton (extChartAt I z a)
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = {↑(extChartAt I z) a}

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = {↑(extChartAt I z) a}
Tactic:
simp only [eq_singleton_iff_unique_mem, mem_inter_iff, PartialEquiv.map_source _ az, true_and_iff,
  mem_preimage, mem_singleton_iff, PartialEquiv.left_inv _ az, eq_self_iff_true]
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ ∀ (x : ℂ), x ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x = a → x = ↑(extChartAt I z) a

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
⊢ ∀ (x : ℂ), x ∈ (extChartAt I z).target ∧ ↑(extChartAt I z).symm x = a → x = ↑(extChartAt I z) a
Tactic:
intro x ⟨m, e⟩
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
e : ↑(extChartAt I z).symm x = a
⊢ x = ↑(extChartAt I z) a

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∈ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
e : ↑(extChartAt I z).symm x = a
⊢ x = ↑(extChartAt I z) a
Tactic:
simp only [← e, PartialEquiv.right_inv _ m]
State after:
no goals

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ Nonseparating ((extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a})
Tactic:
convert Nonseparating.empty
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = ∅

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ (extChartAt I z).target ∩ ↑(extChartAt I z).symm ⁻¹' {a} = ∅
Tactic:
simp only [eq_empty_iff_forall_not_mem, mem_inter_iff, mem_preimage, mem_singleton_iff, not_and]
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ ∀ x ∈ (extChartAt I z).target, ¬↑(extChartAt I z).symm x = a

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
⊢ ∀ x ∈ (extChartAt I z).target, ¬↑(extChartAt I z).symm x = a
Tactic:
intro x m
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
⊢ ¬↑(extChartAt I z).symm x = a

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
az : a ∉ (extChartAt I z).source
x : ℂ
m : x ∈ (extChartAt I z).target
⊢ ¬↑(extChartAt I z).symm x = a
Tactic:
contrapose az
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ¬¬↑(extChartAt I z).symm x = a
⊢ ¬a ∉ (extChartAt I z).source

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ¬¬↑(extChartAt I z).symm x = a
⊢ ¬a ∉ (extChartAt I z).source
Tactic:
simp only [not_not] at az ⊢
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ a ∈ (extChartAt I z).source

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ a ∈ (extChartAt I z).source
Tactic:
rw [← az]
State after:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ ↑(extChartAt I z).symm x ∈ (extChartAt I z).source

State before:
case h.e'_3
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a z : S
x : ℂ
m : x ∈ (extChartAt I z).target
az : ↑(extChartAt I z).symm x = a
⊢ ↑(extChartAt I z).symm x ∈ (extChartAt I z).source
Tactic:
exact PartialEquiv.map_target _ m
State after:
no goals