mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ ↑‖z - x‖₊ < r

pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ x + (z - x) ∈ insert x s

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ ↑‖z - x‖₊ < r
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ x + (z - x) ∈ insert x s

Tactic:
·

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ x + (z - x) ∈ insert x s
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∈ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∈ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∈ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∉ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∈ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∉ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
hxv : x ∉ tsupport v
⊢ (B (u x)) v' + (B u') (v x) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) (ftaylorSeries 𝕜 f x m.succ).curryLeft s x

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) s x

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) (ftaylorSeries 𝕜 f x m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) s x

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticOnNhd 𝕜 f s
m : ℕ
_hm : ↑m ≤ n
x : E
hx : x ∈ s
⊢ ContinuousWithinAt (fun x ↦ ftaylorSeries 𝕜 f x m) s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 g) (insert x s ∩ v)

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ftaylorSeries 𝕜 g x i) (insert x s ∩ v)

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 g) (insert x s ∩ v)
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ftaylorSeries 𝕜 g x i) (insert x s ∩ v)

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ftaylorSeries 𝕜 g x i) (insert x s ∩ v)
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n : ℕ
⊢ HasStrictFDerivAt (f ^ 0) (∑ i ∈ Finset.range 0, f x ^ (Nat.pred 0 - i) •> f' <• f x ^ i) x

Tactic:
simpa using! hasStrictFDerivAt_const 1 x

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

pp: case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f

pp: case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f

Tactic:
·

Goal state after:
case pos
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f

Tactic:
·

Goal state after:
case neg
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c y • f) s x = derivWithin c s x • f