Theorem: Super.bottcherNear_eqn (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 (f c z) = s.bottcherNear c z ^ d
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) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d

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) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d
Tactic:
have e : extChartAt I a (f c z) - extChartAt I a a =
    s.fl c (extChartAt I a z - extChartAt I a a) := by
  simp only [Function.comp, Super.fl, _root_.fl, sub_add_cancel,
    PartialEquiv.left_inv _ (s.near_subset_chart m)]
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
e : ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a = s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d

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
e : ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a = s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a)
⊢ _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a) =
    _root_.bottcherNear (s.fl c) d (↑(extChartAt I a) z - ↑(extChartAt I a) a) ^ d
Tactic:
rw [e, _root_.bottcherNear_eqn (s.superNearC.s (Set.mem_univ c)) (s.mem_near_to_near' m)]
State after:
no goals

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
⊢ ↑(extChartAt I a) (f c z) - ↑(extChartAt I a) a = s.fl c (↑(extChartAt I a) z - ↑(extChartAt I a) a)
Tactic:
simp only [Function.comp, Super.fl, _root_.fl, sub_add_cancel,
  PartialEquiv.left_inv _ (s.near_subset_chart m)]
State after:
no goals