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
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r j / 4 ≤ 1

Tactic:
by linarith only [C]

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ IsMinOn f (Ioi a) b

Tactic:
refine isMinOn_Ioi_of_anti_mono ?_ ?_

Goal state after:
case refine_1
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ AntitoneOn f (Ioc a b)

case refine_2
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap

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✝⁷ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)
⊢ HasStrictFDerivAt (fun fg ↦ fg.1.compContinuousLinearMap fg.2)
    (compContinuousLinearMapL fg.2 ∘SL
        ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i) +
      fg.1.fderivCompContinuousLinearMap fg.2 ∘SL
        ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i))
    fg

Tactic:
have := (compContinuousLinearMapContinuousMultilinear 𝕜 F G H).hasStrictFDerivAt fg.2
  convert! this.comp fg hasStrictFDerivAt_snd |>.clm_apply hasStrictFDerivAt_fst
  ext <;> simp [fderivCompContinuousLinearMap]

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
W : E → E
⊢ lieBracket 𝕜 0 W = 0

Tactic:
simp [← lieBracketWithin_univ]

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
W : E → E
⊢ lieBracket 𝕜 W 0 = 0

Tactic:
simp [← lieBracketWithin_univ]

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
⊢ (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:
have aux₁ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x) :
      DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x)) s x :=
    have := hV.fderivWithin_right_apply (hU.of_le one_le_two) hs le_rfl hx
    this.differentiableWithinAt one_ne_zero

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
⊢ (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))))
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
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
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x

Tactic:
rcases exists_continuousLinearEquiv_fderivWithin_symm_eq hf hf' hs hx
    with ⟨M, -, M_symm_smooth, hM, -⟩

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
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
⊢ DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case h₂
α : 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'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') α := ⋯
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 : α → ℝ := ⋯
r_t0 : ∀ x ∈ t0, r x = r0 x
A : ∑' (x : ↑t0), μ (closedBall (↑x) (r ↑x)) ≤ μ s + ε / 2
B : ∀ (i : Fin N), ∑' (x : ↑(Subtype.val '' S i)), μ (closedBall (↑x) (r ↑x)) ≤ ε / 2 / ↑N
⊢ ∑ i, ε / 2 / ↑N ≤ ε / 2

Tactic:
simp only [Finset.card_fin, Finset.sum_const, nsmul_eq_mul, ENNReal.mul_div_le]

Goal state after:
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 (fun x ↦ ‖x‖) x

Tactic:
rw [eq_const_of_subsingleton (‖·‖) 0]

Goal state after:
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
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace 𝕜
z₀ : 𝕜
R R₁ : 𝕜 → 𝕜
hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z
k : ℕ
IH :
  ∀ {t : ℕ},
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t)! / ↑t ! * R₁ z + (z - z₀) * R₂ z)
t : ℕ
hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + 1 + t) * R₁ z
R₂ : 𝕜 → 𝕜
hR₂ : ∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z
hR₂_eq : ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z)
R₂' : 𝕜 → 𝕜 := fun z ↦ (↑t + 1) * R₂ z + (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
z : 𝕜
this : ↑t + 1 ≠ 0
⊢ (↑t + 1) * (z - z₀) ^ t * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z) +
      (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z)) =
    (z - z₀) ^ t * (↑(k + 1 + t)! / ↑t ! * R₁ z + (z - z₀) * R₂' z)

Tactic:
have : ((t + 1)! : 𝕜) = (t + 1) * t ! := by simp [Nat.factorial_succ]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace 𝕜
z₀ : 𝕜
R R₁ : 𝕜 → 𝕜
hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z
k : ℕ
IH :
  ∀ {t : ℕ},
    (∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) →
      ∃ R₂,
        (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧
          ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t)! / ↑t ! * R₁ z + (z - z₀) * R₂ z)
