Theorem: Super.bottcher_ext (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
m : (c, z) ∈ s.post
⊢ (c, s.bottcher c z) ∈ s.ext
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
State after:
case intro.intro
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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, s.bottcher c z) ∈ s.ext

State before:
case intro.intro
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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, s.bottcher c z) ∈ s.ext
Tactic:
rw [← e, s.bottcher_ray m]
State after:
case intro.intro
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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, x) ∈ s.ext

State before:
case intro.intro
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
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ (c, x) ∈ s.ext
Tactic:
exact m
State after:
no goals