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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
G : Type u_5
H : Type u_6
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
f : E → G [⋀^ι]→L[𝕜] H
f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H
x : E
inst✝ : Finite ι
val✝ : Fintype ι
⊢ HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) (toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x
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
s : Set E
x : E
inst✝ : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) s x

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
𝕜 : 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
s : Set E
x : E
inst✝ : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
val✝ : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) s x
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 ι

Goal state after:
case intro
𝕜 : 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
val✝ : Fintype ι
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x).compContinuousLinearMap (g x)) x
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
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst✝ : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (f x) fun x_1 ↦ g x_1 x) s x

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
s : Set E
x : E
inst✝ : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
val✝ : Fintype ι
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ (f x) fun x_1 ↦ g x_1 x) s x
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
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst✝ : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x) fun x_1 ↦ g x_1 x) x

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : E → F [⋀^ι]→L[𝕜] G
g : ι → E → F
x : E
inst✝ : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
val✝ : Fintype ι
⊢ DifferentiableAt 𝕜 (fun x ↦ (f x) fun x_1 ↦ g x_1 x) x
Module: Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Finite ι
f : E [⋀^ι]→L[𝕜] F
⊢ Differentiable 𝕜 ⇑f

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Finite ι
f : E [⋀^ι]→L[𝕜] F
val✝ : Fintype ι
⊢ Differentiable 𝕜 ⇑f
Module: Mathlib.Analysis.Calculus.FDeriv.Partial

Goal state before:

Tactic:
fun (v, w) => f v.1 v.2 - f v.1 w.2 - ↿f₂ u (v.2 - w.2)
          _ =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v.2 - w.2 : _ → E₂) := by
            have h := (tendsto_fst.comp <| tendsto_fst.comp tendsto_fst).prodMk <|
              tendsto_snd (f := (𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)) (g := 𝓝 u.2)
            let : NormedSpace ℝ E₂ := RestrictScalars.normedSpace ℝ 𝕜 E₂
            apply isLittleO_sub_sub_fderiv (f' := fun (v, w) y => f₂ v.1 y)
              (tendsto_snd.comp tendsto_fst) (tendsto_snd.comp tendsto_snd)
            · simpa using! h.eventually df₂
            · simpa using! cf₂.comp h
          _ =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v - w : _ → E₁ × E₂) := by
            simp [isBigO_of_le]

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

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

Tactic:
by
  obtain rfl | ht := eq_or_ne t 0
  · suffices Subsingleton E from (hasFDerivAt_of_subsingleton _ _).differentiableAt
    rw [zero_smul] at h
    by_contra!
    exact not_differentiableAt_norm_zero E h
  · exact differentiableAt_norm_smul ht |>.2 h

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : 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 : 𝕜
⊢ iteratedDeriv (k + 1) R z = (z - z₀) ^ t * (↑(k + 1 + t)! / ↑t ! * R₁ z + (z - z₀) * R₂' z)

Tactic:
calc iteratedDeriv (k + 1) R z
      _ = deriv (fun w ↦ (w - z₀) ^ (t + 1)
          * (↑(k + (t + 1))! / ↑(t + 1)! * R₁ w + (w - z₀) * R₂ w)) z := by
        rw [iteratedDeriv_succ, funext hR₂_eq]
      _ = (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)) := by
        have hsub : HasDerivAt (· - z₀) 1 z := (hasDerivAt_id z).sub_const z₀
        simpa using! ((hsub.fun_pow (t + 1)).mul
          (((hf1 z).differentiableAt.hasDerivAt.const_mul ((k + (t + 1))! / (t + 1)! : 𝕜)).add
            (hsub.mul (hR₂ z).differentiableAt.hasDerivAt))).deriv
      _ = (z - z₀) ^ t * ((k + 1 + t)! / t ! * R₁ z + (z - z₀) * R₂' z) := by
        have : (t : 𝕜) + 1 ≠ 0 := mod_cast t.succ_ne_zero
        have : ((t + 1)! : 𝕜) = (t + 1) * t ! := by simp [Nat.factorial_succ]
        grind

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

Goal state before:
pp: case refine_1
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
⊢ (Λ 1, Λ₀) ≠ 0

Tactic:
contrapose hΛ

Goal state after:
case refine_1
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 ℝ ℝ
Λ₀ : ℝ
hfΛ : ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
hΛ : (Λ 1, Λ₀) = 0
⊢ (Λ, Λ₀) = 0
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
ι : 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₀
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')

Tactic:
cases nonempty_fintype ι

Goal state after:
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 ι
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: a b : ℝ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x ↦ u x • v' x + u' x • v x) volume a b

