mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_3.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : α → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : ↑v ⊆ s'
hμv : μ (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s'
hv : (↑v).PairwiseDisjoint fun x ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun x ↦ (x, r x)) v
h'p : p ∈ Finset.image (fun x ↦ (x, r x)) v
⊢ p.2 ∈ f p.1

Tactic:
rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩

Goal state after:
case refine_3.inr
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : α → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : ↑v ⊆ s'
hμv : μ (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s'
hv : (↑v).PairwiseDisjoint fun x ↦ closedBall x (r x)
p' : α
p'v : p' ∈ v
hp : (p', r p') ∈ t ∪ Finset.image (fun x ↦ (x, r x)) v
h'p : (p', r p') ∈ Finset.image (fun x ↦ (x, r x)) v
⊢ (p', r p').2 ∈ f (p', r p').1
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n

Tactic:
have isoF : Fu ≃ₗᵢ[𝕜] F := LinearIsometryEquiv.ulift 𝕜 F

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
s : Set E
t : Set F
x : E
N : ℕ∞ω
hg : ContDiffOn 𝕜 N g t
hf : ContDiffOn 𝕜 N f s
hn : ↑n ≤ N
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
Fu : Type (max uF uG) := ULift.{uG, uF} F
Gu : Type (max uF uG) := ULift.{uF, uG} G
isoF : Fu ≃ₗᵢ[𝕜] F
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
r : WithTop ℕ∞
s : Set E
x : E
ω : F → F [⋀^Fin n]→L[𝕜] G
f : E → F
t : Set F
hω : DifferentiableWithinAt 𝕜 ω t (f x)
hf : ContDiffWithinAt 𝕜 r f s x
hr : minSmoothness 𝕜 2 ≤ r
hs : UniqueDiffOn 𝕜 s
hxc : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hxs : x ∈ s
hst : MapsTo f s t
hdf : DifferentiableWithinAt 𝕜 f s x
hd2f : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ ω (f x)) s x

Tactic:
by exact hω.comp x hdf hst

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‖)
⊢ ‖(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:
congrm ‖?_‖

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‖)
⊢ (f' (x + h • v + (t * h) • w)) (h • w) - h • (f' x) w - h ^ 2 • (f'' v) w - (t * h ^ 2) • (f'' w) w =
    (f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (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 V₁ W₁ : E → E
s t : Set E
x✝ : E
hV✝ : V₁ =ᶠ[𝓝[s] x✝] V
hW✝ : W₁ =ᶠ[𝓝[s] x✝] W
ht : t ⊆ s
x : E
hV' : fderivWithin 𝕜 V₁ t x = fderivWithin 𝕜 V t x
hW' : fderivWithin 𝕜 W₁ t x = fderivWithin 𝕜 W t x
hV : V₁ x = V x
hW : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, hV', hW', hV, hW]

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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ¬(fderiv 𝕜 f x).IsInvertible
V : F → F
⊢ pullback 𝕜 f V x = 0

Tactic:
by
  simp [pullback, h]

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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
V : F → F
⊢ pullbackWithin 𝕜 f V univ = pullback 𝕜 f V

Tactic:
by
  ext x
  simp [pullbackWithin, pullback]

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

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
hsx : UniqueDiffWithinAt 𝕜 s x
n : ℕ
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 1 + 1) → E → E
hω : DifferentiableWithinAt 𝕜 ω s x
hV : ∀ (i : Fin (n + 1 + 1)), DifferentiableWithinAt 𝕜 (V i) s x
hcomm : Pairwise fun i j ↦ lieBracketWithin 𝕜 (V i) (V j) s x = 0
⊢ ((extDerivWithin ω s x) fun x_1 ↦ V x_1 x) =
    ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x ↦ (ω x) (i.removeNth fun x_1 ↦ V x_1 x)) s x) (V i x)

Tactic:
rw [extDerivWithin_apply_vectorField hω hV hsx, sub_eq_self]
    refine Fintype.sum_eq_zero _ fun i ↦ sum_eq_zero fun j hj ↦ ?_
    rw [hcomm (ne_of_lt <| by simpa using hj), (ω x).map_coord_zero 0] <;>
      simp

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

