awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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,
      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:
simp only [(eq _).symm]

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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∞)
rw₁ 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∞))
⊢ 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∞)

Tactic:
rw [(mono x).measure_iUnion, ENNReal.mul_iSup]

Premises used: Monotone.measure_iUnion, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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∞))

Tactic:
ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_

Premises used: ENNReal.finsetSum_iSup_of_monotone
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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}
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∞)
⊢ 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∞))

Tactic:
refine ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_

Premises used: ENNReal.finsetSum_iSup_of_monotone
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
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})
⊢ 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:
gcongr _ * μ ?_

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
⊢ 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:
mono p h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
⊢ 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:
exact mono p h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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}
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 μ
⊢ 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 μ)

Tactic:
gcongr with n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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 : ℕ
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∞))
⊢ ∑ 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:
rw [restrict_lintegral _ (h_meas n)]

Premises used: MeasureTheory.SimpleFunc.restrict_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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∞))

Tactic:
le_of_eq (Finset.sum_congr rfl fun r _ => ?_)

Premises used: le_of_eq, Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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 : ℕ
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∞)
⊢ 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:
refine le_of_eq (Finset.sum_congr rfl fun r _ => ?_)

Premises used: le_of_eq, Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_1 : r ∈ (SimpleFunc.map c rs).range
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
⊢ 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:
congr 2 with a
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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

Tactic:
and_congr_right ?_

Premises used: Set.Mem, setOf, Set.inter, and_congr_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_1 : r ∈ (SimpleFunc.map c rs).range
a : α
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)
⊢ 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:
refine and_congr_right ?_

Premises used: and_congr_right