Theorem: bottcherNear_eqn_iter (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
⊢ bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
Tactic:
induction' n with n h
State after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ bottcherNear f d (f^[0] z) = bottcherNear f d z ^ d ^ 0

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)

State before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ bottcherNear f d (f^[0] z) = bottcherNear f d z ^ d ^ 0

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_zero, id, pow_zero, pow_one]
State after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)
Tactic:
simp only [Function.comp, Function.iterate_succ', pow_succ, pow_mul,
  bottcherNear_eqn s (s.mapsTo n zt), h]
State after:
no goals