Tactic:
exact (hv'.continuousOn_smul hu).add (hu'.smul_continuousOn hv)

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

Goal state before:
pp: a : ℝ
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[<] a) l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hal : l ∈ Iio a
hl : Ioo l a ⊆ s
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] a) l✝

Tactic:
refine lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv <;> grind

Goal state after:
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ c ⊆ a ∪ (b ∪ c)

Tactic:
exact subset_union_right.trans subset_union_right

Goal state after:
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hf' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal |f' x| * u (f x)

Tactic:
abs_of_nonneg (deriv_c x hx)

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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hf' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal (f' x) * u (f x)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr
E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : ↑T
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
⊢ x ∈ ⋃ n, (fun q ↦ K (F q).1 (F q).2.1 (F q).2.2) n

Tactic:
obtain ⟨q, hq⟩ : ∃ q, F q = (n, z, p) := hF _

Goal state after:
case inr
E : Type u_1
F✝ : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : SecondCountableTopology F✝
f : E → F✝
s : Set E
f' : E → E →L[ℝ] F✝
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F✝) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0
hs : s.Nonempty
T : Set ↑s
T_count : T.Countable
hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))
u : ℕ → ℝ
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → ↑T → Set E :=
  fun n z ↦ {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z
closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → ↑T → ℕ → Set E :=
  fun n z p ↦ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))
K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × ↑T × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : ↑T
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ ⋃ n, (fun q ↦ K (F q).1 (F q).2.1 (F q).2.2) n
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 : MonotoneOn f s
g : ℝ → F
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
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
⊢ c ⊆ a ∪ (b ∪ c)

Tactic:
exact subset_union_right.trans subset_union_right

Goal state after:
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 : MonotoneOn f s
g : ℝ → F
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
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ |f' x| • g (f x) = f' x • g (f x)

Tactic:
abs_of_nonneg (deriv_c x hx)

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 : MonotoneOn f s
g : ℝ → F
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
I : IntegrableOn (fun x ↦ f' x • g (f x)) s volume ↔ IntegrableOn (fun x ↦ f' x • g (f x)) c volume
J : IntegrableOn g (f '' s) volume ↔ IntegrableOn g (f '' c) volume
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ f' x • g (f x) = f' x • g (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 : 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
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
⊢ c ⊆ a ∪ (b ∪ c)

Tactic:
exact subset_union_right.trans subset_union_right

Goal state after:
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 : 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
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
J : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in f '' c, g x
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ f' x • g (f x) = |f' x| • g (f x)

Tactic:
abs_of_nonneg (deriv_c x hx)

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 : 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
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I : ∫ (x : ℝ) in s, f' x • g (f x) = ∫ (x : ℝ) in c, f' x • g (f x)
J : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in f '' c, g x
F' : ℝ → ℝ →L[ℝ] ℝ := fun x ↦ smulRight 1 (f' x)
hF' : ∀ x ∈ c, HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
⊢ f' x • g (f x) = f' x • g (f x)
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))

Tactic:
refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ (fun i ↦ ∫ (x : ℝ) in φ i, f x ∂μ) =ᶠ[l] fun i ↦ ∫ (x : ℝ) in a i..b i, f x ∂μ