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 α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
this_1 : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
this : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (1 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
have ha₁ : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
this_1 : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
this : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
have this₁ : LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)
Tactic: have : (rs.map c) x < ⨆ n : ℕ, f n x := by
      refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
      suffices r * s x < 1 * s x by simpa
      gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
this_1 : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
this_2 : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
this : LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
have neg : ∀ (i : ℕ) (hi : (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x < f i x),
  Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
Tactic: rcases lt_iSup_iff.1 this with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have eq : ∀ (p : ℝ≥0∞),
  Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
    (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
Tactic: have eq : ∀ p, rs.map c ⁻¹' {p} = ⋃ n, rs.map c ⁻¹' {p} ∩ { a | p ≤ f n a } := by
    intro p
    rw [← inter_iUnion]; nth_rw 1 [← inter_univ (map c rs ⁻¹' {p})]
    refine Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_
    by_cases p_eq : p = 0
    · simp [p_eq]
    simp only [coe_map, mem_preimage, Function.comp_apply, mem_singleton_iff] at hx
    subst hx
    have : r * s x ≠ 0 := by rwa [Ne, ← ENNReal.coe_eq_zero]
    have : s x ≠ 0 := right_ne_zero_of_mul this
    have : (rs.map c) x < ⨆ n : ℕ, f n x := by
      refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
      suffices r * s x < 1 * s x by simpa
      gcongr
    rcases lt_iSup_iff.1 this with ⟨i, hi⟩
    exact mem_iUnion.2 ⟨i, le_of_lt hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r_1 : ℝ≥0
right ha_1 : (↑r_1 : ℝ≥0∞) < 1
ha : r_1 < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r_1 * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r_1 : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
r : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ LE.le.{u_1} (α := Set α)
    ((fun (n : ℕ) ↦ (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a} : Set α))
      i)
    ((fun (n : ℕ) ↦ (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a} : Set α))
      j)
have refine : Subset.{u_1} (α := Set α) {a : α | r ≤ f i a} {a : α | r ≤ f j a}
Tactic: refine inter_subset_inter_right _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have mono : ∀ (r : ℝ≥0∞),
  Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
    preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
Tactic: have mono : ∀ r : ℝ≥0∞, Monotone fun n => rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a } := by
    intro r i j h
    refine inter_subset_inter_right _ ?_
    simp_rw [subset_def, mem_setOf]
    intro x hx
    exact le_trans hx (h_mono h x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
Tactic: have h_meas : ∀ n, MeasurableSet {a : α | map c rs a ≤ f n a} := fun n =>
    measurableSet_le (SimpleFunc.measurable _) (hf n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
have rw : (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
  ∑ r ∈ (SimpleFunc.map c rs).range,
    HMul.hMul (β := ℝ≥0∞) r
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
Tactic: rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
rw :
  (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
have rw₁ : (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
  ∑ r_1 ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
    HMul.hMul (β := ℝ≥0∞) r_1
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {r_1}) :
        ℝ≥0∞)
Tactic: rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
rw :
  (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
rw₁ :
  (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
    ∑ r_1 ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
      HMul.hMul (β := ℝ≥0∞) r_1
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {r_1}) :
          ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  (∑ x ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
    HMul.hMul (β := ℝ≥0∞) x
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {x}) :
        ℝ≥0∞))
  (∑ r_1 ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
    HMul.hMul (β := ℝ≥0∞) r_1
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {r_1}) :
        ℝ≥0∞))
Tactic: rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
x : ℝ≥0∞
h : x ∈ (SimpleFunc.map c rs).range
⊢ HMul.hMul (β := ℝ≥0∞) x
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
        ℝ≥0∞) =
    ⨆ (n : ℕ),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
          ℝ≥0∞)
have rw : x *
    ⨆ (i : ℕ),
      (μ : (a : Set α) → ℝ≥0∞)
        (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f i a}) =
  ⨆ (n : ℕ),
    HMul.hMul (β := ℝ≥0∞) x
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
        ℝ≥0∞)
Tactic: rw [(mono x).measure_iUnion, ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
x : ℝ≥0∞
h : x ∈ (SimpleFunc.map c rs).range
rw :
  x *
      ⨆ (i : ℕ),
        (μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f i a}) =
    ⨆ (n : ℕ),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
          ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) x
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
        ℝ≥0∞) =
    ⨆ (n : ℕ),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
          ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  (⨆ (i : ℕ),
    HMul.hMul (β := ℝ≥0∞) x
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f i a}) :
        ℝ≥0∞))
  (⨆ (n : ℕ),
    HMul.hMul (β := ℝ≥0∞) x
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {x} ∩ {a : α | x ≤ f n a}) :
        ℝ≥0∞))
Tactic: rw [(mono x).measure_iUnion, ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
⊢ Eq (α := ℝ≥0∞)
    (∑ r ∈ (SimpleFunc.map c rs).range,
      ⨆ (n : ℕ),
        HMul.hMul (β := ℝ≥0∞) r
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}) :
            ℝ≥0∞))
    (⨆ (n : ℕ),
      ∑ r ∈ (SimpleFunc.map c rs).range,
        HMul.hMul (β := ℝ≥0∞) r
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}) :
            ℝ≥0∞))
have refine : ∀ (p : ℝ≥0∞) (i j : ℕ) (h : i ≤ j),
  HMul.hMul (β := ℝ≥0∞) p
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f i a}) :
        ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) p
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f j a}) :
        ℝ≥0∞)
Tactic: refine ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
p : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ HMul.hMul (β := ℝ≥0∞) p
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f i a}) :
        ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) p
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f j a}) :
        ℝ≥0∞)
have bc : Subset (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f i a})
  (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f j a})
Tactic: gcongr _ * μ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (p : ℝ≥0∞),
    Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
      (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (n : ℕ),
      ∑ r ∈ (SimpleFunc.map c rs).range,
        HMul.hMul (β := ℝ≥0∞) r
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}) :
            ℝ≥0∞))
    (⨆ (n : ℕ), ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}).lintegral μ)
have h : ∀ (n : ℕ),
  ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}) :
          ℝ≥0∞) ≤
    ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}).lintegral μ
Tactic: gcongr with n