awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : Ne (α := ℝ≥0∞) ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (μ.restrict (Ioc a b))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ g x - f x

Tactic:
hle.mono fun x => sub_nonneg.2

Premises used: Iff.mpr, Filter.Eventually.mono, Filter.EventuallyLE, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : Ne (α := ℝ≥0∞) ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ g x - f x) (μ.restrict (Ioc a b))

Tactic:
hgi.1.sub hfi.1

Premises used: MeasureTheory.IntegrableOn.sub, MeasureTheory.IntegrableOn, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g
hlt : Ne (α := ℝ≥0∞) ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae (μ.restrict (Ioc a b))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ g x - f x

Tactic:
exacts [hle.mono fun x => sub_nonneg.2, hgi.1.sub hfi.1]

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.sub, Filter.Eventually.mono, And.left, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
hle₁ : f ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
hlt₁ : Ne (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) (∫ (x : ℝ) in a..b, f x) (∫ (x : ℝ) in a..b, g x)

Tactic:
apply integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero hab.le
    (hfc.intervalIntegrable_of_Icc hab.le) (hgc.intervalIntegrable_of_Icc hab.le)

Premises used: LT.lt.le, ContinuousOn.intervalIntegrable_of_Icc, intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ f ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g

Tactic:
simpa only [measurableSet_Ioc, ae_restrict_eq]
      using (ae_restrict_mem measurableSet_Ioc).mono hle

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono, MeasureTheory.ae_restrict_eq, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
hlt₁ :
  ∀
    (hlt :
      Eq (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞))
    (c : ℝ) (_ : c ∈ Icc a b), g c ≤ f c
⊢ Ne (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
contrapose! hlt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : Eq (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc a b), g a ≤ f a

Tactic:
simp only [← not_le, ← ae_iff] at hlt

Premises used: not_le, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc a b), g a ≤ f a
⊢ f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g

Tactic:
EventuallyLE.antisymm ((ae_restrict_iff' measurableSet_Ioc).2 <|
      Eventually.of_forall hle) hlt

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.EventuallyLE.antisymm, MeasureTheory.ae_restrict_iff', measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc a b), g a ≤ f a
⊢ f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g

Tactic:
exact EventuallyLE.antisymm ((ae_restrict_iff' measurableSet_Ioc).2 <|
      Eventually.of_forall hle) hlt

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.EventuallyLE.antisymm, MeasureTheory.ae_restrict_iff', measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : Eq (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g

Tactic:
have h_eq : f =ᵐ[volume.restrict (Ioc a b)] g := by
    simp only [← not_le, ← ae_iff] at hlt
    exact EventuallyLE.antisymm ((ae_restrict_iff' measurableSet_Ioc).2 <|
      Eventually.of_forall hle) hlt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : Eq (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
⊢ f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] g

Tactic:
rw [Measure.restrict_congr_set Ioc_ae_eq_Icc] at h_eq

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioc_ae_eq_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : Eq (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] g
⊢ ∀ (c : ℝ) (_ : c ∈ Icc a b), g c ≤ f c

Tactic:
fun c hc ↦ (Measure.eqOn_Icc_of_ae_eq volume hab.ne h_eq hfc hgc hc).ge

Premises used: Eq.ge, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.eqOn_Icc_of_ae_eq, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : Eq (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] g
⊢ ∀ (c : ℝ) (_ : c ∈ Icc a b), g c ≤ f c

Tactic:
exact fun c hc ↦ (Measure.eqOn_Icc_of_ae_eq volume hab.ne h_eq hfc hgc hc).ge

Premises used: Eq.ge, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.eqOn_Icc_of_ae_eq, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Icc a b))] f
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), 0 x ≤ f x := ⋯
⊢ LE.le (α := ℝ) 0 (∫ (u : ℝ) in a..b, f u ∂μ)

Tactic:
simpa only [integral_of_le hab] using setIntegral_nonneg_of_ae_restrict H

Premises used: intervalIntegral.integral_of_le, MeasureTheory.setIntegral_nonneg_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae μ] f
⊢ LE.le (α := ℝ) 0 (∫ (u : ℝ) in a..b, f u ∂μ)

Tactic:
integral_nonneg_of_ae_restrict hab <| ae_restrict_of_ae hf

Premises used: MeasureTheory.ae_restrict_of_ae, intervalIntegral.integral_nonneg_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : ∀ (u : ℝ), 0 ≤ f u
⊢ LE.le (α := ℝ) 0 (∫ (u : ℝ) in a..b, f u ∂μ)

Tactic:
integral_nonneg_of_ae hab <| Eventually.of_forall hf

Premises used: Filter.Eventually.of_forall, intervalIntegral.integral_nonneg_of_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : ∀ u ∈ Icc a b, 0 ≤ f u
⊢ LE.le (α := ℝ) 0 (∫ (u : ℝ) in a..b, f u ∂μ)

