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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
set d := (s / ‖a.c j‖) • a.c j with hd

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
d : E := (s / ‖a.c j‖) • a.c j
hd : d = (s / ‖a.c j‖) • a.c j
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
Module: Mathlib.Analysis.Calculus.ContDiff.Polynomial

Goal state before:
pp: case add
R : Type u_1
𝕜 : Type u_2
inst✝² : CommSemiring R
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : Algebra R 𝕜
n : WithTop ℕ∞
f g : R[X]
fc : ContDiff 𝕜 n fun x ↦ (aeval x) f
gc : ContDiff 𝕜 n fun x ↦ (aeval x) g
⊢ ContDiff 𝕜 n fun x ↦ (aeval x) (f + g)

Tactic:
simpa using fc.add gc

Goal state after:
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
⊢ ‖if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i‖ ≤ 2

Tactic:
split_ifs with h

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ‖a.c i‖ ≤ 2
⊢ ‖a.c i‖ ≤ 2

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ¬‖a.c i‖ ≤ 2
⊢ ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
Module: Mathlib.Analysis.Calculus.Deriv.Pi

Goal state before:
pp: case e'_9
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ (if j = i then z else 0 j) = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Tactic:
split_ifs with h

Goal state after:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : j = i
⊢ z = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

case neg
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : ¬j = i
⊢ 0 j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j
Module: Mathlib.Analysis.Calculus.Deriv.Pi

Goal state before:
pp: case neg
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : ¬j = i
⊢ 0 j = (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜))) z j

Tactic:
simp [Pi.single_eq_of_ne h]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ μ (s \ ⋃ p ∈ u (n + 1), closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)

Tactic:
rw [u_succ]; exact (hF (u n) (Pu n)).2.2

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
| ↑N

Tactic:
rw [← add_zero (N : ℝ≥0∞)]

Goal state after:
α : 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
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
| ↑N + 0
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: case inr
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ≠ x₀
hx' : x₀ < x
⊢ sign (f x) = sign (x - x₀)

Tactic:
· rw [sign_pos (pos_of_slope_pos hx' hx₀ hx), sign_pos (sub_pos.mpr hx')]

Goal state after:
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
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n

Tactic:
let Gu : Type max uF uG := ULift.{uF, uG} G

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
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
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
V W : E → E
s : Set E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f s x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
⊢ (fderivWithin 𝕜 f s x) (lieBracketWithin 𝕜 V W s x) =
    (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 f s x) (W x)) s x) (V x) -
      (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 f s x) (V x)) s x) (W x)

Tactic:
have H₀ : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x :=
    (hf.fderivWithin_right hs (by decide) hxs).differentiableWithinAt one_ne_zero

