Theorem: Super.bottcherNear_eq_zero (Ray/Dynamics/BottcherNearM.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ s.bottcherNear c z = 0 ↔ z = a
Tactic:
simp only [Super.bottcherNear]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 ↔ z = a
Tactic:
constructor
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 → z = a

case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ z = a → _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0 → z = a
Tactic:
intro za
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
⊢ z = a

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
⊢ z = a
Tactic:
contrapose za
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ¬_root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ¬_root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
apply bottcherNear_ne_zero (s.superNearC.s (Set.mem_univ _)) (s.mem_near_to_near' m)
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) (c, z).2 - ↑(extChartAt I a) a ≠ 0

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) (c, z).2 - ↑(extChartAt I a) a ≠ 0
Tactic:
simp only [sub_ne_zero]
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) z ≠ ↑(extChartAt I a) a

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : ¬z = a
⊢ ↑(extChartAt I a) z ≠ ↑(extChartAt I a) a
Tactic:
exact (extChartAt I a).injOn.ne (s.near_subset_chart m) (mem_extChartAt_source I a) za
State after:
no goals

State before:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
⊢ z = a → _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
intro za
State after:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : z = a
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0

State before:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
m : (c, z) ∈ s.near
za : z = a
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) = 0
Tactic:
simp only [za, sub_self, bottcherNear_zero]
State after:
no goals