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
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}
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 μ
have h : LE.le (α := ℝ≥0∞)
  (∑ 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∞))
  (∑ r ∈ (SimpleFunc.map c rs).range,
    HMul.hMul (β := ℝ≥0∞) r
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩
            {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}) :
        ℝ≥0∞))
Tactic: rw [restrict_lintegral _ (h_meas 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}
n : ℕ
⊢ LE.le (α := ℝ≥0∞)
    (∑ 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∞))
    (∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩
              {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}) :
          ℝ≥0∞))
have h : ∀ 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∞) =
    HMul.hMul (β := ℝ≥0∞) r
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩
            {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}) :
        ℝ≥0∞)
Tactic: refine le_of_eq (Finset.sum_congr rfl fun r _ => ?_)
-- 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})
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}
n : ℕ
r : ℝ≥0∞
h : 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∞) =
    HMul.hMul (β := ℝ≥0∞) r
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩
            {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}) :
        ℝ≥0∞)
have h : ∀ (a : α),
  Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a})
      a ↔
    Membership.mem (γ := Set α)
      (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩
        {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a})
      a
Tactic: congr 2 with a
-- 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})
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}
n : ℕ
r : ℝ≥0∞
h : r ∈ (SimpleFunc.map c rs).range
a : α
⊢ Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a})
      a ↔
    Membership.mem (γ := Set α)
      (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩
        {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a})
      a
have h : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) a →
  (Membership.mem (γ := Set α) {a : α | r ≤ f n a} a ↔
    Membership.mem (γ := Set α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} a)
Tactic: refine and_congr_right ?_
-- 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 : ℕ), ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}).lintegral μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
have simp : LE.le (α := ℝ≥0∞)
  (⨆ (n : ℕ),
    ∫⁻ (a : α),
      ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞) a ∂μ)
  (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
Tactic: simp only [← SimpleFunc.lintegral_eq_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}
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (n : ℕ),
      ∫⁻ (a : α),
        ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞)
          a ∂μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
have h : ∀ (n : ℕ) (a : α),
  ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞) a ≤ f n a
Tactic: gcongr with n a
-- 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 : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a}
n : ℕ
a : α
⊢ ((SimpleFunc.map c rs).restrict {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a} : (a : α) → ℝ≥0∞) a ≤ f n a
have h : indicator {a : α | c ((rs : (a : α) → ℝ≥0) a) ≤ f n a} (c ∘ (⇑rs : (a : α) → ℝ≥0)) a ≤ f n a
Tactic: simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]
-- 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 ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have μ₁ : (↑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: calc
    (r : ℝ≥0∞) * (s.map c).lintegral μ = ∑ r ∈ (rs.map c).range, r * μ (rs.map c ⁻¹' {r}) := by
      rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]
    _ = ∑ r ∈ (rs.map c).range, r * μ (⋃ n, rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a }) := by
      simp only [(eq _).symm]
    _ = ∑ r ∈ (rs.map c).range, ⨆ n, r * μ (rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a }) :=
      Finset.sum_congr rfl fun x _ => by rw [(mono x).measure_iUnion, ENNReal.mul_iSup]
    _ = ⨆ n, ∑ r ∈ (rs.map c).range, r * μ (rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a }) := by
      refine ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_
      gcongr _ * μ ?_
      exact mono p h
    _ ≤ ⨆ n : ℕ, ((rs.map c).restrict { a | (rs.map c) a ≤ f n a }).lintegral μ := by
      gcongr with n
      rw [restrict_lintegral _ (h_meas n)]
      refine le_of_eq (Finset.sum_congr rfl fun r _ => ?_)
      congr 2 with a
      refine and_congr_right ?_
      simp +contextual
    _ ≤ ⨆ n, ∫⁻ a, f n a ∂μ := by
      simp only [← SimpleFunc.lintegral_eq_lintegral]
      gcongr with n a
      simp only [map_apply] at h_meas
      simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]
      exact indicator_apply_le id