t : ℕ
hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + 1 + t) * R₁ z
R₂ : 𝕜 → 𝕜
hR₂ : ∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z
hR₂_eq : ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z)
R₂' : 𝕜 → 𝕜 := fun z ↦ (↑t + 1) * R₂ z + (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z))
z : 𝕜
this✝ : ↑t + 1 ≠ 0
this : ↑(t + 1)! = (↑t + 1) * ↑t !
⊢ (↑t + 1) * (z - z₀) ^ t * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ z + (z - z₀) * R₂ z) +
      (z - z₀) ^ (t + 1) * (↑(k + (t + 1))! / ↑(t + 1)! * deriv R₁ z + (R₂ z + (z - z₀) * deriv R₂ z)) =
    (z - z₀) ^ t * (↑(k + 1 + t)! / ↑t ! * R₁ z + (z - z₀) * R₂' z)
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
x : G
⊢ φ.rightDeriv ((fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) x) = x

Tactic:
exact φ.fderiv_implicitFunction_apply_eq_iff.mp rfl |>.right

Goal state after:
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
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto g (𝓝[>] a) (𝓝 0)

Tactic:
rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]

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
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto g (𝓝[Ioo a b] a) (𝓝 (g a))
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case refine_2
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto g (𝓝[>] a) (𝓝 0)

Tactic:
rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]

Goal state after:
case refine_2
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto g (𝓝[Ioo a b] a) (𝓝 (g a))
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[<] b) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] b) l

Tactic:
have hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx =>
    (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)
  have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
  exact HasDerivAt.lhopital_zero_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfb hgb hdiv

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) atBot l
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
have hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x := fun x hx =>
    (hdf x hx).differentiableAt (Iio_mem_nhds hx)
  have hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
  exact HasDerivAt.lhopital_zero_atBot_on_Iio (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfbot hgbot hdiv

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

Goal state before:
pp: case hf'
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
⊢ DifferentiableOn ℝ f (interior [[a, b]])

Tactic:
rw [uIcc, interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

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

Goal state before:
pp: case hf'
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
⊢ DifferentiableOn ℝ f (interior [[a, b]])

Tactic:
rw [uIcc, interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s) x} ∈ 𝓝 0

Tactic:
have : Iio (.mk ε εpos.le) ∈ 𝓝 (0 : ℝ≥0) := by apply Iio_mem_nhds; exact εpos

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
⊢ {x | (fun δ ↦ ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s) x} ∈ 𝓝 0
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
⊢ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = {f x} + r • ⇑A '' closedBall 0 1 + r • closedBall 0 ε

Tactic:
add_comm {f x},

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
⊢ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = r • ⇑A '' closedBall 0 1 + {f x} + r • closedBall 0 ε
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case hfi
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ Integrable (fun x ↦ ‖f x‖) (volume.restrict (Ioc (a i) (b i)))

pp: case hs
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ Ioc (a i) (b i) ∩ Ioc a₀ b₀ ⊆ Ioc (a i) (b i)

Tactic:
· exact (hfi i).norm

Goal state after:
case hs
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ Ioc (a i) (b i) ∩ Ioc a₀ b₀ ⊆ Ioc (a i) (b i)
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 : AntitoneOn f s
u : ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)

Tactic:
let n : ℝ → ℝ := (fun x ↦ -x)

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun x ↦ -x
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) s volume

Tactic:
let n : ℝ → ℝ := (fun x ↦ -x)

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun x ↦ -x
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) s volume
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, -f' x • g (f x)

Tactic:
let n : ℝ → ℝ := (fun x ↦ -x)

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun x ↦ -x
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, -f' x • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
⊢ atTop.limUnder (⇑F ∘ f) = F 0

Tactic:
apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A

Goal state after:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
fint : IntegrableOn f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x
Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume
F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume
A : Tendsto (⇑F ∘ f) atTop (𝓝 (atTop.limUnder (⇑F ∘ f)))
this : IntegrableAtFilter (⇑F ∘ f) atTop volume
⊢ ∀ s ∈ atTop, volume s = ∞