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

Goal state before:
pp: case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
⊢ c ∈ Ioo a b

Tactic:
rcases cmem.2.eq_or_lt' with (rfl | hcb)

Goal state after:
case inr.inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ b ∈ Ioo a b

case inr.inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
hcb : c < b
⊢ c ∈ Ioo a b
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_4
α : 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)
⊢ μ (s \ ⋃ p ∈ t ∪ Finset.image (fun x ↦ (x, r x)) v, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ s'

Tactic:
· convert! hμv using 2
      rw [Finset.set_biUnion_union, ← sdiff_sdiff, Finset.set_biUnion_finset_image]

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
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (⇑L ∘ f) s x‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
by
  have h := L.norm_compContinuousMultilinearMap_le (iteratedFDerivWithin 𝕜 n f s x)
  rwa [← L.iteratedFDerivWithin_comp_left hf hs hx hn] at h

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

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

Tactic:
intro x hx
    cases hx with
    | inl hx =>
      rw [r_t0 x hx]
      exact (hr0 _ hx).1
    | inr hx =>
      have h'x : x ∈ s' := by
        simp only [mem_iUnion, mem_image] at hx
        rcases hx with ⟨i, y, _, rfl⟩
        exact y.2
      simp only [r, if_pos h'x, (hr1 x h'x).1.1]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
hf : DifferentiableWithinAt 𝕜 f univ x
⊢ lieBracket 𝕜 V (fun y ↦ f y • W y) x = (fderiv 𝕜 f x) (V x) • W x + f x • lieBracket 𝕜 V W x

Tactic:
← lieBracketWithin_univ,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
hf : DifferentiableWithinAt 𝕜 f univ x
⊢ lieBracketWithin 𝕜 V (fun y ↦ f y • W y) univ x = (fderiv 𝕜 f x) (V x) • W x + f x • lieBracketWithin 𝕜 V W univ x
Module: Mathlib.Analysis.Calculus.VectorField

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

Tactic:
← lieBracketWithin_univ,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
h : s ∈ 𝓝 x
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W univ x
Module: Mathlib.Analysis.Calculus.VectorField

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

Tactic:
← lieBracketWithin_univ,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracket 𝕜 V W x
Module: Mathlib.Analysis.Calculus.VectorField

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

Tactic:
← lieBracketWithin_univ,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracketWithin 𝕜 V₁ W₁ univ x = lieBracketWithin 𝕜 V W univ x
Module: Mathlib.Analysis.Calculus.VectorField

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

Tactic:
hWy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : E
hVy : V₁ =ᶠ[𝓝 y] V
hWy : W₁ =ᶠ[𝓝 y] W
⊢ lieBracket 𝕜 V₁ W₁ y = lieBracket 𝕜 V W y
Module: Mathlib.Analysis.Calculus.DifferentialForm.VectorField

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
n : ℕ
x : E
ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F
V : Fin (n + 2) → E → E
hω : DifferentiableWithinAt 𝕜 ω Set.univ x
hV : ∀ (i : Fin (n + 2)), DifferentiableWithinAt 𝕜 (V i) Set.univ x
⊢ ((extDerivWithin ω Set.univ x) fun x_1 ↦ V x_1 x) =
    ∑ x_1, (-1) ^ ↑x_1 • (fderivWithin 𝕜 (fun x ↦ (ω x) (x_1.removeNth fun x_2 ↦ V x_2 x)) Set.univ x) (V x_1 x) -
      ∑ x_1,
        ∑ x_2 ≥ x_1,
          (-1) ^ (↑x_1 + ↑x_2) •
            (ω x)
              (Matrix.vecCons (lieBracketWithin 𝕜 (V x_1.castSucc) (V x_2.succ) Set.univ x)
                (x_2.removeNth (x_1.castSucc.removeNth fun x_3 ↦ V x_3 x)))

Tactic:
exact extDerivWithin_apply_vectorField hω hV (by simp)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
h : HasLineDerivWithinAt 𝕜 f f' univ x v
⊢ HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)

Tactic:
exact HasLineDerivWithinAt.smul h c

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 : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
m : E
this : x + 4 • (z + 0 • m) = y
⊢ Tendsto (fun t ↦ t • m) (𝓝 0) (𝓝 (0 • m))

