-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integrableOn_deriv_right_of_nonneg (hcont : ContinuousOn g (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x)
    (g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x) : IntegrableOn g' (Ioc a b)

Proof state:
case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
⊢ False

Tactic:
obtain ⟨f, fle, fint, hf⟩ :
  ∃ f : SimpleFunc ℝ ℝ≥0,
    (∀ x, f x ≤ ‖g' x‖₊) ∧
      (∫⁻ x : ℝ in Ioo a b, f x) < ∞ ∧ ENNReal.ofReal (g b - g a) < ∫⁻ x : ℝ in Ioo a b, f x :=
  exists_lt_lintegral_simpleFunc_of_lt_lintegral H

Result:
case pos.intro.intro.intro
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
⊢ False

Proof state:
case neg
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : ¬a < b
⊢ IntegrableOn g' (Ioc a b) volume

Tactic:
simp [Ioc_eq_empty hab]

Result:
no goals

Proof state:
case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
⊢ IntegrableOn g' (Ioo a b) volume

Tactic:
suffices H : (∫⁻ x in Ioo a b, ‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a) from
  ⟨meas_g'.aestronglyMeasurable, H.trans_lt ENNReal.ofReal_lt_top⟩

Result:
case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
⊢ ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊ ≤ ENNReal.ofReal (g b - g a)

Proof state:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
⊢ (fun x => derivWithin g (Ioi x) x) =ᶠ[ae (volume.restrict (Ioo a b))] g'

Tactic:
refine (ae_restrict_mem measurableSet_Ioo).mono fun x hx => ?_

Result:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ (fun x => derivWithin g (Ioi x) x) x = g' x

Proof state:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
⊢ HasFiniteIntegral F (volume.restrict (Ioo a b))

Tactic:
simpa only [F, hasFiniteIntegral_iff_enorm, comp_apply, NNReal.enorm_eq] using fint

Result:
no goals

Proof state:
case pos.intro.intro.intro
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
⊢ False

Tactic:
let F : ℝ → ℝ := (↑) ∘ f

Result:
case pos.intro.intro.intro
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
⊢ False

Proof state:
case refine_1
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b) volume
A : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ IntegrableOn F (Icc a b) volume

Tactic:
rwa [integrableOn_Icc_iff_integrableOn_Ioo]

Result:
no goals

Proof state:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
⊢ IntegrableOn F (Ioo a b) volume

Tactic:
refine ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, ?_⟩

Result:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
⊢ HasFiniteIntegral F (volume.restrict (Ioo a b))

Proof state:
case pos.intro.intro.intro
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
intF : IntegrableOn F (Ioo a b) volume
⊢ False

Tactic:
have A : ∫⁻ x : ℝ in Ioo a b, f x = ENNReal.ofReal (∫ x in Ioo a b, F x) :=
  lintegral_coe_eq_integral _ intF

Result:
case pos.intro.intro.intro
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(f x)
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
intF : IntegrableOn F (Ioo a b) volume
A : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ False