awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_4
f : α → ℝ≥0∞
μ : ι → Measure α
simp_rw : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
simp_rw₁ : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (Measure.sum μ))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
simp_rw₃ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), ∑' (i : ι), g.lintegral (μ i))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
have simp_rw₄ : Eq (α := ℝ≥0∞)
  (⨆ (g : α →ₛ ℝ≥0∞),
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
      ⨆ (s : Finset ι), ∑ i ∈ s, g.lintegral (μ i))
  (⨆ (s : Finset ι),
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
Tactic: simp_rw [ENNReal.tsum_eq_iSup_sum, ← lintegral_finsetSum_measure,
    lintegral, SimpleFunc.lintegral_sum, ENNReal.tsum_eq_iSup_sum,
    SimpleFunc.lintegral_finsetSum, iSup_comm (ι := Finset ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_4
f : α → ℝ≥0∞
μ : ι → Measure α
simp_rw : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
simp_rw₁ : ∫⁻ (a : α), f a ∂Measure.sum μ = ⨆ (s : Finset ι), ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (Measure.sum μ))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
simp_rw₃ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), ∑' (i : ι), g.lintegral (μ i))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
simp_rw₄ :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
        ⨆ (s : Finset ι), ∑ i ∈ s, g.lintegral (μ i))
    (⨆ (s : Finset ι),
      ⨆ (g : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (∑ i ∈ s, μ i))
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
have simp_rw₅ : Eq (α := ℝ≥0∞)
  (⨆ (g : α →ₛ ℝ≥0∞),
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
      ⨆ (s : Finset ι), ∑ i ∈ s, g.lintegral (μ i))
  (⨆ (s : Finset ι),
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), ∑ i ∈ s, g.lintegral (μ i))
Tactic: simp_rw [ENNReal.tsum_eq_iSup_sum, ← lintegral_finsetSum_measure,
    lintegral, SimpleFunc.lintegral_sum, ENNReal.tsum_eq_iSup_sum,
    SimpleFunc.lintegral_finsetSum, iSup_comm (ι := Finset ι)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_4
inst : MeasurableSpace α
inst_1 : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = 0
have this : Subsingleton.{u_4 + 1} (Measure α)
Tactic: have : Subsingleton (Measure α) := inferInstance
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = 0
have rw : ∫⁻ (x : α), f x ∂0 = 0
Tactic: rw [Measure.restrict_empty, lintegral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂0 = 0
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [Measure.restrict_empty, lintegral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0
have h : μ.restrict s = 0
Tactic: convert! lintegral_zero_measure _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h_1 : f =ᶠ[ae μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ g (f a) = g (f' a)
have rw : g (f' a) = g (f' a)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁_1 : f₁ =ᶠ[ae μ] f₁'
h₂_1 : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x : α
h₂ : f₂ x = f₂' x
h₁ : f₁ x = f₁' x
⊢ g (f₁ x) (f₂ x) = g (f₁' x) (f₂' x)
have rw : g (f₁' x) (f₂ x) = g (f₁' x) (f₂' x)
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁_1 : f₁ =ᶠ[ae μ] f₁'
h₂_1 : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x : α
h₂ : f₂ x = f₂' x
h₁ : f₁ x = f₁' x
rw : g (f₁' x) (f₂ x) = g (f₁' x) (f₂' x)
⊢ g (f₁ x) (f₂ x) = g (f₁' x) (f₂' x)
have rw₁ : g (f₁' x) (f₂' x) = g (f₁' x) (f₂' x)
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ
have simp : LE.le (α := ℝ≥0∞)
  (⨆ (g : α →ₛ ℝ≥0∞),
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a), g.lintegral μ)
  (⨆ (g : α →ₛ ℝ≥0∞),
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s))
Tactic: simp only [lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a), g.lintegral μ)
    (⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s))
have apply : ∀ (g : α →ₛ ℝ≥0∞) (hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a),
  g.lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s)
Tactic: apply iSup_le (fun g ↦ (iSup_le (fun hg ↦ ?_)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
⊢ g.lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s)
have this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
Tactic: have : g ≤ f := hg.trans (indicator_le_self s f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
⊢ g.lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral (μ.restrict s)
have refine : g.lintegral μ = g.lintegral (μ.restrict s)
Tactic: refine le_iSup_of_le g (le_iSup_of_le this (le_of_eq ?_))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
⊢ g.lintegral μ = g.lintegral (μ.restrict s)
have rw : Eq (α := ℝ≥0∞)
  (∑ x ∈ g.range,
    HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
  (∑ y ∈ g.range,
    HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞))
Tactic: rw [lintegral_restrict, SimpleFunc.lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ y ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞))
have e_f : ∀ (t : ℝ≥0∞),
  HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
Tactic: congr with t
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
have pos : ∀ (H : t = 0),
  HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
Tactic: by_cases H : t = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
pos :
  ∀ (H : t = 0),
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
have neg : ∀ (H : ¬t = 0),
  HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
Tactic: by_cases H : t = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
H : ¬t = 0
⊢ HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) t ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s) : ℝ≥0∞)
have neg : ∀ (x : α),
  Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) x ↔
    x ∈ preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
