internlm/Lean-Github huggingface dataset:
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof 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 ⊢
Proof 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
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof 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
Proof 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
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof 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]
Proof state after:
no goals
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 : ℕ
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]
Proof 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
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 : ℕ
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]
Proof state after:
no goals
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
⊢ (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]
Proof 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
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
⊢ deriv (fun z => (z - c) • g z) c = g c
Tactic:
rw [deriv_smul]
Proof 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
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof 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 _)
Proof 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
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof 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]
Proof 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
Theorem: AnalyticAt.monomial_mul_leadingCoeff
Proof 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
Proof state after:
no goals
Theorem: AnalyticAt.fderiv
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 → F
c : E
fa : AnalyticAt 𝕜 f c
⊢ AnalyticAt 𝕜 (_root_.fderiv 𝕜 f) c
Tactic:
rcases Metric.isOpen_iff.mp (isOpen_analyticAt 𝕜 f) _ fa with ⟨r, rp, fa⟩
Proof state after:
case intro.intro
𝕜 : 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 → F
c : E
fa✝ : AnalyticAt 𝕜 f c
r : ℝ
rp : r > 0
fa : ball c r ⊆ {x | AnalyticAt 𝕜 f x}
⊢ AnalyticAt 𝕜 (_root_.fderiv 𝕜 f) c
Theorem: AnalyticAt.fderiv
Proof state before:
case intro.intro
𝕜 : 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 → F
c : E
fa✝ : AnalyticAt 𝕜 f c
r : ℝ
rp : r > 0
fa : ball c r ⊆ {x | AnalyticAt 𝕜 f x}
⊢ AnalyticAt 𝕜 (_root_.fderiv 𝕜 f) c
Tactic:
exact AnalyticOn.fderiv fa _ (Metric.mem_ball_self rp)
Proof state after:
no goals
Theorem: AnalyticAt.deriv
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 : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv f x) c
Tactic:
simp only [← fderiv_deriv]
Proof 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 : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c
Theorem: AnalyticAt.deriv
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 : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c
Tactic:
have a1 : ∀ g, AnalyticAt 𝕜 (fun g : 𝕜 →L[𝕜] 𝕜 ↦ ContinuousLinearMap.apply 𝕜 𝕜 1 g) g := fun g ↦
  ContinuousLinearMap.analyticAt _ _
Proof 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 : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
a1 : ∀ (g : 𝕜 →L[𝕜] 𝕜), AnalyticAt 𝕜 (fun g => ((ContinuousLinearMap.apply 𝕜 𝕜) 1) g) g
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c
Theorem: AnalyticAt.deriv
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 : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
a1 : ∀ (g : 𝕜 →L[𝕜] 𝕜), AnalyticAt 𝕜 (fun g => ((ContinuousLinearMap.apply 𝕜 𝕜) 1) g) g
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c
Tactic:
refine (a1 _).comp fa.fderiv
Proof state after:
no goals
Theorem: AnalyticAt.deriv2
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
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv (f x.1) x.2) c
Tactic:
set p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := ContinuousLinearMap.apply 𝕜 𝕜 (0, 1)
Proof 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
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv (f x.1) x.2) c
Theorem: AnalyticAt.deriv2
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
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
e : ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv (f x.1) x.2) c
Tactic:
rw [analyticAt_congr e]
Proof 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
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
e : ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
⊢ AnalyticAt 𝕜 (fun x => p (_root_.fderiv 𝕜 (uncurry f) x)) c