Theorem: Super.bottcher_eq_bottcherNear (Ray/Dynamics/Bottcher.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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Tactic:
have eq := (s.ray_nontrivial (s.mem_ext c)).nhds_eq_map_nhds
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 (s.ray c 0) = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 (s.ray c 0) = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Tactic:
simp only [s.ray_zero] at eq
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
Tactic:
simp only [eq, Filter.eventually_map]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (a_1 : ℂ) in 𝓝 0, s.bottcher c (s.ray c a_1) = s.bottcherNear c (s.ray c a_1)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (a_1 : ℂ) in 𝓝 0, s.bottcher c (s.ray c a_1) = s.bottcherNear c (s.ray c a_1)
Tactic:
apply ((continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_zero c)).mp
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    s.bottcherNear (c, id x).1 (s.ray (c, id x).1 (c, id x).2) = (c, id x).2 →
      s.bottcher c (s.ray c x) = s.bottcherNear c (s.ray c x)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    s.bottcherNear (c, id x).1 (s.ray (c, id x).1 (c, id x).2) = (c, id x).2 →
      s.bottcher c (s.ray c x) = s.bottcherNear c (s.ray c x)
Tactic:
refine ((s.isOpen_ext.snd_preimage c).eventually_mem (s.mem_ext c)).mp
  (eventually_of_forall fun z m e ↦ ?_)
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ s.bottcher c (s.ray c z) = s.bottcherNear c (s.ray c z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ s.bottcher c (s.ray c z) = s.bottcherNear c (s.ray c z)
Tactic:
simp only [s.bottcher_ray 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✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ z = s.bottcherNear c (s.ray c z)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
eq : 𝓝 a = Filter.map (s.ray c) (𝓝 0)
z : ℂ
m : z ∈ {b | (c, b) ∈ s.ext}
e : s.bottcherNear (c, id z).1 (s.ray (c, id z).1 (c, id z).2) = (c, id z).2
⊢ z = s.bottcherNear c (s.ray c z)
Tactic:
exact e.symm
State after:
no goals