Tactic:
integral_nonneg_of_ae_restrict hab <| (ae_restrict_iff' measurableSet_Icc).mpr <| ae_of_all μ hf

Premises used: Iff.mpr, intervalIntegral.integral_nonneg_of_ae_restrict, MeasureTheory.ae_of_all, measurableSet_Icc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
⊢ LE.le (α := ℝ) |∫ (x : ℝ) in a..b, f x ∂μ| (∫ (x : ℝ) in a..b, |f x| ∂μ)

Tactic:
simpa only [← Real.norm_eq_abs] using norm_integral_le_integral_norm hab

Premises used: intervalIntegral.norm_integral_le_integral_norm, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hle : ∀ x ∈ Ioc a b, 0 ≤ f x
hlt : ∃ c ∈ Icc a b, 0 < f c
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f
hfi : IntervalIntegrable f μ c d
rw : LE.le (α := ℝ) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc c d, f x ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ)

Tactic:
rw [integral_of_le hab, integral_of_le (hca.trans (hab.trans hbd))]

Premises used: intervalIntegral.integral_of_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f
hfi : IntervalIntegrable f μ c d
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc c d, f x ∂μ)

Tactic:
setIntegral_mono_set hfi.1 hf (Ioc_subset_Ioc hca hbd).eventuallyLE

Premises used: MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, Set.Ioc_subset_Ioc, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f
hfi : IntervalIntegrable f μ c d
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc c d, f x ∂μ)

Tactic:
exact setIntegral_mono_set hfi.1 hf (Ioc_subset_Ioc hca hbd).eventuallyLE

Premises used: MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, Set.Ioc_subset_Ioc, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
h : Ι a b ⊆ Ι c d
hf : 0 ≤ᶠ[ae (μ.restrict (Ι c d))] f
hfi : IntervalIntegrable f μ c d
⊢ LE.le (α := ℝ) |∫ (x : ℝ) in a..b, f x ∂μ| |∫ (x : ℝ) in c..d, f x ∂μ|

Tactic:
have hf' : 0 ≤ᵐ[μ.restrict (Ι a b)] f := ae_mono (Measure.restrict_mono h le_rfl) hf
  calc
    |∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| := abs_integral_eq_abs_integral_uIoc f
    _ = ∫ x in Ι a b, f x ∂μ := abs_of_nonneg (MeasureTheory.integral_nonneg_of_ae hf')
    _ ≤ ∫ x in Ι c d, f x ∂μ := setIntegral_mono_set hfi.def' hf h.eventuallyLE
    _ ≤ |∫ x in Ι c d, f x ∂μ| := le_abs_self _
    _ = |∫ x in c..d, f x ∂μ| := (abs_integral_eq_abs_integral_uIoc f).symm

Premises used: Trans.trans, le_rfl, le_abs_self, MeasureTheory.Measure.restrict_mono, Set.uIoc, MeasureTheory.setIntegral_mono_set, MeasureTheory.ae_mono, MeasureTheory.Measure.restrict, HasSubset.Subset.eventuallyLE, MeasureTheory.integral_nonneg_of_ae, MeasureTheory.integral, IntervalIntegrable.def', abs_of_nonneg, intervalIntegral.abs_integral_eq_abs_integral_uIoc, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᶠ[ae (μ.restrict (Icc a b))] g
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), f x ≤ g x := ⋯
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in a..b, f u ∂μ) (∫ (u : ℝ) in a..b, g u ∂μ)

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_ae_restrict hf.1 hg.1 H

Premises used: intervalIntegral.integral_of_le, And.left, MeasureTheory.setIntegral_mono_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᶠ[ae μ] g
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in a..b, f u ∂μ) (∫ (u : ℝ) in a..b, g u ∂μ)

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_ae hf.1 hg.1 h

Premises used: intervalIntegral.integral_of_le, And.left, MeasureTheory.setIntegral_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ x ∈ Icc a b, f x ≤ g x
H : ∀ (x : ℝ) (hx : x ∈ Ioc a b), f x ≤ g x := ⋯
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in a..b, f u ∂μ) (∫ (u : ℝ) in a..b, g u ∂μ)

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_on hf.1 hg.1 measurableSet_Ioc H

Premises used: intervalIntegral.integral_of_le, And.left, measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
simp : LE.le (α := ℝ) (∫ (u : ℝ) in Ioo a b, f u ∂μ) (∫ (u : ℝ) in Ioo a b, g u ∂μ)
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in a..b, f u ∂μ) (∫ (u : ℝ) in a..b, g u ∂μ)

Tactic:
simp only [integral_of_le hab, integral_Ioc_eq_integral_Ioo]

