Theorem: Super.bottcher_eq_bottcherPost (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
⊢ s.bottcher c z = s.bottcherPost c z
Tactic:
have h : ∃ n, (c, (f c)^[n] z) ∈ s.post := ⟨0, by simpa only [Function.iterate_zero_apply]⟩
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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c z = s.bottcherPost 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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c z = s.bottcherPost c z
Tactic:
have h0 := (Nat.find_eq_zero h).mpr 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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
h0 : Nat.find h = 0
⊢ s.bottcher c z = s.bottcherPost 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
m : (c, z) ∈ s.post
h : ∃ n, (c, (f c)^[n] z) ∈ s.post
h0 : Nat.find h = 0
⊢ s.bottcher c z = s.bottcherPost c z
Tactic:
simp only [Super.bottcher, h, dif_pos, h0, Function.iterate_zero_apply, pow_zero, inv_one,
  Complex.cpow_one]
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 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, (f c)^[0] z) ∈ s.post
Tactic:
simpa only [Function.iterate_zero_apply]
State after:
no goals