awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ f = 0

Tactic:
rw [Ioc_eq_empty hab.not_gt, subset_empty_iff, support_eq_empty_iff] at h

Premises used: Function.support_eq_empty_iff, Set.Ioc_eq_empty, LE.le.not_gt, Set.subset_empty_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
h₁ : f = 0
⊢ b ≤ a

Tactic:
rw [Ioc_eq_empty hab.not_gt, subset_empty_iff, support_eq_empty_iff] at h

Premises used: Function.support_eq_empty_iff, Set.Ioc_eq_empty, LE.le.not_gt, Set.subset_empty_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : f = 0
hab : b ≤ a
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc a b → f x = g x
h' : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc b a → f x = g x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
simp only [intervalIntegral, setIntegral_congr_ae measurableSet_Ioc h,
    setIntegral_congr_ae measurableSet_Ioc h']

Premises used: MeasureTheory.setIntegral_congr_ae, intervalIntegral, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → f x = g x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
integral_congr_ae' (ae_uIoc_iff.mp h).1 (ae_uIoc_iff.mp h).2

Premises used: MeasureTheory.ae_uIoc_iff, And.right, And.left, Iff.mp, intervalIntegral.integral_congr_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
integral_congr_ae (ae_imp_of_ae_restrict h)

Premises used: MeasureTheory.ae_imp_of_ae_restrict, intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
f₁ f₂ : ℝ → ℝ
hf : f₁ =ᶠ[codiscreteWithin (Ι a b)] f₂
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f₁ x) (∫ (x : ℝ) in a..b, f₂ x)

Tactic:
integral_congr_ae_restrict (ae_restrict_le_codiscreteWithin measurableSet_uIoc hf)

Premises used: intervalIntegral.integral_congr_ae_restrict, measurableSet_uIoc, ae_restrict_le_codiscreteWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → f x = 0
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0

Tactic:
calc
    ∫ x in a..b, f x ∂μ = ∫ _ in a..b, 0 ∂μ := integral_congr_ae h
    _ = 0 := integral_zero

Premises used: Trans.trans, intervalIntegral.integral_zero, intervalIntegral.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
⊢ {x : ℝ | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂

Tactic:
have : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂ := Iic_inter_Ioc_of_le h.2
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x : ℝ | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
rw rw₁ : MeasurableSet (α := ℝ) {x : ℝ | x ≤ a₂}
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a₁..a₃, indicator {x : ℝ | x ≤ a₂} f x ∂μ) (∫ (x : ℝ) in a₁..a₂, f x ∂μ)

Tactic:
rw [integral_of_le h.1, integral_of_le (h.1.trans h.2), integral_indicator,
    Measure.restrict_restrict, this]

Premises used: MeasureTheory.Measure.restrict_restrict, intervalIntegral.integral_of_le, And.right, And.left, intervalIntegral.integral_indicator, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x : ℝ | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet (α := ℝ) {x : ℝ | x ≤ a₂}

Tactic:
measurableSet_Iic

Premises used: setOf, measurableSet_Iic, Set.Iic
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x : ℝ | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet (α := ℝ) {x : ℝ | x ≤ a₂}

Tactic:
exact measurableSet_Iic

Premises used: measurableSet_Iic
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x : ℝ | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet (α := ℝ) {x : ℝ | x ≤ a₂}

Tactic:
apply measurableSet_Iic

Premises used: measurableSet_Iic
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x : ℝ | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet (α := ℝ) {x : ℝ | x ≤ a₂}

Tactic:
all_goals apply measurableSet_Iic

Premises used: measurableSet_Iic
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi : IntervalIntegrable f μ a b
rw : Eq (α := ℝ) (∫ (x : ℝ) in Ioc a b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
rw₁ rw₂ : f =ᶠ[ae (μ.restrict (Ioc a b))] 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0

Tactic:
rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]

Premises used: intervalIntegral.integral_of_le, MeasureTheory.integral_eq_zero_iff_of_nonneg_ae, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
inl : ∀ (hab : a ≤ b), Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
inr : ∀ (hab : b ≤ a), Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
inl :
  ∀ (hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f),
    Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0

