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
⊢ ∀ t ∈ Icc 0 1, HasDerivWithinAt g (g' t) (Icc 0 1) t

Tactic:
intro t

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
t : ℝ
⊢ t ∈ Icc 0 1 → HasDerivWithinAt g (g' t) (Icc 0 1) t
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 ∈ Ico 0 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2

Tactic:
intro t

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 : ℝ
⊢ t ∈ Ico 0 1 → ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 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
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 (fun y ↦ f y • V y) W s x = -(fderivWithin 𝕜 f s x) (W x) • V x + f x • lieBracketWithin 𝕜 V W s x

Tactic:
by
  rw [lieBracketWithin_swap, Pi.neg_apply, lieBracketWithin_smul_right hf hV hs,
    lieBracketWithin_swap, add_comm]
  simp

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
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) - (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:
fderivWithin_fun_sub (hs x hx) (aux₁ hV hW) (aux₁ hW hV)

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))))
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: case hx
𝕜 : 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
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))

Tactic:
have hMx : M x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx hM

Goal state after:
case hx
𝕜 : 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
inst✝ : CompleteSpace E
f : E → F
V : F → F
s : Set E
t : Set F
x : E
hV : DifferentiableWithinAt 𝕜 V t (f x)
hf : ContDiffWithinAt 𝕜 2 f s x
hf' : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
this : DifferentiableWithinAt 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
hMx : ↑(M x) = fderivWithin 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x).inverse (V (f x)) = ↑(M x).symm (V (f x))
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
k : ℕ
⊢ y k ∈ u → IsSymmSndFDerivWithinAt 𝕜 f s (y k)

Tactic:
hk

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
k : ℕ
hk : y k ∈ u
⊢ IsSymmSndFDerivWithinAt 𝕜 f s (y k)
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t < 0
h : HasFDerivAt (fun x ↦ ‖x‖) f x
⊢ HasFDerivAt (fun x ↦ ‖x‖) (-f) (t • x)

Tactic:
by
  simpa [ht] using h.hasFDerivAt_norm_smul ht.ne

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
k : ℕ
⊢ y k ∈ u → y k ∈ s ∩ u

Tactic:
hk

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
k : ℕ
hk : y k ∈ u
⊢ y k ∈ s ∩ u
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
C :
  ∀ (v w : E),
    Tendsto (fun k ↦ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) v) w) atTop
      (𝓝 (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w))
v w : E
k : ℕ
⊢ IsSymmSndFDerivWithinAt 𝕜 f s (y k) →
    ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) w) v

Tactic:
hk

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 ↑2 ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
C :
  ∀ (v w : E),
    Tendsto (fun k ↦ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) v) w) atTop
      (𝓝 (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w))
v w : E
k : ℕ
hk : IsSymmSndFDerivWithinAt 𝕜 f s (y k)
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) w) v
Module: Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
hs : IsOpen s
⊢ Set.EqOn (deriv^[k] fun y ↦ y ^ m) (fun y ↦ (∏ i ∈ Finset.range k, (↑m - ↑i)) * y ^ (m - ↑k)) s

Tactic:
intro t

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
hs : IsOpen s
t : 𝕜
⊢ t ∈ s → deriv^[k] (fun y ↦ y ^ m) t = (fun y ↦ (∏ i ∈ Finset.range k, (↑m - ↑i)) * y ^ (m - ↑k)) t
Module: Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
k : ℕ
hs : IsOpen s
⊢ Set.EqOn (deriv^[k] fun y ↦ 1 / y) (fun y ↦ (-1) ^ k * ↑k ! * y ^ (-1 - ↑k)) s

Tactic:
intro t

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
k : ℕ
hs : IsOpen s
t : 𝕜
⊢ t ∈ s → deriv^[k] (fun y ↦ 1 / y) t = (fun y ↦ (-1) ^ k * ↑k ! * y ^ (-1 - ↑k)) t
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: 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
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[>] a) l

Tactic:
have sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b := fun x hx =>
    Ioo_subset_Ioo (le_refl a) (le_of_lt hx.2)
  have hg : ∀ x ∈ Ioo a b, g x ≠ 0 := by
    intro x hx h
    have : Tendsto g (𝓝[<] x) (𝓝 0) := by
      rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]
      exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
    obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0 :=
      exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy
    exact hg' y (sub x hx hyx) hy
  have : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, f x * g' c = g x * f' c := by
    intro x hx
    rw [← sub_zero (f x), ← sub_zero (g x)]
    exact exists_ratio_hasDerivAt_eq_ratio_slope' g g' hx.1 f f' (fun y hy => hgg' y <| sub x hx hy)
      (fun y hy => hff' y <| sub x hx hy) hga hfa
      (tendsto_nhdsWithin_of_tendsto_nhds (hgg' x hx).continuousAt.tendsto)
      (tendsto_nhdsWithin_of_tendsto_nhds (hff' x hx).continuousAt.tendsto)
  choose! c hc using this
  have : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x := by grind
  have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x := fun x hx ↦ (hc x hx).1
  rw [← nhdsWithin_Ioo_eq_nhdsGT hab]
  apply tendsto_nhdsWithin_congr this
  apply hdiv.comp
  refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
    (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
      (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) ?_ ?_) ?_
  all_goals
    apply eventually_nhdsWithin_of_forall
    intro x hx
    have := cmp x hx
    simp
    linarith [this]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case hf'_nonneg
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ ∀ x ∈ interior [[a, b]], 0 ≤ deriv f x

Tactic:
rw [uIcc, interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
L1 : Tendsto (fun k ↦ ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖) atTop (𝓝 ‖f y - f x - (f' ↑↑z) (y - x)‖)
L2 : Tendsto (fun k ↦ ↑(r (f' ↑↑z)) * ‖y - a k‖) atTop (𝓝 (↑(r (f' ↑↑z)) * ‖y - x‖))
L : Tendsto (fun k ↦ dist y (a k)) atTop (𝓝 (dist y x))
k : ℕ
⊢ dist y (a k) < u n → ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - a k‖

Tactic:
hk

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
n : ℕ
z : ↑T
x : E
xs : x ∈ s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
y : E
hy : y ∈ s ∩ ball x (u n)
a : ℕ → E
aM : ∀ (k : ℕ), a k ∈ M n z
a_lim : Tendsto a atTop (𝓝 x)
L1 : Tendsto (fun k ↦ ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖) atTop (𝓝 ‖f y - f x - (f' ↑↑z) (y - x)‖)
L2 : Tendsto (fun k ↦ ↑(r (f' ↑↑z)) * ‖y - a k‖) atTop (𝓝 (↑(r (f' ↑↑z)) * ‖y - x‖))
L : Tendsto (fun k ↦ dist y (a k)) atTop (𝓝 (dist y x))
k : ℕ
hk : dist y (a k) < u n
⊢ ‖f y - f (a k) - (f' ↑↑z) (y - a k)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - a k‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case inl.hab
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : a ≤ b
⊢ a ≤ b

Tactic:
exact hab

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case hf'_nonpos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
⊢ ∀ x ∈ interior [[a, b]], deriv f x ≤ 0

Tactic:
rw [uIcc, interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz

Goal state after: