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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
t : ℝ
ht : t ∈ Ico 0 1
I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖)
⊢ ‖(fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w) t‖ =
    ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖

Tactic:
]

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
t : ℝ
ht : t ∈ Ico 0 1
I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖)
⊢ ‖(fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w) t‖ =
    ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case neg
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
x : α
hx : x ∈ s
h'x : x ∉ s'
y : α
yt0 : y ∈ t0
hxy : x ∈ closedBall y (r0 y)
⊢ x ∈ closedBall y (r0 y)

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
x : α
hx : x ∈ s
h'x : x ∉ s'
y : α
yt0 : y ∈ t0
hxy : x ∈ closedBall y (r0 y)
⊢ x ∈ closedBall y (r0 y)
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V₁ s x) (W x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W x))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
s : Set E
x : E
hV : DifferentiableWithinAt 𝕜 V s x
hV₁ : DifferentiableWithinAt 𝕜 V₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W s x) (V₁ x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V₁ s x) (W x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W s x) (V₁ x) - (fderivWithin 𝕜 V₁ s x) (W x))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W x) (V₁ x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V₁ x) (W x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 V₁ x) (W x))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W x) (V₁ x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V₁ x) (W x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 V₁ x) (W x))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W₁ s x) (V x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
s : Set E
x : E
hW : DifferentiableWithinAt 𝕜 W s x
hW₁ : DifferentiableWithinAt 𝕜 W₁ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 W s x) (V x) + (fderivWithin 𝕜 W₁ s x) (V x) -
      ((fderivWithin 𝕜 V s x) (W x) + (fderivWithin 𝕜 V s x) (W₁ x)) =
    (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x) +
      ((fderivWithin 𝕜 W₁ s x) (V x) - (fderivWithin 𝕜 V s x) (W₁ x))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W₁ x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W₁ x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case e_f
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
x : ↑t0
⊢ μ (closedBall (↑x) (r0 ↑x)) = μ (closedBall (↑x) (r0 ↑x))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
t : ℝ
ht : t ∈ Ico 0 1
I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖)
⊢ ‖h • v + (t * h) • w‖ < δ

Tactic:
]

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
g : ℝ → F :=
  fun t ↦ f (x + h • v + (t * h) • w) - (t * h) • (f' x) w - (t * h ^ 2) • (f'' v) w - ((t * h) ^ 2 / 2) • (f'' w) w
g' : ℝ → F :=
  fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
hg' : g' = fun t ↦ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w
g_deriv : ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t
t : ℝ
ht : t ∈ Ico 0 1
I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖)
⊢ ‖h • v + (t * h) • w‖ < δ
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : ℕ∞ω
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap

Goal state before:
pp: case intro.mp
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
val✝ : Fintype ι
h :
  (fun p ↦
      (toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2 -
        (toContinuousMultilinearMapCLM 𝕜 ∘SL f') (p.1 - p.2)) =o[𝕜;
    𝓝 (x, x)] fun p ↦ p.1 - p.2
⊢ (fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; 𝓝 (x, x)] fun p ↦ p.1 - p.2

Tactic:
]

Goal state after:
case intro.mp
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
val✝ : Fintype ι
h :
  (fun p ↦
      (toContinuousMultilinearMap ∘ f) p.1 - (toContinuousMultilinearMap ∘ f) p.2 -
        (toContinuousMultilinearMapCLM 𝕜 ∘SL f') (p.1 - p.2)) =o[𝕜;
    𝓝 (x, x)] fun p ↦ p.1 - p.2
⊢ (fun p ↦ f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; 𝓝 (x, x)] fun p ↦ p.1 - p.2
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
h : s ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W univ x = lieBracketWithin 𝕜 V W univ x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracketWithin 𝕜 V W univ x = lieBracketWithin 𝕜 V W univ x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x

Tactic:
by
  cases nonempty_fintype ι
  constructor <;> intro h
  · rw [hasStrictFDerivAt_iff_isLittleOTVS] at h ⊢
    refine Asymptotics.IsBigOTVS.trans_isLittleOTVS ?_ h
    simp only [Function.comp_apply, ← toContinuousMultilinearMapCLM_apply 𝕜,
      ContinuousLinearMap.comp_apply, ← map_sub]
    apply LinearMap.isBigOTVS_rev_comp
    simp [isEmbedding_toContinuousMultilinearMap.nhds_eq_comap]
  · exact (toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt.comp x h

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ fun fg ↦ fg.1.compContinuousLinearMap fg.2)
    (toContinuousMultilinearMapCLM 𝕜 ∘SL
      (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) +
        fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G)))
    fg

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
F : Type u_4
G : Type u_5
H : Type u_6
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ fun fg ↦ fg.1.compContinuousLinearMap fg.2)
    (toContinuousMultilinearMapCLM 𝕜 ∘SL
      (compContinuousLinearMapCLM fg.2 ∘SL ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) +
        fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G)))
    fg
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
aux₁ :
  ∀ {U V : E → E},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x → DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x)) s x
aux₂ :
  ∀ {U V : E → E},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x →
        fderivWithin 𝕜 (fun y ↦ (fderivWithin 𝕜 U s y) (V y)) s x =
          fderivWithin 𝕜 U s x ∘SL fderivWithin 𝕜 V s x + (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x).flip (V x)
⊢ (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 W s x) (V x)) s x -
          fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (W x)) s x)
        (U x) -
      ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) - (fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x))) =
    (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 V s x) (U x)) - (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) -
        (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x) - (fderivWithin 𝕜 U s x) (V x)) s x) (W x) +
      ((fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 W s x) (U x) - (fderivWithin 𝕜 U s x) (W x)) s x) (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 2 U s x
hV : ContDiffWithinAt 𝕜 2 V s x
hW : ContDiffWithinAt 𝕜 2 W s x
h'U : IsSymmSndFDerivWithinAt 𝕜 U s x
h'V : IsSymmSndFDerivWithinAt 𝕜 V s x
h'W : IsSymmSndFDerivWithinAt 𝕜 W s x
aux₁ :
  ∀ {U V : E → E},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x → DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x)) s x
aux₂ :
  ∀ {U V : E → E},
    ContDiffWithinAt 𝕜 2 U s x →
      ContDiffWithinAt 𝕜 2 V s x →
        fderivWithin 𝕜 (fun y ↦ (fderivWithin 𝕜 U s y) (V y)) s x =
          fderivWithin 𝕜 U s x ∘SL fderivWithin 𝕜 V s x + (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x).flip (V x)
⊢ (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 W s x) (V x)) s x -
          fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (W x)) s x)
        (U x) -
      ((fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 W s x) (V x)) - (fderivWithin 𝕜 U s x) ((fderivWithin 𝕜 V s x) (W x))) =
    (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 V s x) (U x)) - (fderivWithin 𝕜 W s x) ((fderivWithin 𝕜 U s x) (V x)) -
        (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x) - (fderivWithin 𝕜 U s x) (V x)) s x) (W x) +
      ((fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 W s x) (U x) - (fderivWithin 𝕜 U s x) (W x)) s x) (V x) -
        ((fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 W s x) (U x)) - (fderivWithin 𝕜 V s x) ((fderivWithin 𝕜 U s x) (W x))))