Tactic:
simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢

Premises used: Set.union_empty, Set.empty_union, Set.Ioc_eq_empty, LE.le.not_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
inr :
  ∀ (hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f),
    Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0

Tactic:
simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢

Premises used: Set.union_empty, Set.empty_union, Set.Ioc_eq_empty, LE.le.not_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0

Tactic:
integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi

Premises used: intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0

Tactic:
exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi

Premises used: intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
inr : Eq (α := ℝ) (-∫ (x : ℝ) in b..a, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
inr₁ : Eq (α := ℝ) (∫ (x : ℝ) in b..a, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
inr₂ inr₃ : f =ᶠ[ae (μ.restrict (Ioc b a))] 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0

Tactic:
rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm]

Premises used: neg_eq_zero, intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae, intervalIntegral.integral_symm, IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
inl :
  ∀ (hab : a < b),
    LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
      a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)
inr :
  ∀ (hba : b ≤ a),
    LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
      a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
    a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
rcases lt_or_ge a b with hab | hba

Premises used: lt_or_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f

Tactic:
rw [uIoc_of_le hab.le] at hf

Premises used: LT.lt.le, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
hf₁ : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
⊢ IntervalIntegrable f μ a b

Tactic:
rw [uIoc_of_le hab.le] at hf

Premises used: LT.lt.le, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
hf₁ : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi₁ : IntervalIntegrable f μ a b
⊢ a < b

Tactic:
rw [uIoc_of_le hab.le] at hf

Premises used: LT.lt.le, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
    a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
simp only [hab, true_and, integral_of_le hab.le,
      setIntegral_pos_iff_support_of_nonneg_ae hf hfi.1]

Premises used: LT.lt.le, intervalIntegral.integral_of_le, And.left, MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae, true_and
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
this : LE.le (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
    a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
simp only [this.not_gt, hba.not_gt, false_and]

Premises used: false_and, LE.le.not_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
inr : LE.le (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
    a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_gt, hba.not_gt, false_and]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
inr : LE.le (α := ℝ) 0 (∫ (x : ℝ) in Ioc b a, f x ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0

Tactic:
rw [integral_of_ge hba, neg_nonpos]

Premises used: neg_nonpos, intervalIntegral.integral_of_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f

Tactic:
rw [uIoc_comm, uIoc_of_le hba] at hf

Premises used: Set.uIoc_comm, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
hf₁ : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
⊢ IntervalIntegrable f μ a b

Tactic:
rw [uIoc_comm, uIoc_of_le hba] at hf

Premises used: Set.uIoc_comm, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
hf₁ : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
hfi₁ : IntervalIntegrable f μ a b
⊢ b ≤ a

Tactic:
rw [uIoc_comm, uIoc_of_le hba] at hf

Premises used: Set.uIoc_comm, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in Ioc b a, f x ∂μ)

Tactic:
integral_nonneg_of_ae hf

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

Tactic:
exact integral_nonneg_of_ae hf

Premises used: MeasureTheory.integral_nonneg_of_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : IntervalIntegrable f μ a b
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x ∂μ) ↔
    a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
integral_pos_iff_support_of_nonneg_ae' (ae_mono Measure.restrict_le_self hf) hfi

Premises used: intervalIntegral.integral_pos_iff_support_of_nonneg_ae', MeasureTheory.ae_mono, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
⊢ Ioo a b ⊆ support f ∩ Ioc a b

Tactic:
have hsupp : Ioo a b ⊆ support f ∩ Ioc a b := fun x hx =>
    ⟨mem_support.mpr (hpos x hx).ne', Ioo_subset_Ioc_self hx⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
rw : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), 0 x ≤ f x
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] f

Tactic:
rw [EventuallyLE, uIoc_of_le hab.le]

Premises used: LT.lt.le, Filter.EventuallyLE, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), 0 x ≤ f x

Tactic:
ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_

Premises used: MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
refine : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioo a b), 0 x ≤ f x
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), 0 x ≤ f x

Tactic:
refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_