Goal state before:
pp: case e'_7
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 : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h ↦
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
TA2 :
  (fun h ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
⊢ (fun h ↦
      f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w) =
    fun x_1 ↦
    f (x + x_1 • (2 • v + w) + x_1 • w) - f (x + x_1 • (2 • v + w)) - x_1 • (f' x) w - x_1 ^ 2 • (f'' (2 • v + w)) w -
        (x_1 ^ 2 / 2) • (f'' w) w -
      (f (x + x_1 • (v + w) + x_1 • w) - f (x + x_1 • (v + w)) - x_1 • (f' x) w - x_1 ^ 2 • (f'' (v + w)) w -
        (x_1 ^ 2 / 2) • (f'' w) w)

Tactic:
ext h

Goal state after:
case e'_7
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 : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h ↦
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
TA2 :
  (fun h ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
h : ℝ
⊢ f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
      h ^ 2 • (f'' v) w =
    f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w -
      (f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w)
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case e'_7
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 : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
⊢ (fun h ↦ h ^ 2 • ((f'' w) v - (f'' v) w)) = fun x_1 ↦
    f (x + x_1 • (2 • v + 2 • w)) + f (x + x_1 • (v + w)) - f (x + x_1 • (2 • v + w)) - f (x + x_1 • (v + 2 • w)) -
        x_1 ^ 2 • (f'' v) w -
      (f (x + x_1 • (2 • w + 2 • v)) + f (x + x_1 • (w + v)) - f (x + x_1 • (2 • w + v)) - f (x + x_1 • (w + 2 • v)) -
        x_1 ^ 2 • (f'' w) v)

Tactic:
ext h

Goal state after:
case e'_7
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 : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
h : ℝ
⊢ h ^ 2 • ((f'' w) v - (f'' v) w) =
    f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w -
      (f (x + h • (2 • w + 2 • v)) + f (x + h • (w + v)) - f (x + h • (2 • w + v)) - f (x + h • (w + 2 • v)) -
        h ^ 2 • (f'' w) v)
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 : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun t ↦ x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)
m : E
⊢ interior s ∈ 𝓝 y

Tactic:
rw [mem_interior_iff_mem_nhds] at hy

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 : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : s ∈ 𝓝 y
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun t ↦ x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)
m : E
⊢ interior s ∈ 𝓝 y
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hn : n ≠ 0
h : ContDiffAt ℝ n (fun x ↦ ‖x‖) (0 • x)
this : Subsingleton E
⊢ ContDiffAt ℝ n (Function.const E ‖0‖) x

Tactic:
exact contDiffAt_const

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

Goal state before:
pp: 𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (fun x ↦
      match x with
      | (v, w) => v.1 - w.1) =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2]
    fun x ↦
    match x with
    | (v, w) => v - w

Tactic:
by
            simp [isBigO_of_le]

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

Goal state before:
pp: 𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (fun x ↦
      match x with
      | (v, w) => v.2 - w.2) =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2]
    fun x ↦
    match x with
    | (v, w) => v - w

Tactic:
by
            simp [isBigO_of_le]

Goal state after:
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
⊢ HasGradientAt f (∇ f x) x

Tactic:
by
  simpa [hasGradientAt_iff_hasFDerivAt] using h.hasFDerivAt

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

Goal state before:
pp: case refine_1
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
⊢ a ≤ c x

Tactic:
have := cmp x hx

Goal state after:
case refine_1
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ a ≤ c x
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case refine_2
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
⊢ c x ≤ id x

Tactic:
have := cmp x hx

Goal state after:
case refine_2
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ c x ≤ id x
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case refine_3
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
⊢ c x ∈ Ioi a

Tactic:
have := cmp x hx

Goal state after:
case refine_3
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : ℝ → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ x ∈ Ioo a b, ((fun x' ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ c x ∈ Ioi a