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

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 : ℕ
s : Set E
x : E
c : 𝕜
ω : E → E [⋀^Fin n]→L[𝕜] F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ extDerivWithin (c • ω) s x = c • extDerivWithin ω s x

Tactic:
by
  simp [extDerivWithin, fderivWithin_const_smul_field, hsx, alternatizeUncurryFin_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
g : E → F →L[𝕜] G
x : E
inst✝ : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) x

Tactic:
cases nonempty_fintype ι
  classical
  exact hf.hasFDerivAt.continuousAlternatingMapCompContinuousLinearMap hg.hasFDerivAt
    |>.differentiableAt

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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

Tactic:
by_cases h : (fderivWithin 𝕜 f s x).IsInvertible

Goal state after:
case pos
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x

case neg
𝕜 : 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
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : ¬(fderivWithin 𝕜 f s x).IsInvertible
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x
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 : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h ↦
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
⊢ (fun h ↦
      f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2

Tactic:
have TA2 := s_conv.taylor_approx_two_segment hf xs hx hvw hvww

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h ↦
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
TA2 :
  (fun h ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
⊢ (fun h ↦
      f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun t ↦ x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s
t : E → ℝ
ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C : ∀ (m : E), (f'' m) z = (f'' z) m
this✝ :
  (f'' z) z + t v • (f'' z) v + t w • ((f'' z) w + t v • (f'' v) w) =
    (f'' z) z + t w • (f'' z) w + t v • ((f'' z) v + t w • (f'' w) v)
this : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v
⊢ (f'' v) w = (f'' w) v

Tactic:
apply smul_right_injective F _ this

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun t ↦ x + 4 • (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + 4 • (z + t • m) ∈ interior s
t : E → ℝ
ts : ∀ (m : E), x + 4 • (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C : ∀ (m : E), (f'' m) z = (f'' z) m
this✝ :
  (f'' z) z + t v • (f'' z) v + t w • ((f'' z) w + t v • (f'' v) w) =
    (f'' z) z + t w • (f'' z) w + t v • ((f'' z) v + t w • (f'' w) v)
this : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v
⊢ t v * t w ≠ 0
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
· have : closedBall x r = closedBall x (δ / 2) := Subset.antisymm ht (by gcongr)
        rw [this] at tf
        exact ⟨δ / 2, ⟨half_pos δpos, tf⟩, ⟨half_pos δpos, half_lt_self δpos⟩⟩

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x y : F
h : HasGradientAt f f' x
⊢ (fderiv 𝕜 f x) y = ⟪f', y⟫

Tactic:
h.hasFDerivAt.fderiv,

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x y : F
h : HasGradientAt f f' x
⊢ ((toDual 𝕜 F) f') y = ⟪f', y⟫
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)
⊢ 𝓝[φ.toOpenPartialHomeomorph.symm.target ∩
        ↑φ.toOpenPartialHomeomorph.symm.symm ⁻¹'
          {φ.leftFun φ.pt} ×ˢ ((↑φ.toOpenPartialHomeomorph.symm ∘ fun x ↦ (φ.leftFun φ.pt, x)) ⁻¹' s)]
      φ.pt =
    𝓝[s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt}] φ.pt

Tactic:
conv_rhs =>
      rw [← φ.toOpenPartialHomeomorph.nhdsWithin_source_inter
        φ.pt_mem_toOpenPartialHomeomorph_source]

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)
⊢ 𝓝[φ.toOpenPartialHomeomorph.symm.target ∩
        ↑φ.toOpenPartialHomeomorph.symm.symm ⁻¹'
          {φ.leftFun φ.pt} ×ˢ ((↑φ.toOpenPartialHomeomorph.symm ∘ fun x ↦ (φ.leftFun φ.pt, x)) ⁻¹' s)]
      φ.pt =
    𝓝[φ.toOpenPartialHomeomorph.source ∩ (s ∩ φ.leftFun ⁻¹' {φ.leftFun φ.pt})] φ.pt
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
g f : 𝕜 → 𝕜
x : 𝕜
hg : ContDiffAt 𝕜 2 g (f x)
hf : ContDiffAt 𝕜 2 f x
⊢ iteratedDeriv 2 (g ∘ f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← derivWithin_univ]
  exact iteratedDerivWithin_comp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _)
    (mapsTo_univ _ _)

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

Goal state before:
pp: case intro
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ g, ∑ i, g i • Option.elim' φ' f' i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
refine ⟨Option.elim' Λ₀ Λ, ?_, ?_⟩

Goal state after:
case intro.refine_1
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∑ i, Option.elim' Λ₀ Λ i • Option.elim' φ' f' i = 0

case intro.refine_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst✝ : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val✝ : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ i, Option.elim' Λ₀ Λ i ≠ 0
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, 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:
by
  apply @lhopital_zero_nhdsNE _ _ _ f' _ g' <;>
    (first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds) <;> assumption

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), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
have M : MonotoneOn f (uIcc a b) := by
    apply monotoneOn_of_deriv_nonneg (convex_uIcc a b) hf
    · rw [uIcc, interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt
    · rw [uIcc, interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz
  simp only [Function.comp_apply]
  rcases le_or_gt a b with hab | hab
  · rw [integral_of_le hab, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonneg, integral_of_le, ← integral_Icc_eq_integral_Ioc]
    · apply M left_mem_uIcc right_mem_uIcc hab
    · rwa [uIcc_of_le hab] at hf
    · grind
    · grind
    · exact hab
  · rw [integral_of_ge hab.le, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonneg, integral_of_ge, ← integral_Icc_eq_integral_Ioc]
    · apply M right_mem_uIcc left_mem_uIcc hab.le
    · rwa [uIcc_of_ge hab.le] at hf
    · grind
    · grind
    · exact hab.le

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
_x : α
hx : _x ∈ Iio B
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico (c i) (b i)

Tactic:
simp only [mem_Ico, eventually_and]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : OpensMeasurableSpace α
b c : ι → α
B : α
hb : Tendsto b l (𝓝 B)
hc : Tendsto c l atBot
_x : α
hx : _x ∈ Iio B
⊢ (∀ᶠ (x : ι) in l, c x ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < b x
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst✝ : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
⊢ ∀ᶠ (i : ι) in l, _x ∈ Ico B (d i)

Tactic:
simp only [mem_Ico, eventually_and]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst✝ : NoMaxOrder α
_x : α
hx : _x ∈ Ici B
⊢ (∀ᶠ (x : ι) in l, B ≤ _x) ∧ ∀ᶠ (x : ι) in l, _x < d x
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), f' x ≤ 0
⊢ IntervalIntegrable (fun x ↦ (g ∘ f) x * f' x) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
by
  simpa [mul_comm] using! integrable_deriv_smul_comp_iff_of_deriv_nonpos hf hff' hf'

Goal state after:
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
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ

Tactic:
have A : ν.prod volume = (addHaarScalarFactor (ν.prod volume) μ) • μ :=
    isAddLeftInvariant_eq_smul _ _

Goal state after:
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
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x ↦ (B (f' x)) (g x)) μ
hfg' : Integrable (fun x ↦ (B (f x)) (g' x)) μ
hfg : Integrable (fun x ↦ (B (f x)) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ∫ (x : ℝ) in Iic a, f' x = f a - m

Tactic:
refine integral_Iic_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le)
    f'int hf
  exact (hderiv a self_mem_Iic).continuousAt.continuousWithinAt

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
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ μ (s ∩ t n) ≤ 0

Tactic:
exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)

Goal state after:
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
hne : x ≠ c
⊢ DifferentiableWithinAt ℂ f s x

Tactic:
· simpa only [DifferentiableWithinAt, HasFDerivWithinAt, hne.nhdsWithin_sdiff_singleton] using
      hd x ⟨hx, hne⟩

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable ((Ioi c).indicator fun x ↦ f (a * x)) volume ↔ IntegrableOn f (Ioi (a * c)) volume

Tactic:
← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi <| a * c)

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable ((Ioi c).indicator fun x ↦ f (a * x)) volume ↔ Integrable ((Ioi (a * c)).indicator f) volume
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
g : β → α
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : ℕ → β → α
h : HasProdLocallyUniformly f g
⊢ TendstoLocallyUniformly (fun x1 x2 ↦ ∏ i ∈ Finset.range x1, f i x2) g atTop

Tactic:
by
  simpa only [tendstoLocallyUniformlyOn_univ] using
    (h.hasProdLocallyUniformlyOn (s := .univ)).tendstoLocallyUniformlyOn_finsetRange

Goal state after:
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
hs : IsOpen[inst✝²] s
xs : x ∈ s
⊢ ∃ s, IsOpen[inst✝²] s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G

Tactic:
refine ⟨s, hs, xs, ?_⟩

Goal state after:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas M G
he' : e' ∈ maximalAtlas M G
x : H
hx : x ∈ (e.symm ≫ₕ e').source
f : OpenPartialHomeomorph M H := chartAt H (↑e.symm x)
s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source
hs : IsOpen[inst✝²] s
xs : x ∈ s
⊢ (e.symm ≫ₕ e').restr s ∈ G
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case refine_2
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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
t : Set E
g : E → E
⊢ ApproximatesLinearOn g A t (min δ δ'') → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t

Tactic:
htg

Goal state after:
case refine_2
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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
⊢ μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t