Theorem: Super.bottcher_eqn_iter (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
n : ℕ
⊢ s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
Tactic:
induction' n with n h
State after:
case zero
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
⊢ s.bottcher c ((f c)^[0] z) = s.bottcher c z ^ d ^ 0

case succ
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
n : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)

State before:
case zero
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
⊢ s.bottcher c ((f c)^[0] z) = s.bottcher c z ^ d ^ 0

case succ
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
n : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_zero_apply, pow_zero, pow_one]
State after:
case succ
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
n : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)

State before:
case succ
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
n : ℕ
h : s.bottcher c ((f c)^[n] z) = s.bottcher c z ^ d ^ n
⊢ s.bottcher c ((f c)^[n + 1] z) = s.bottcher c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_succ_apply', s.bottcher_eqn, h, ← pow_mul, pow_succ]
State after:
no goals