Theorem: AnalyticAt.monomial_mul_leadingCoeff (Ray/Analytic/Analytic.lean)

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
n : ℕ
⊢ leadingCoeff (fun z => (z - c) ^ n • f z) c = leadingCoeff f c
Tactic:
simp [leadingCoeff, fa.monomial_mul_orderAt fnz n]
State after:
𝕜 : 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
n : ℕ
⊢ (Function.swap dslope c)^[n + orderAt f c] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[orderAt f c] f c

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
n : ℕ
⊢ (Function.swap dslope c)^[n + orderAt f c] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[orderAt f c] f c
Tactic:
generalize orderAt f c = a
State after:
𝕜 : 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
n a : ℕ
⊢ (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c

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
n a : ℕ
⊢ (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
Tactic:
induction' n with n h
State after:
case zero
𝕜 : 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 : ℕ
⊢ (Function.swap dslope c)^[0 + a] (fun z => (z - c) ^ 0 • f z) c = (Function.swap dslope c)^[a] f c

case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + 1 + a] (fun z => (z - c) ^ (n + 1) • f z) c = (Function.swap dslope c)^[a] f c

State before:
case zero
𝕜 : 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 : ℕ
⊢ (Function.swap dslope c)^[0 + a] (fun z => (z - c) ^ 0 • f z) c = (Function.swap dslope c)^[a] f c
Tactic:
simp only [zero_add, pow_zero, one_smul, Nat.zero_eq]
State after:
no goals

State before:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + 1 + a] (fun z => (z - c) ^ (n + 1) • f z) c = (Function.swap dslope c)^[a] f c
Tactic:
simp [pow_succ', ← smul_smul, Nat.succ_add]
State after:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c

State before:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Tactic:
generalize hg : (fun z ↦ (z - c) ^ n • f z) = g
State after:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c

State before:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Tactic:
have hg' : ∀ z, (z - c) ^ n • f z = g z := by
  rw [←hg]; simp only [eq_self_iff_true, forall_const]
State after:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c

State before:
case succ
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
hg' : ∀ (z : 𝕜), (z - c) ^ n • f z = g z
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • (z - c) ^ n • f z) c =
    (Function.swap dslope c)^[a] f c
Tactic:
simp_rw [hg'] at h ⊢
State after:
case succ
𝕜 : 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
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • g z) c = (Function.swap dslope c)^[a] f c

State before:
case succ
𝕜 : 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
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • g z) c = (Function.swap dslope c)^[a] f c
Tactic:
have e : (Function.swap dslope c fun z ↦ (z - c) • g z) = g := by
  simp only [Function.swap, dslope_sub_smul, Function.update_eq_self_iff, sub_self]
  rw [deriv_smul]
  simp only [sub_self, zero_smul, deriv_sub, differentiableAt_id', differentiableAt_const,
    deriv_id'', deriv_const', sub_zero, one_smul, zero_add]
  exact differentiableAt_id.sub (differentiableAt_const _)
  rw [←hg]
  exact ((differentiableAt_id.sub (differentiableAt_const _)).pow _).smul fa.differentiableAt
State after:
case succ
𝕜 : 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
e : (Function.swap dslope c fun z => (z - c) • g z) = g
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • g z) c = (Function.swap dslope c)^[a] f c

State before:
case succ
𝕜 : 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
e : (Function.swap dslope c fun z => (z - c) • g z) = g
⊢ (Function.swap dslope c)^[n + a] (Function.swap dslope c fun z => (z - c) • g z) c = (Function.swap dslope c)^[a] f c
Tactic:
rw [e, h]
State after:
no goals

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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ ∀ (z : 𝕜), (z - c) ^ n • f z = g z
Tactic:
rw [←hg]
State after:
𝕜 : 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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ ∀ (z : 𝕜), (z - c) ^ n • f z = (fun z => (z - c) ^ n • f z) z

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 : ℕ
h : (Function.swap dslope c)^[n + a] (fun z => (z - c) ^ n • f z) c = (Function.swap dslope c)^[a] f c
g : 𝕜 → E
hg : (fun z => (z - c) ^ n • f z) = g
⊢ ∀ (z : 𝕜), (z - c) ^ n • f z = (fun z => (z - c) ^ n • f z) z
Tactic:
simp only [eq_self_iff_true, forall_const]
State after:
no goals

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
⊢ (Function.swap dslope c fun z => (z - c) • g z) = g
Tactic:
simp only [Function.swap, dslope_sub_smul, Function.update_eq_self_iff, sub_self]
State after:
𝕜 : 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
⊢ deriv (fun z => (z - c) • g z) c = g c

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
⊢ deriv (fun z => (z - c) • g z) c = g c
Tactic:
rw [deriv_smul]
State after:
𝕜 : 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

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]
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

State before:
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:
exact differentiableAt_id.sub (differentiableAt_const _)
State after:
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

State before:
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:
rw [←hg]
State after:
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 => (fun z => (z - c) ^ n • f z) z) c

State before:
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 => (fun z => (z - c) ^ n • f z) z) c
Tactic:
exact ((differentiableAt_id.sub (differentiableAt_const _)).pow _).smul fa.differentiableAt
State after:
no goals