awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ (const α r * s).lintegral μ ≤
    ⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ r * f a), g.lintegral μ
have refine : ∀ (x : α),
  LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((const α r * s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((fun (a : α) ↦ r * f a) x : ℝ≥0∞)
Tactic: refine le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => ?_) le_rfl)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) x) ((const α r * s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((fun (a : α) ↦ r * f a) x : ℝ≥0∞)
have dsimp : HMul.hMul (β := ℝ≥0∞) r ((s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ≤ r * f x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
x : α
⊢ HMul.hMul (β := ℝ≥0∞) r ((s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ≤ r * f x
have grw : r * (fun (a : α) ↦ f a) x ≤ r * (fun (a : α) ↦ f a) x
Tactic: grw [hs x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have pos : ∀ (h : r = 0), ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
pos : ∀ (h : r = 0), ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have neg : ∀ (h : ¬r = 0), ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have apply : ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
Tactic: apply le_antisymm _ (lintegral_const_mul_le r f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
have rinv : r * r⁻¹ = 1
Tactic: have rinv : r * r⁻¹ = 1 := ENNReal.mul_inv_cancel h hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
have rinv' : r⁻¹ * r = 1
Tactic: have rinv' : r⁻¹ * r = 1 := by
    rw [mul_comm]
    exact rinv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
have this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
Tactic: have := lintegral_const_mul_le (μ := μ) r⁻¹ fun x => r * f x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
have this₁ : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), 1 * f a ∂μ
Tactic: simp only [(mul_assoc _ _ _).symm, rinv'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
have simp_rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Tactic: simp_rw [mul_comm, lintegral_const_mul r hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
have simp_rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Tactic: simp_rw [mul_comm, lintegral_const_mul'' r hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ
have simp_rw : r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ
Tactic: simp_rw [mul_comm, lintegral_const_mul_le r f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
have simp_rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
Tactic: simp_rw [mul_comm, lintegral_const_mul' r f hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
have refine_1 : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
  MeasurableSet s → (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (s.indicator fun (x : α) ↦ c)
Tactic: refine
    @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
refine_1 :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (s.indicator fun (x : α) ↦ c)
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
have refine_2 : ∀ ⦃f g : α → ℝ≥0∞⦄,
  Disjoint (Function.support f) (Function.support g) →
    Measurable f →
      Measurable g →
        (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
          (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
            (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)
Tactic: refine
    @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
refine_1 :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (s.indicator fun (x : α) ↦ c)
refine_2 :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f →
            (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g →
              (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
have refine_3 : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
  (∀ (n : ℕ), Measurable (f n)) →
    Monotone f →
      (∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)) →
        (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) fun (x : α) ↦ ⨆ (n : ℕ), f n x
Tactic: refine
    @Measurable.ennreal_induction α m (fun f => ∫⁻ a, f a ∂μ.trim hm = ∫⁻ a, f a ∂μ) ?_ ?_ ?_ f hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ.trim hm = ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ
have refine_1 : HMul.hMul (β := ℝ≥0∞) c ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [lintegral_indicator hs, lintegral_indicator (hm s hs), setLIntegral_const,
      setLIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    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 [h_trim_s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine_1 : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: suffices h_trim_s : μ.trim hm s = μ s by rw [h_trim_s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
have h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
Tactic: have h_m := lintegral_add_left (μ := Measure.trim μ hm) hf g
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
have h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
Tactic: have h_m0 := lintegral_add_left (μ := μ) (Measurable.mono hf hm le_rfl) g
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
have refine_2 : ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ.trim hm)
  (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
  ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
Tactic: rwa [hf_prop, hg_prop, ← h_m0] at h_m
Cleared hypotheses: h_m, h_m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
refine_2 :
  ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ.trim hm)
    (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
    ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
have refine_2₁ : ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ)
  (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
  ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
Tactic: rwa [hf_prop, hg_prop, ← h_m0] at h_m
Cleared hypotheses: h_m, h_m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f g : α → ℝ≥0∞
h : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
h_1 : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
refine_2 :
  ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ.trim hm)
    (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
    ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
refine_2₁ :
  ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ)
    (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
    ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
have refine_2₂ : ∀ (h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a + g a ∂μ)
  (h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ),
  ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
Tactic: rwa [hf_prop, hg_prop, ← h_m0] at h_m
Cleared hypotheses: h_m, h_m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ.trim hm =
    ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ
have refine_3 : ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ
Tactic: rw [lintegral_iSup hf hf_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
⊢ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ
have refine_3 : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
Tactic: rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
have rw : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
    lintegral_trim hm hf.measurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
rw : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
have rw₁ : ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
    lintegral_trim hm hf.measurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
rw : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
rw₁ : ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
have rw₂ : ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
    lintegral_trim hm hf.measurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ
have rw : ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
Tactic: rw [← lintegral_trim_ae hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ
have rw₁ : AEMeasurable f ((μ.restrict s).trim hm)
Tactic: rw [← lintegral_trim_ae hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
have rw : ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α) in s, f a ∂μ.trim hm
Tactic: rw [← restrict_trim hm _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.restrict s).trim hm)
have rw : AEMeasurable f ((μ.trim hm).restrict s)
Tactic: rw [← restrict_trim hm _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ ∫⁻ (a : α), (f : (a : α) → ℝ≥0∞) a ∂μ = f.lintegral μ
have rw : ⨆ (g : α →ₛ ℝ≥0∞),
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ (f : (a : α) → ℝ≥0∞) a), g.lintegral μ =
  f.lintegral μ
Tactic: rw [MeasureTheory.lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν
have rw : LE.le (α := ℝ≥0∞)
  (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
  (⨆ (g_1 : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral ν)
Tactic: rw [lintegral, lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
have a : ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
a : ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
⊢ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
have a₁ : ∫⁻ (a : α), f a ∂μ ≤ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ ≤ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
have a : LE.le (α := ℝ≥0∞)
  (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
  (⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ)
Tactic: rw [lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ)
have a : ∀ (i : α →ₛ ℝ≥0∞) (hi : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
  i.lintegral μ ≤ ∫⁻ (a : α), (i : (a : α) → ℝ≥0∞) a ∂μ
Tactic: refine iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∫⁻ (x : α), c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : ∫⁻ (x : α), c ∂μ = ∫⁻ (a : α), Function.const α c a ∂μ
Tactic: rw [← SimpleFunc.const_lintegral, ← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) univ
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) univ
Tactic: rw [lintegral_const, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) univ
⊢ ∫⁻ (x : α), 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) univ
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [lintegral_const, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ ∫⁻ (x : α) in s, c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [lintegral_const, Measure.restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
rw :
  HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, c ∂μ = 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_const, Measure.restrict_apply_univ]