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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), term f d n (f z) = term f d (n + 1) z ^ d
Tactic:
intro n
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ term f d n (f z) = term f d (n + 1) z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ term f d n (f z) = term f d (n + 1) z ^ d
Tactic:
simp only [term, ← Function.iterate_succ_apply, pow_mul_nat, div_mul, pow_succ' _ (n + 1),
  mul_div_cancel_left₀ _ s.dz, Nat.succ_eq_add_one, Nat.cast_mul]
State after:
no goals