awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a₁..a₃, indicator {x : ℝ | x ≤ a₂} f x ∂μ) (∫ (x : ℝ) in a₁..a₂, f x ∂μ)
have this : {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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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₂
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a₁..a₃, indicator {x : ℝ | x ≤ a₂} f x ∂μ) (∫ (x : ℝ) in a₁..a₂, f x ∂μ)
have rw : MeasurableSet (α := ℝ) {x : ℝ | x ≤ a₂}
Tactic: rw [integral_of_le h.1, integral_of_le (h.1.trans h.2), integral_indicator,
    Measure.restrict_restrict, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi : IntervalIntegrable f μ a b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
have rw : Eq (α := ℝ) (∫ (x : ℝ) in Ioc 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
have rw₁ : f =ᶠ[ae (μ.restrict (Ioc a b))] 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
Tactic: rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
have inl : ∀ (hab : a ≤ b), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
have inr : ∀ (hab : b ≤ a), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
have inl : ∀ (hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f),
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0
Tactic: simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0
have inr : ∀ (hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f),
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
Tactic: simp only [Ioc_eq_empty hab.not_gt, empty_union, union_empty] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
have inr : Eq (α := ℝ) (-∫ (x : ℝ) in b..a, 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
have inr₁ : Eq (α := ℝ) (∫ (x : ℝ) in b..a, 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
have inr₂ : f =ᶠ[ae (μ.restrict (Ioc b a))] 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] 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∞)
have 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∞)
Tactic: rcases lt_or_ge a b with hab | hba
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rcases lt_or_ge a b with hab | hba
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι 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∞)
have hf₁ : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
Tactic: rw [uIoc_of_le hab.le] at hf
Cleared hypotheses: hf, hfi, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
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∞)
have inr : LE.le (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0
Tactic: suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_gt, hba.not_gt, false_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have inr : LE.le (α := ℝ) 0 (∫ (x : ℝ) in Ioc b a, f x ∂μ)
Tactic: rw [integral_of_ge hba, neg_nonpos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in Ioc b a, f x ∂μ)
have hf₁ : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
Tactic: rw [uIoc_comm, uIoc_of_le hba] at hf
Cleared hypotheses: hf, hfi, hba
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x)
have hsupp : 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
have rw : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), 0 x ≤ f x
Tactic: rw [EventuallyLE, uIoc_of_le hab.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
have refine : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioo a b), 0 x ≤ f x
Tactic: refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 (Ioo a b), 0 x ≤ f x
have rw : ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x
Tactic: rw [ae_restrict_iff' measurableSet_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 : ℝ), x ∈ Ioo a b → 0 x ≤ f x
have h : ∀ (a_1 : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ioo a b → 0 x ≤ f x) x} a_1
Tactic: filter_upwards with x hx using (hpos x hx).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x
have h₁ : ∀ a_1 ∈ Ioo a b, 0 a_1 ≤ f a_1
Tactic: filter_upwards with x hx using (hpos x hx).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
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
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x)
have h₀ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in a..b, f x)
have rw : a < b ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (support f ∩ Ioc a b) : ℝ≥0∞)
Tactic: rw [integral_pos_iff_support_of_nonneg_ae' h₀ hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ.restrict (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) (support (M := ℝ) fun (x : ℝ) ↦ g x - f x) : ℝ≥0∞)
Tactic: rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
    MeasureTheory.integral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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∞)
⊢ LT.lt (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
have hf : (ae (μ.restrict (Ioc a b))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ g x - f x
Tactic: rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
    MeasureTheory.integral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ LT.lt (α := ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
have hfi₁ : Integrable (ε := ℝ) (fun (x : ℝ) ↦ g x - f x) (μ.restrict (Ioc a b))
Tactic: rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
    MeasureTheory.integral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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∞)
have refine : Subset (α := Set ℝ) {x : ℝ | f x < g x} (support (M := ℝ) fun (x : ℝ) ↦ g x - f x)
Tactic: refine pos_iff_ne_zero.2 (mt (measure_mono_null ?_) hlt)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ LT.lt (α := ℝ) (∫ (x : ℝ) in a..b, f x) (∫ (x : ℝ) in a..b, g x)
have hle₁ : f ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] g
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ LT.lt (α := ℝ) (∫ (x : ℝ) in a..b, f x) (∫ (x : ℝ) in a..b, g x)
have hlt₁ : Ne (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Ne (α := ℝ≥0∞) ((Measure.restrict volume (Ioc a b) : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | f x < g x} : ℝ≥0∞) (0 : ℝ≥0∞)
have 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
Tactic: contrapose! hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
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
have hlt₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc a b), g a ≤ f a
Tactic: simp only [← not_le, ← ae_iff] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
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∞)
⊢ ∀ (c : ℝ) (_ : c ∈ Icc a b), g c ≤ f c
have h_eq : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
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
⊢ ∀ (c : ℝ) (_ : c ∈ Icc a b), g c ≤ f c
have h_eq₁ : f =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] g
Tactic: rw [Measure.restrict_congr_set Ioc_ae_eq_Icc] at h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ)
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc c d, f x ∂μ)
Tactic: rw [integral_of_le hab, integral_of_le (hca.trans (hab.trans hbd))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in a..b, f u ∂μ) (∫ (u : ℝ) in a..b, g u ∂μ)
have simp : LE.le (α := ℝ) (∫ (u : ℝ) in Ioo a b, f u ∂μ) (∫ (u : ℝ) in Ioo a b, g u ∂μ)
Tactic: simp only [integral_of_le hab, integral_Ioc_eq_integral_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in Ioo a b, f u ∂μ) (∫ (u : ℝ) in Ioo a b, g u ∂μ)
have hf₁ : IntegrableOn f (Ioo a b) μ
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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) μ
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in Ioo a b, f u ∂μ) (∫ (u : ℝ) in Ioo a b, g u ∂μ)
have hg₁ : IntegrableOn g (Ioo a b) μ
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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) μ
⊢ LE.le (α := ℝ) (∫ (u : ℝ) in Ioo a b, f u ∂μ) (∫ (u : ℝ) in Ioo a b, g u ∂μ)
have hs : MeasurableSet (Ioo a b)
Tactic: apply setIntegral_mono_on
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 y + (↑n : ℝ)..y + (↑n : ℝ) + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have simp_rw : HasSum.{u_5, 0} (α := E) (fun (n : ℤ) ↦ ∫ (x : ℝ) in Ioc (y + (↑n : ℝ)) (y + (↑n : ℝ) + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
Tactic: simp_rw [integral_of_le (le_add_of_nonneg_right zero_le_one)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 : ℝ), f x ∂μ)
have 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 ∂μ)
Tactic: rw [← setIntegral_univ, ← iUnion_Ioc_add_intCast y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have inl : ∀ (h : ContDiffOn ℝ 1 f (Icc a a)) (hab : a ≤ a), ∫ (x : ℝ) in a..a, deriv f x = f a - f a
Tactic: rcases hab.eq_or_lt with rfl | h'ab
Cleared hypotheses: b, h, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have inr : ∀ (h'ab : a < b), ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Tactic: rcases hab.eq_or_lt with rfl | h'ab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
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 : ℝ) in a..b, deriv f x = f b - f a
have inr : ∀ x ∈ Ioo a b, HasDerivAt f (deriv f x) x
Tactic: apply integral_eq_sub_of_hasDerivAt_of_le hab h.continuousOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
have inr₁ : IntervalIntegrable (deriv f) volume a b
Tactic: apply integral_eq_sub_of_hasDerivAt_of_le hab h.continuousOn