Premises used: MeasureTheory.Ioo_ae_eq_Ioc, MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
rw : ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioo a b), 0 x ≤ f x

Tactic:
rw [ae_restrict_iff' measurableSet_Ioo]

Premises used: measurableSet_Ioo, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
x : ℝ
hx : x ∈ Ioo a b
⊢ 0 x ≤ f x

Tactic:
(hpos x hx).le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h : ∀ (a_1 : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ioo a b → 0 x ≤ f x) x} a_1
h₁ h₂ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), 0 x ≤ f x
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x

Tactic:
filter_upwards with x hx using (hpos x hx).le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] f

Tactic:
have h₀ : 0 ≤ᵐ[volume.restrict (uIoc a b)] f := by
    rw [EventuallyLE, uIoc_of_le hab.le]
    refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_
    rw [ae_restrict_iff' measurableSet_Ioo]
    filter_upwards with x hx using (hpos x hx).le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] f
rw : a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x)

Tactic:
rw [integral_pos_iff_support_of_nonneg_ae' h₀ hfi]

Premises used: intervalIntegral.integral_pos_iff_support_of_nonneg_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] f
⊢ a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
⟨hab, ((Measure.measure_Ioo_pos _).mpr hab).trans_le (measure_mono hsupp)⟩

Premises used: Iff.mpr, LT.lt.trans_le, And.intro, MeasureTheory.measure_mono, MeasureTheory.Measure.measure_Ioo_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι a b))] f
⊢ a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)

Tactic:
exact ⟨hab, ((Measure.measure_Ioo_pos _).mpr hab).trans_le (measure_mono hsupp)⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ (x : ℝ), 0 < f x
hab : a < b
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x)

Tactic:
intervalIntegral_pos_of_pos_on hfi (fun x _ => hpos x) hab

Premises used: intervalIntegral.intervalIntegral_pos_of_pos_on
-- 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∞)
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) (support (M := ℝ) fun (x : ℝ) ↦ g x - f x) : ℝ≥0∞)
hf : (ae (μ.restrict (Ioc a b))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ g x - f x
hfi₁ : Integrable (ε := ℝ) (fun (x : ℝ) ↦ g x - f x) (μ.restrict (Ioc a b))
⊢ LT.lt (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
    MeasureTheory.integral_pos_iff_support_of_nonneg_ae]

Premises used: sub_pos, MeasureTheory.integral_pos_iff_support_of_nonneg_ae, intervalIntegral.integral_of_le, intervalIntegral.integral_sub
-- 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∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) (support (M := ℝ) fun (x : ℝ) ↦ g x - f x) : ℝ≥0∞)

Tactic:
pos_iff_ne_zero.2 (mt (measure_mono_null ?_) hlt)

Premises used: Iff.mpr, mt, MeasureTheory.measure_mono_null, pos_iff_ne_zero
-- 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∞)
refine : Subset (α := Set ℝ) {x : ℝ | f x < g x} (support (M := ℝ) fun (x : ℝ) ↦ g x - f x)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) (support (M := ℝ) fun (x : ℝ) ↦ g x - f x) : ℝ≥0∞)

Tactic:
refine pos_iff_ne_zero.2 (mt (measure_mono_null ?_) hlt)

Premises used: Iff.mpr, mt, MeasureTheory.measure_mono_null, pos_iff_ne_zero
-- 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∞)
⊢ Subset (α := Set ℝ) {x : ℝ | f x < g x} (support (M := ℝ) fun (x : ℝ) ↦ g x - f x)

Tactic:
fun x hx => (sub_pos.2 hx.out).ne'

Premises used: Iff.mpr, sub_pos, Membership.mem.out, Set.Mem, setOf, Set.Subset, LT.lt.ne', Function.support, Not
-- 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∞)
⊢ Subset (α := Set ℝ) {x : ℝ | f x < g x} (support (M := ℝ) fun (x : ℝ) ↦ g x - f x)

Tactic:
exact fun x hx => (sub_pos.2 hx.out).ne'

Premises used: Iff.mpr, sub_pos, LT.lt.ne'