awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
x : ℝ
hx : x ∈ Ioo a b
⊢ 0 ≤ derivWithin f (Icc a b) x

Tactic:
exact hf.derivWithin_nonneg

Premises used: MonotoneOn.derivWithin_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
⊢ ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x

Tactic:
have f_deriv_nonneg {x : ℝ} (hx : x ∈ Ioo a b) : 0 ≤ deriv f x := by
    rw [← derivWithin_of_mem_nhds (Icc_mem_nhds (a := a) (b := b) (by grind) (by grind))]
    exact hf.derivWithin_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
left : LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x)
right : ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x) ∧ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
left : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] deriv f
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x)

Tactic:
apply intervalIntegral.integral_nonneg_of_ae_restrict hab

Premises used: intervalIntegral.integral_nonneg_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ MeasurableSet (Icc a b)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
left : ∀ᵐ (x : ℝ), x ∈ Icc a b → 0 x ≤ deriv f x
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] deriv f

Tactic:
rw [Filter.EventuallyLE, MeasureTheory.ae_restrict_iff' (by simp)]

Premises used: MeasureTheory.ae_restrict_iff', Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
x : ℝ
h : x ≠ a → x ≠ b → x ∈ Icc a b → 0 x ≤ deriv f x
⊢ x ≠ a → x ≠ b → x ∈ Icc a b → 0 x ≤ deriv f x

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
x : ℝ
h_1 : x ≠ a
h : x ≠ b → x ∈ Icc a b → 0 x ≤ deriv f x
⊢ x ≠ b → x ∈ Icc a b → 0 x ≤ deriv f x

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
x : ℝ
h_1 : x ≠ a
h_2 : x ≠ b
h : x ∈ Icc a b → 0 x ≤ deriv f x
⊢ x ∈ Icc a b → 0 x ≤ deriv f x

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
h : ∀ (x : ℝ), x ≠ a → x ≠ b → x ∈ Icc a b → 0 x ≤ deriv f x
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → 0 x ≤ deriv f x

Tactic:
filter_upwards [h₁, h₂] with x _ _ _
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
x : ℝ
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
⊢ x ∈ Ioo a b

Tactic:
grind [Icc_diff_both]

Premises used: Set.Icc_diff_both
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
x : ℝ
h : x ≠ a
h_1 : x ≠ b
h_2 : x ∈ Icc a b
⊢ 0 x ≤ deriv f x

Tactic:
exact f_deriv_nonneg (by grind [Icc_diff_both])
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ MeasurableSet (uIcc a b)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ ∂volume) atTop

Tactic:
have ebound := lintegral_enorm_le_liminf_of_tendsto
      ((MeasureTheory.ae_restrict_iff' (by measurability) |>.mpr hGf))
      (fun n ↦ (hG n).aemeasurable.enorm)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound :
  ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ ∂volume) atTop
⊢ ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ ENNReal.ofReal (f b - f a)

Tactic:
grw [hG'] at ebound
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound :
  ENNReal.ofReal
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ ‖deriv f x‖) ≤
    ENNReal.ofReal (f b - f a)
linarith : f b - f a < 0 → f a - f b + (f b - f a - 0) = 0
⊢ 0 ≤ f b - f a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ ENNReal.ofReal (f b - f a)
⊢ ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a

Tactic:
rw [uIcc_of_le hab,
        ← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm integrable_f_deriv,
        ENNReal.ofReal_le_ofReal_iff (by linarith),
        integral_Icc_eq_integral_Ioc,
        ← intervalIntegral.integral_of_le hab] at ebound

Premises used: ENNReal.ofReal_le_ofReal_iff, Set.uIcc_of_le, intervalIntegral.integral_of_le, MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a

Tactic:
ebound
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
h : Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x) (∫ (x : ℝ) in a..b, ‖deriv f x‖)
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
convert! ebound using 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x) (∫ (x : ℝ) in a..b, ‖deriv f x‖)

Tactic:
intervalIntegral.integral_congr_ae ?_

Premises used: intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
h : ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x = ‖deriv f x‖
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x) (∫ (x : ℝ) in a..b, ‖deriv f x‖)

Tactic:
refine intervalIntegral.integral_congr_ae ?_

Premises used: intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
h : ∀ᵐ (x : ℝ), x ∈ Ioc a b → deriv f x = ‖deriv f x‖
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x = ‖deriv f x‖

Tactic:
rw [uIoc_of_le hab]

Premises used: Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
x : ℝ
h : x ≠ b → x ∈ Ioc a b → deriv f x = ‖deriv f x‖
⊢ x ≠ b → x ∈ Ioc a b → deriv f x = ‖deriv f x‖

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
x : ℝ
h_1 : x ≠ b
h : x ∈ Ioc a b → deriv f x = ‖deriv f x‖
⊢ x ∈ Ioc a b → deriv f x = ‖deriv f x‖

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
h : ∀ (x : ℝ), x ≠ b → x ∈ Ioc a b → deriv f x = ‖deriv f x‖
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc a b → deriv f x = ‖deriv f x‖

Tactic:
filter_upwards [h₂] with x _ _