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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * term f d 0 z) ^ d
Tactic:
rw [term]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d (f^[0] z) ^ (1 / ↑(d ^ (0 + 1)))) ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d (f^[0] z) ^ (1 / ↑(d ^ (0 + 1)))) ^ d
Tactic:
simp only [Function.iterate_zero, id, pow_one, one_div]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d z ^ (↑(d ^ (0 + 1)))⁻¹) ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d z ^ (↑(d ^ (0 + 1)))⁻¹) ^ d
Tactic:
rw [mul_pow, pow_mul_nat, zero_add, pow_one, inv_mul_cancel _]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = z ^ d * g f d z ^ 1

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ↑d ≠ 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = z ^ d * g f d z ^ 1
Tactic:
rw [s.fg]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ z ^ d * g f d z = z ^ d * g f d z ^ 1

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ z ^ d * g f d z = z ^ d * g f d z ^ 1
Tactic:
simp only [Complex.cpow_one]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ↑d ≠ 0
Tactic:
simp only [Ne, Nat.cast_eq_zero]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ¬d = 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ¬d = 0
Tactic:
exact (gt_of_ge_of_gt s.d2 (by norm_num)).ne'
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ 2 > 0
Tactic:
norm_num
State after:
no goals