t : ℝ≥0∞
H : ¬t = 0
x : α
⊢ Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t}) x ↔
    x ∈ preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {t} ∩ s
have neg : (g : (a : α) → ℝ≥0∞) x = t → x ∈ s
Tactic: simp only [mem_preimage, mem_singleton_iff, mem_inter_iff, iff_self_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a
this : (⇑g : (a : α) → ℝ≥0∞) ≤ f
x : α
H : ¬Eq (α := ℝ≥0∞) ((g : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ x ∈ s
have neg : ∀ (H : x ∉ s), Eq (α := ℝ≥0∞) ((g : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
have apply : ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ
Tactic: apply le_antisymm (lintegral_indicator_le f s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ
have simp : LE.le (α := ℝ≥0∞)
  (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
    ((↑x : α →ₛ ℝ≥0∞).restrict s).lintegral μ)
  (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
    (↑x : α →ₛ ℝ≥0∞).lintegral μ)
Tactic: simp only [lintegral, ← restrict_lintegral_eq_lintegral_restrict _ hs, iSup_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a }),
      ((↑x : α →ₛ ℝ≥0∞).restrict s).lintegral μ)
    (⨆ (x : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
      (↑x : α →ₛ ℝ≥0∞).lintegral μ)
have refine : ∀ (φ : α →ₛ ℝ≥0∞) (hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
  ∃ (i' : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
    ((↑(Subtype.mk (p := fun (a : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑a : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                    hφ) :
                α →ₛ ℝ≥0∞).restrict
            s).lintegral
        μ ≤
      (↑i' : α →ₛ ℝ≥0∞).lintegral μ
Tactic: refine iSup_mono' (Subtype.forall.2 fun φ hφ => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ ∃ (i' : { i : α →ₛ ℝ≥0∞ // LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ s.indicator f a }),
    ((↑(Subtype.mk (p := fun (a : α →ₛ ℝ≥0∞) ↦ LE.le (α := (a : α) → ℝ≥0∞) (⇑a : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a) φ
                    hφ) :
                α →ₛ ℝ≥0∞).restrict
            s).lintegral
        μ ≤
      (↑i' : α →ₛ ℝ≥0∞).lintegral μ
have refine : ∀ (x : α),
  LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((φ.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
    ((fun (a : α) ↦ s.indicator f a) x : ℝ≥0∞)
Tactic: refine ⟨⟨φ.restrict s, fun x => ?_⟩, le_rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
have rw : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
Tactic: rw [lintegral_indicator hs, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
rw : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
have rw₁ : ∫⁻ (a : α) in s ∩ t, f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
Tactic: rw [lintegral_indicator hs, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
have rw : ∫⁻ (a : α), (toMeasurable μ s).indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    lintegral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
f : α → ℝ≥0∞
rw : ∫⁻ (a : α), (toMeasurable μ s).indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
have rw₁ : ∫⁻ (a : α) in toMeasurable μ s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    lintegral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
f : α → ℝ≥0∞
rw : ∫⁻ (a : α), (toMeasurable μ s).indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
rw₁ : ∫⁻ (a : α) in toMeasurable μ s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
⊢ ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
have rw₂ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [← lintegral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    lintegral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
have rw : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
Tactic: rw [lintegral_indicator₀ hs, Measure.restrict_restrict₀ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
rw : ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
have rw₁ : ∫⁻ (a : α) in s ∩ t, f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
Tactic: rw [lintegral_indicator₀ hs, Measure.restrict_restrict₀ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [lintegral_indicator₀ hs, setLIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
rw : ∫⁻ (a : α) in s, c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [lintegral_indicator₀ hs, setLIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ
have apply : ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ
Tactic: apply le_antisymm (setLIntegral_le_lintegral s fun x ↦ f x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ
have apply : ∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ
Tactic: apply le_trans (le_of_eq _) (lintegral_indicator_le _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ
have e_f : ∀ (x : α), f x = s.indicator f x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
⊢ f x = if x ∈ s then f x else 0
have pos : ∀ (h : x ∈ s), f x = f x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
x : α
pos : ∀ (h : x ∈ s), f x = f x
⊢ f x = if x ∈ s then f x else 0
have neg : ∀ (h : x ∉ s), f x = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
⊢ ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
have this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
Tactic: have : ∀ x ∈ { x | f x = r }, f x = r := fun _ hx => hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
⊢ ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
have rw : ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
Tactic: rw [setLIntegral_congr_fun _ this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ (x : α), Membership.mem (γ := Set α) {x : α | f x = r} x → f x = r
rw : ∫⁻ (x : α) in {x : α | f x = r}, r ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
⊢ ∫⁻ (x : α) in {x : α | f x = r}, f x ∂μ = HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x = r} : ℝ≥0∞)
have rw₁ : MeasurableSet.{u_1} (α := α) {x : α | f x = r}
Tactic: rw [setLIntegral_congr_fun _ this]