Premises used: MeasureTheory.integral_Ioc_eq_integral_Ioo, intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
hf₁ : IntegrableOn f (Ioo a b) μ
hg₁ : IntegrableOn g (Ioo a b) μ
hs : MeasurableSet (Ioo a b)
h₁ : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in Ioo a b, f u ∂μ) (∫ (u : ℝ) in Ioo a b, g u ∂μ)

Tactic:
apply setIntegral_mono_on

Premises used: MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn f (Ioo a b) μ

Tactic:
apply hf.1.mono Ioo_subset_Ioc_self le_rfl

Premises used: le_rfl, And.left, Set.Ioo_subset_Ioc_self, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

Tactic:
apply hg.1.mono Ioo_subset_Ioc_self le_rfl

Premises used: le_rfl, And.left, Set.Ioo_subset_Ioc_self, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

Tactic:
measurableSet_Ioo

Premises used: measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

Tactic:
exact measurableSet_Ioo

Premises used: measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst : NoAtoms μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ g
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in a..b, f u ∂μ) (∫ (u : ℝ) in a..b, g u ∂μ)

Tactic:
integral_mono_ae hab hf hg <| ae_of_all _ h

Premises used: intervalIntegral.integral_mono_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
simp_rw :
  HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)
    (∫ (x : ℝ), f x ∂μ)
⊢ HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in y + (↑n : ℝ)..y + (↑n : ℝ) + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
simp_rw [integral_of_le (le_add_of_nonneg_right zero_le_one)]

Premises used: zero_le_one, intervalIntegral.integral_of_le, le_add_of_nonneg_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
rw :
  HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)
    (∫ (x : ℝ) in ⋃ (n : ℤ), Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)
⊢ HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)
    (∫ (x : ℝ), f x ∂μ)

Tactic:
rw [← setIntegral_univ, ← iUnion_Ioc_add_intCast y]

Premises used: iUnion_Ioc_add_intCast, MeasureTheory.setIntegral_univ
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)
    (∫ (x : ℝ) in ⋃ (n : ℤ), Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)

Tactic:
hasSum_integral_iUnion (fun i => measurableSet_Ioc) (pairwise_disjoint_Ioc_add_intCast y)
      hfi.integrableOn

Premises used: Set.pairwise_disjoint_Ioc_add_intCast, MeasureTheory.hasSum_integral_iUnion, MeasureTheory.Integrable.integrableOn, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)
    (∫ (x : ℝ) in ⋃ (n : ℤ), Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ)

Tactic:
exact
    hasSum_integral_iUnion (fun i => measurableSet_Ioc) (pairwise_disjoint_Ioc_add_intCast y)
      hfi.integrableOn

Premises used: Set.pairwise_disjoint_Ioc_add_intCast, MeasureTheory.hasSum_integral_iUnion, MeasureTheory.Integrable.integrableOn, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in 0..1, f (x + (↑n : ℝ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f x)

Tactic:
simpa only [integral_comp_add_right, zero_add, add_comm (1 : ℝ)] using
    hfi.hasSum_intervalIntegral 0

Premises used: MeasureTheory.Integrable.hasSum_intervalIntegral, zero_add, add_comm, intervalIntegral.integral_comp_add_right, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
inl : ∀ (h : ContDiffOn ℝ 1 f (Icc a a)) (hab : a ≤ a), ∫ (x : ℝ) in a..a, deriv f x = f a - f a
inr : ∀ (h'ab : a < b), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
rcases hab.eq_or_lt with rfl | h'ab

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a a)
hab : a ≤ a
⊢ ∫ (x : ℝ) in a..a, deriv f x = f a - f a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
inr : ∀ x ∈ Ioo a b, HasDerivAt f (deriv f x) x
inr₁ : IntervalIntegrable (deriv f) volume a b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
apply integral_eq_sub_of_hasDerivAt_of_le hab h.continuousOn

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, ContDiffOn.continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
inr : DifferentiableAt ℝ f x
⊢ HasDerivAt f (deriv f x) x

Tactic:
apply DifferentiableAt.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
inr : Icc a b ∈ 𝓝 x
⊢ DifferentiableAt ℝ f x

Tactic:
apply ((h x ⟨hx.1.le, hx.2.le⟩).differentiableWithinAt one_ne_zero).differentiableAt

Premises used: DifferentiableWithinAt.differentiableAt, LT.lt.le, And.right, And.left, And.intro, one_ne_zero, ContDiffWithinAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 x

Tactic:
Icc_mem_nhds hx.1 hx.2

Premises used: Set.Mem, And.right, And.left, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 x

Tactic:
exact Icc_mem_nhds hx.1 hx.2

Premises used: And.right, And.left, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ HAdd.hAdd (α := WithTop ℕ∞) 0 1 ≤ 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst_2 : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
⊢ ContinuousOn (derivWithin f (Icc a b)) (Icc a b)

Tactic:
have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn