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

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
⊢ f z = z ^ d * g f d z
Tactic:
by_cases z0 : z = 0
State after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : z = 0
⊢ f z = z ^ d * g f d z

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * g f d z

State before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : z = 0
⊢ f z = z ^ d * g f d z
Tactic:
simp only [z0, zero_pow s.d0, s.f0, MulZeroClass.zero_mul]
State after:
no goals

State before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * g f d z
Tactic:
simp only [g, z0, if_false]
State after:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * (f z / z ^ d)

State before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * (f z / z ^ d)
Tactic:
field_simp [z0]
State after:
no goals