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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
have dz : HasDerivAt (fun z : ℂ ↦ z) 1 0 := hasDerivAt_id 0
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
have db := HasDerivAt.mul dz (term_prod_analytic_z s 0 s.t0).differentiableAt.hasDerivAt
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (1 * tprodOn (term f d) 0 + 0 * deriv (tprodOn (term f d)) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (1 * tprodOn (term f d) 0 + 0 * deriv (tprodOn (term f d)) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
simp only [one_mul, MulZeroClass.zero_mul, add_zero] at db
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (tprodOn (term f d) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (tprodOn (term f d) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
rw [term_prod_at_zero s] at db
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
exact db
State after:
no goals