Theorem: f_f'_iter (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
z : ℂ
⊢ (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
Tactic:
induction' n with n h
State after:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (f d c)^[0] ↑z = ↑((f' d c)^[0] z)

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)

State before:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (f d c)^[0] ↑z = ↑((f' d c)^[0] z)

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)
Tactic:
simp only [Function.iterate_zero, id]
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)
Tactic:
simp only [h, Function.iterate_succ_apply']
State after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ f d c ↑((f' d c)^[n] z) = ↑(f' d c ((f' d c)^[n] z))

State before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ f d c ↑((f' d c)^[n] z) = ↑(f' d c ((f' d c)^[n] z))
Tactic:
simp only [f, lift', rec_coe]
State after:
no goals