Theorem: bottcher_mfderiv_inf_ne_zero (Ray/Dynamics/Multibrot/Bottcher.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ mfderiv I I (bottcher d) ∞ ≠ 0
Tactic:
simp only [mfderiv, (bottcherHolomorphic d _ multibrotExt_inf).mdifferentiableAt, if_pos,
  writtenInExtChartAt, bottcher_inf, extChartAt_inf, extChartAt_eq_refl, Function.comp,
  PartialEquiv.refl_coe, id, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply,
  RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, PartialEquiv.coe_trans_symm,
  PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm,
  ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fderiv ℂ (fun x => bottcher d (↑x)⁻¹) 0 ≠ 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fderiv ℂ (fun x => bottcher d (↑x)⁻¹) 0 ≠ 0
Tactic:
rw [bottcher_hasDerivAt_one.hasFDerivAt.fderiv]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousLinearMap.smulRight 1 1 ≠ 0
Tactic:
rw [Ne, ContinuousLinearMap.ext_iff, not_forall]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∃ x, ¬(ContinuousLinearMap.smulRight 1 1) x = 0 x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∃ x, ¬(ContinuousLinearMap.smulRight 1 1) x = 0 x
Tactic:
use 1
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬(ContinuousLinearMap.smulRight 1 1) 1 = 0 1

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬(ContinuousLinearMap.smulRight 1 1) 1 = 0 1
Tactic:
simp only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
  Algebra.id.smul_eq_mul, mul_one, ContinuousLinearMap.zero_apply]
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬1 = 0 1

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ¬1 = 0 1
Tactic:
convert one_ne_zero
State after:
case h.convert_4
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ NeZero 1

State before:
case h.convert_4
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ NeZero 1
Tactic:
exact NeZero.one
State after:
no goals