Theorem: SuperAt.approx (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Tactic:
have a := s.fa0.leading_approx
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - (z - 0) ^ orderAt f 0 • leadingCoeff f 0) =o[𝓝 0] fun z => (z - 0) ^ orderAt f 0
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - (z - 0) ^ orderAt f 0 • leadingCoeff f 0) =o[𝓝 0] fun z => (z - 0) ^ orderAt f 0
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Tactic:
simp only [s.fd, s.fc, sub_zero, Pi.one_apply, Algebra.id.smul_eq_mul, mul_one] at a
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Tactic:
exact a
State after:
no goals