Goal state after:
𝕜 : 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
V W : E → E
s : Set E
x : E
f : E → F
hf : ContDiffWithinAt 𝕜 2 f s x
hsymm : IsSymmSndFDerivWithinAt 𝕜 f s x
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hW : DifferentiableWithinAt 𝕜 W s x
hV : DifferentiableWithinAt 𝕜 V s x
H₀ : DifferentiableWithinAt 𝕜 (fderivWithin 𝕜 f s) s x
⊢ (fderivWithin 𝕜 f s x) (lieBracketWithin 𝕜 V W s x) =
    (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 f s x) (W x)) s x) (V x) -
      (fderivWithin 𝕜 (fun x ↦ (fderivWithin 𝕜 f s x) (V x)) s x) (W x)
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 (fun fg ↦ fg.1.compContinuousLinearMap fg.2)
    (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:
by
  rw [← hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff]
  have H₁ := ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap
    (fg.1.1, fun _ : ι ↦ fg.2)
  have H₂ := ((toContinuousMultilinearMapCLM 𝕜).hasStrictFDerivAt (x := fg.1))
  have H₃ := hasStrictFDerivAt_pi.mpr fun i : ι ↦ hasStrictFDerivAt_id (𝕜 := 𝕜) fg.2
  exact H₁.comp fg (H₂.prodMap fg 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
M : E ≃L[𝕜] F
x : E
hf : ↑M = fderiv 𝕜 f x
V : F → F
⊢ pullback 𝕜 f V x = M.symm (V (f x))

Tactic:
simp [pullback, ← hf]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
split_ifs with h

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
h : IsRCLikeNormedField 𝕜
⊢ n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
h : ¬IsRCLikeNormedField 𝕜
⊢ ω = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
⊢ ∃ n', (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
split_ifs with h

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ n', ↑m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then ↑m else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ n', ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ (fderiv ℝ (fun x ↦ ‖x‖) x) x = ‖x‖

Tactic:
rw [← h.lineDeriv_eq_fderiv, lineDeriv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x ↦ ‖x‖) x
⊢ deriv (fun t ↦ ‖x + t • x‖) 0 = ‖x‖
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
frechet : StrongDual 𝕜 F
⊢ HasFDerivAt f frechet x ↔ HasGradientAt f ((toDual 𝕜 F).symm frechet) x

Tactic:
by
  rw [hasGradientAt_iff_hasFDerivAt, (toDual 𝕜 F).apply_symm_apply frechet]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Complemented

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
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
⊢ (↥p × ↥q) ≃L[𝕜] E

Tactic:
by
  haveI := hp.completeSpace_coe; haveI := hq.completeSpace_coe
  refine (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous ?_
  exact (p.subtypeL.coprod q.subtypeL).continuous

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ ContDiffAt 𝕜 n (fun x ↦ ((⋯.implicitFunctionDataOfProdDomain if₂).implicitFunction (f u) x).2) u.1

Tactic:
set φ := (cdf.hasStrictFDerivAt pn).implicitFunctionDataOfProdDomain if₂

Goal state after:
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E₁ : Type u_2
inst✝⁸ : NormedAddCommGroup E₁
inst✝⁷ : NormedSpace 𝕜 E₁
inst✝⁶ : CompleteSpace E₁
E₂ : Type u_3
inst✝⁵ : NormedAddCommGroup E₂
inst✝⁴ : NormedSpace 𝕜 E₂
inst✝³ : CompleteSpace E₂
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
n : ℕ∞ω
cdf : ContDiffAt 𝕜 n f u
pn : n ≠ 0
if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
φ : ImplicitFunctionData 𝕜 (E₁ × E₂) F E₁ := ⋯.implicitFunctionDataOfProdDomain if₂
⊢ ContDiffAt 𝕜 n (fun x ↦ (φ.implicitFunction (f u) x).2) u.1
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : 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
g : E → F
f : 𝕜 → E
s : Set 𝕜
t : Set E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
hi : ↑i ≤ n
⊢ iteratedDerivWithin i (g ∘ f) s x =
    ∑ c, (iteratedFDerivWithin 𝕜 c.length g t (f x)) fun j ↦ iteratedDerivWithin (c.partSize j) f s x

Tactic:
by
  simp only [iteratedDerivWithin, iteratedFDerivWithin_comp hg hf ht hs hx hst hi]
  simp [FormalMultilinearSeries.taylorComp, ftaylorSeriesWithin,
    OrderedFinpartition.applyOrderedFinpartition_apply, comp_def]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
s : Set E
H : φ.implicitFunction (φ.leftFun φ.pt) = ↑φ.toOpenPartialHomeomorph.symm ∘ fun x ↦ (φ.leftFun φ.pt, x)
⊢ map (φ.implicitFunction (φ.leftFun φ.pt)) (𝓝[φ.implicitFunction (φ.leftFun φ.pt) ⁻¹' s] φ.rightFun φ.pt) =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt

Tactic:
H,

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
s : Set E
H : φ.implicitFunction (φ.leftFun φ.pt) = ↑φ.toOpenPartialHomeomorph.symm ∘ fun x ↦ (φ.leftFun φ.pt, x)
⊢ map (↑φ.toOpenPartialHomeomorph.symm ∘ fun x ↦ (φ.leftFun φ.pt, x))
      (𝓝[(↑φ.toOpenPartialHomeomorph.symm ∘ fun x ↦ (φ.leftFun φ.pt, x)) ⁻¹' s] φ.rightFun φ.pt) =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
K : HasDerivWithinAt f 0 (s ∩ Ioo p x) x
K' : HasDerivWithinAt f (f' x) (s ∩ Ioo p x) x
J1 : (s ∩ Ioo p x) \ {x} = s ∩ Ioo p x
⊢ 𝓝[s ∩ Ioo p x] x = 𝓝[s ∩ Iio x] x

Tactic:
simp [nhdsWithin_inter, nhdsWithin_Ioo_eq_nhdsLT px]

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‖}
x : E
xs : x ∈ s
z : ↑s
zT : z ∈ T
hz : f' x ∈ ball (f' ↑z) ↑(r (f' ↑z))
ε : ℝ
εpos : 0 < ε
hε : ‖f' x - f' ↑z‖ + ε ≤ ↑(r (f' ↑z))
δ : ℝ
δpos : 0 < δ
hδ : ball x δ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}
n : ℕ
hn : u n < δ
y : E
hy : y ∈ s ∩ ball x (u n)
⊢ y ∈ s ∩ ball x δ

Tactic:
exact inter_subset_inter_right _ (ball_subset_ball hn.le) hy

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

Goal state before:
pp: 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), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) volume
this : Fact (f x ∈ J)
⊢ HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x

Tactic:
have : HasDerivWithinAt (fun u ↦ ∫ x in f a..u, g x) (g (f x)) J (f x) :=
      intervalIntegral.integral_hasDerivWithinAt_right h2g h3g (hg_cont (f x) h2x)

Goal state after:
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), HasDerivWithinAt f (f' x) (Ioi x) x
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
x : ℝ
hx : x ∈ Ioo (min a b) (max a b)
c : ℝ
hc : c ∈ Ioo (min a b) x
d : ℝ
hd : d ∈ Ioo x (max a b)
cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b)
J : Set ℝ := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
hg_cont : ContinuousOn g J
hJ : f '' [[c, d]] = J
h2x : f x ∈ J
h2g : IntervalIntegrable g volume (f a) (f x)
h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) volume
this✝ : Fact (f x ∈ J)
this : HasDerivWithinAt (fun u ↦ ∫ (x : ℝ) in f a..u, g x) (g (f x)) J (f x)
⊢ HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
⊢ ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
have : ∫⁻ x in a, ENNReal.ofReal (f' x) * u (f x) = 0 :=
      setLIntegral_measure_zero a _ (a_count.measure_zero volume)

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
this : ∫⁻ (x : ℝ) in a, ENNReal.ofReal (f' x) * u (f x) = 0
⊢ ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)