Tactic:
exact continuousAt_id.smul continuousAt_const

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
f : E → ℝ
f' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ : Module.Dual ℝ ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
x : E
⊢ Λ (f' x) = f' x * Λ 1

Tactic:
simpa only [mul_one, smul_eq_mul] using Λ.map_smul (f' x) 1

Goal state after:
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
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
x : ℝ
hx : x ∈ Ioo a b
⊢ ∃ c ∈ Ioo a x, (f x - 0) * g' c = (g x - 0) * f' c

Tactic:
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)

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ ∀ x ∈ Ioo 0 a'⁻¹, g' x⁻¹ * -(x ^ 2)⁻¹ ≠ 0

Tactic:
intro x hx
      refine mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)
      exact hg' _ (fact2 x hx)

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x ↦ f x / g x) atBot l

Tactic:
rw [neg_Iio] at hdnf hdng

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x ↦ f x / g x) atBot l
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|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
r : ℝ
hr : r ∈ Ioi 0
⊢ μ (cthickening r (⇑A '' closedBall 0 1)) = μ (closedBall 0 r + ⇑A '' closedBall 0 1)

Tactic:
← HC.add_closedBall_zero (le_of_lt hr),

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|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
r : ℝ
hr : r ∈ Ioi 0
⊢ μ (⇑A '' closedBall 0 1 + closedBall 0 r) = μ (closedBall 0 r + ⇑A '' closedBall 0 1)
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case pos
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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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 f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)

Tactic:
have a_s : a ⊆ s := by rw [← h_union]; exact subset_union_left

Goal state after:
case pos
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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn g (f '' s) volume
H' : IntegrableOn (fun x ↦ f' x • g (f x)) s volume
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
a_s : a ⊆ s
⊢ ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)
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|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ ∃ ε, μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1) ∧ 0 < ε

Tactic:
have L2 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (d * μ (closedBall 0 1))) := by
      convert! L1
      exact (addHaar_image_continuousLinearMap _ _ _).symm

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|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε ↦ μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L2 : Tendsto (fun ε ↦ μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (d * μ (closedBall 0 1)))
⊢ ∃ ε, μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1) ∧ 0 < ε
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
φ : ℕ → Set α
hφ : AECover μ atTop φ
hmono : Monotone φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
F : ℕ → α → ℝ≥0∞ := fun n ↦ (φ n).indicator f
key₁ : ∀ (n : ℕ), AEMeasurable (F n) μ
x : α
_i _j : ℕ
hij : _i ≤ _j
⊢ (fun n ↦ F n x) _i ≤ (fun n ↦ F n x) _j

Tactic:
by
    dsimp [F]; grw [hmono hij]

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

Goal state before:
pp: a b : ℝ
f f' g : ℝ → ℝ
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 : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
simpa [mul_comm] using! integral_deriv_smul_comp_of_deriv_nonneg hf hff' hf'

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f b) (f a), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ ∫ (t : ℝ) in Ioo a b, f' t • g (f t) = -∫ (u : ℝ) in f '' Ioo a b, g u

Tactic:
integral_image_eq_integral_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f b) (f a), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ ∫ (t : ℝ) in Ioo a b, f' t • g (f t) = -∫ (x : ℝ) in Ioo a b, -f' x • g (f x)

case hf'
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f b) (f a), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

case hf
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A : ∫ (u : ℝ) in Icc (f b) (f a), g u = ∫ (u : ℝ) in f '' Ioo a b, g u
⊢ AntitoneOn f (Ioo a b)
Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x ↦ (B (f x)) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y ↦ (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y ↦ (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y ↦ (B (f (x, y))) (g (x, y))) volume
t : ℝ
ht : t ∈ tsupport fun x_1 ↦ g (x, x_1)
this : (x, t) ∈ tsupport g
⊢ HasDerivAt (fun x_1 ↦ f (x, x_1)) (f' (x, t)) t

Tactic:
convert! (hf (x, t) this).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t)))
        (by simp) <;> simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := ⇑I ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
⊢ ‖∫ (x : ℝ) in Iic x, deriv f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ

Tactic:
exact enorm_integral_le_lintegral_enorm _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
ha : 0 < a
⊢ IntegrableOn g (Ioi (log a)) volume ↔ IntegrableOn (fun x ↦ x⁻¹ • g (log x)) (Ioi a) volume

Tactic:
simpa  using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a : ℝ
ha : 0 < a
⊢ IntegrableOn g (Ioi (log a)) volume ↔ IntegrableOn (fun x ↦ x⁻¹ • g (log x)) (Ioi a) volume
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∀ (i : ℕ), MeasurableSet (closedBall 0 R ∩ t i)

Tactic:
intro n
        exact measurableSet_closedBall.inter (t_meas n)

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

Goal state before:
pp: case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∀ (i : ℕ), MeasurableSet (closedBall 0 R ∩ t i)

Tactic:
· intro n
        exact measurableSet_closedBall.inter (t_meas n)

Goal state after: