mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g : E →L[𝕜] F
⊢ ∀ (x : E →L[𝕜] F) (v : ι → E) (i j : ι),
    v i = v j →
      i ≠ j →
        (((f.fderivCompContinuousLinearMap fun x ↦ g) ∘SL
                ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (E →L[𝕜] F))
              x)
            v =
          0

Tactic:
by
    intro dg v a b heq hne
    trans ∑ i, f fun j ↦ Function.update (fun _ ↦ g) i dg j (v j)
    · simp
    · rw [← Finset.sum_add_sum_compl {a, b}, Finset.sum_pair hne, Finset.sum_eq_zero, add_zero]
      · convert! f.map_add_swap _ hne with i
        rcases eq_or_ne i a with rfl | hia
        · simp [heq, hne, hne.symm]
        · rcases eq_or_ne i b with rfl | hib
          · simp [Function.update_apply, heq]
          · simp [Function.update_apply, Equiv.swap_apply_of_ne_of_ne, *]
      · simp only [mem_compl, mem_insert, mem_singleton, not_or, and_imp]
        intro i hia hib
        apply f.map_eq_zero_of_eq _ _ hne
        simp [*, Ne.symm]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i j : ι
hj : j ∈ {i}ᶜ
⊢ ?m.434 ≠ ?m.435

Tactic:
simpa using

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i j : ι
hj : j ∈ {i}ᶜ
⊢ ¬?m.434 = ?m.435
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: case h1
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i j : ι
hj : j ∈ {i}ᶜ
⊢ ‖(Function.update (fun x ↦ g) i dg j) (v j)‖ ≤ ‖g‖ * ‖v j‖

Tactic:
simpa using

Goal state after:
case h1
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i j : ι
hj : j ∈ {i}ᶜ
⊢ ‖g (v j)‖ ≤ ‖g‖ * ‖v j‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
v' : ι' → F
⊢ f v = 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
v : ι → E
i j : ι
hv : v i = v j
hij : i ≠ j
v' : ι' → F
⊢ f v = 0
Module: Mathlib.Analysis.Normed.Module.Completion

Goal state before:
pp: case ih
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
x y : A
⊢ ‖↑x * ↑y‖ ≤ ‖↑x‖ * ‖↑y‖

Tactic:
simpa using

Goal state after:
case ih
𝕜 : Type u_1
E : Type u_2
A : Type u_3
inst✝ : SeminormedRing A
x y : A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ |dist a b| < ε

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ |dist a b| < ε
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | dist p.1 p.2 < ε}
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f ↑a) (Completion.extension f ↑b) ≤ ↑K * dist ↑a ↑b

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (f a) (f b) ≤ ↑K * dist a b
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
N : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + -a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x + -a)
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (x : E), (p x 0).curry0 = f x

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (x : E), (p x 0) ![] = f x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m ≤ n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ p x m

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m ≤ n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ p x m
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ x ∈ univ, (p x 0).curry0 = f x

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (x : E), (p x 0) ![] = f x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ p x m) univ

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m ≤ n → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ p x m
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y ↦ p y m) (p x m.succ).curryLeft x

Tactic:
simpa using

Goal state after:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn n f p univ
⊢ ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y ↦ p y m) (p x (m + 1)).curryLeft x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m < n → ∀ x ∈ univ, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft univ x

Tactic:
simpa using

Goal state after:
case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpTo n f p
⊢ ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun x ↦ p x m) (p x (m + 1)).curryLeft 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
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x

Tactic:
simpa using

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
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ (fun p_1 ↦ f p_1.1 - f p_1.2 - ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (p_1.1 - p_1.2)) =o[𝓝 (x, x)] fun p ↦
    p.1 - p.2
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ HasStrictDerivAt f (deriv f x) x

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ HasStrictFDerivAt f (fderiv 𝕜 f x) x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : 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
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ x + y ≠ x

Tactic:
simpa using

Goal state after:
case inr
𝕜 : 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
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
h''y : y ≠ 0
Z : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (insert (x + y) s) (x + y)
⊢ ¬y = 0
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
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ fderiv 𝕜 p.sum x = p.derivSeries.sum x

Tactic:
simpa using

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
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ fderiv 𝕜 p.sum x = p.derivSeries.sum 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
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ x ∈ Metric.eball 0 p.radius

Tactic:
simpa using

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
x : E
inst✝ : CompleteSpace F
h : ‖x‖ₑ < p.radius
⊢ ‖x‖ₑ < p.radius
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (a + z)) = fun x ↦ iteratedFDeriv 𝕜 n f (a + x)

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) univ = fun x ↦ iteratedFDerivWithin 𝕜 n f univ (a + x)
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (z + a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + a)

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (z + a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + a)
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (z - a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x - a)

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z ↦ f (z + -a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + -a)
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : 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
u' : E
v' : F
hu : HasDerivWithinAt u u' s x
hv : HasDerivWithinAt v v' s x
⊢ HasDerivWithinAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x

Tactic:
simpa using

Goal state after:
𝕜 : 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
u' : E
v' : F
hu : HasDerivWithinAt u u' s x
hv : HasDerivWithinAt v v' s x
⊢ HasDerivWithinAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) 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 : 𝕜
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:
simpa using

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: 𝕜 : 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 : HasStrictDerivAt u u' x
hv : HasStrictDerivAt v v' x
⊢ HasStrictDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
simpa using

Goal state after:
𝕜 : 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 : HasStrictDerivAt u u' x
hv : HasStrictDerivAt v v' x
⊢ HasStrictDerivAt (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: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) s x

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) s x