Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
a n : ℕ
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
h : (Function.swap dslope c)^[n + a] (fun z => g z) c = (Function.swap dslope c)^[a] f c
⊢ (c - c) • deriv (fun z => g z) c + deriv (fun z => z - c) c • g c = g c

case hc
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
a n : ℕ
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
h : (Function.swap dslope c)^[n + a] (fun z => g z) c = (Function.swap dslope c)^[a] f c
⊢ DifferentiableAt 𝕜 (fun z => z - c) c

case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
a n : ℕ
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
h : (Function.swap dslope c)^[n + a] (fun z => g z) c = (Function.swap dslope c)^[a] f c
⊢ DifferentiableAt 𝕜 (fun z => g z) c
Tactic:
simp only [sub_self, zero_smul, deriv_sub, differentiableAt_id', differentiableAt_const,
  deriv_id'', deriv_const', sub_zero, one_smul, zero_add]
Proof state after:
case hc
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
a n : ℕ
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
h : (Function.swap dslope c)^[n + a] (fun z => g z) c = (Function.swap dslope c)^[a] f c
⊢ DifferentiableAt 𝕜 (fun z => z - c) c

case hf
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
fnz : ∃ᶠ (z : 𝕜) in 𝓝 c, f z ≠ 0
a n : ℕ
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
h : (Function.swap dslope c)^[n + a] (fun z => g z) c = (Function.swap dslope c)^[a] f c
⊢ DifferentiableAt 𝕜 (fun z => g z) c