-- 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∞)
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have μ₂ : Eq (α := ℝ≥0∞)
  (∑ r ∈ (SimpleFunc.map c rs).range,
    HMul.hMul (β := ℝ≥0∞) r
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
  (∑ r ∈ (SimpleFunc.map c rs).range,
    HMul.hMul (β := ℝ≥0∞) r
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}) :
        ℝ≥0∞))
Tactic: calc
    (r : ℝ≥0∞) * (s.map c).lintegral μ = ∑ r ∈ (rs.map c).range, r * μ (rs.map c ⁻¹' {r}) := by
      rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]
    _ = ∑ r ∈ (rs.map c).range, r * μ (⋃ n, rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a }) := by
      simp only [(eq _).symm]
    _ = ∑ r ∈ (rs.map c).range, ⨆ n, r * μ (rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a }) :=
      Finset.sum_congr rfl fun x _ => by rw [(mono x).measure_iUnion, ENNReal.mul_iSup]
    _ = ⨆ n, ∑ r ∈ (rs.map c).range, r * μ (rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a }) := by
      refine ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_
      gcongr _ * μ ?_
      exact mono p h
    _ ≤ ⨆ n : ℕ, ((rs.map c).restrict { a | (rs.map c) a ≤ f n a }).lintegral μ := by
      gcongr with n
      rw [restrict_lintegral _ (h_meas n)]
      refine le_of_eq (Finset.sum_congr rfl fun r _ => ?_)
      congr 2 with a
      refine and_congr_right ?_
      simp +contextual
    _ ≤ ⨆ n, ∫⁻ a, f n a ∂μ := by
      simp only [← SimpleFunc.lintegral_eq_lintegral]
      gcongr with n a
      simp only [map_apply] at h_meas
      simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]
      exact indicator_apply_le id
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have simp_rw : ∫⁻ (a : α), (⨆ (i : ℕ), f i) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: simp_rw [← iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
have pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p n x ≤ aeSeq hf p m x
Tactic: by_cases hx : x ∈ aeSeqSet hf p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p n x ≤ aeSeq hf p m x
⊢ aeSeq hf p n x ≤ aeSeq hf p m x
have neg : ∀ (hx : x ∉ aeSeqSet hf p), aeSeq hf p n x ≤ aeSeq hf p m x
Tactic: by_cases hx : x ∈ aeSeqSet hf p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
⊢ ∫⁻ (a : α), (⨆ (i : ℕ), f i) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have h_ae_seq_mono : Monotone (aeSeq hf p)
Tactic: have h_ae_seq_mono : Monotone (aeSeq hf p) := by
    intro n m hnm x
    by_cases hx : x ∈ aeSeqSet hf p
    · exact aeSeq.prop_of_mem_aeSeqSet hf hx hnm
    · simp only [aeSeq, hx, if_false, le_rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ (i : ℕ), f i) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rw : ∫⁻ (a : α), (⨆ (n : ℕ), aeSeq hf p n) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ (n : ℕ), aeSeq hf p n) a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have simp_rw : ∫⁻ (a : α), ⨆ (i : ℕ), aeSeq hf p i a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: simp_rw [iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ ∫⁻ (a : α), ⨆ (i : ℕ), aeSeq hf p i a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rw : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
Tactic: rw [lintegral_iSup (aeSeq.measurable hf p) h_ae_seq_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Monotone (aeSeq hf p)
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
have e_s : ∀ (n : ℕ), ∫⁻ (a : α), aeSeq hf p n a ∂μ = ∫⁻ (a : α), f n a ∂μ
Tactic: congr with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
have this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
Tactic: have : Monotone fun n => ∫⁻ x, f n x ∂μ := fun i j hij =>
    lintegral_mono_ae (h_mono.mono fun x hx => hx hij)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ))
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
have suffices : ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
Tactic: suffices key : ∫⁻ x, F x ∂μ = ⨆ n, ∫⁻ x, f n x ∂μ by
    rw [key]
    exact tendsto_atTop_iSup this