-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iSup {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : Monotone f) :
    ∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n => ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
p : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ p * μ (⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f i a}) ≤ p * μ (⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f j a})

Tactic:
gcongr _ * μ ?_

Result:
case bc.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n => ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
p : ℝ≥0∞
i j : ℕ
h : i ≤ j
⊢ ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f i a} ⊆ ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f j a}

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
⊢ ↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
let rs := s.map fun a => r * a

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
⊢ ↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : x ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {p}
⊢ x ∈ ⋃ i, {a | p ≤ f i a}

Tactic:
by_cases p_eq : p = 0

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : x ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {p}
p_eq : p = 0
⊢ x ∈ ⋃ i, {a | p ≤ f i a}

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : x ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {p}
p_eq : ¬p = 0
⊢ x ∈ ⋃ i, {a | p ≤ f i a}

Proof state:
case h.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r✝ : ℝ≥0
right✝ : ↑r✝ < 1
ha✝ : ↑r✝ < 1
ha : r✝ < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r✝ * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r✝ * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n => ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
n : ℕ
r : ℝ≥0∞
x✝ : r ∈ (SimpleFunc.map c rs).range
a : α
⊢ a ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a} ↔
    a ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | (SimpleFunc.map c rs) a ≤ f n a}

Tactic:
refine and_congr_right ?_

Result:
case h.e_a.h.e_6.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r✝ : ℝ≥0
right✝ : ↑r✝ < 1
ha✝ : ↑r✝ < 1
ha : r✝ < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r✝ * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r✝ * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n => ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
n : ℕ
r : ℝ≥0∞
x✝ : r ∈ (SimpleFunc.map c rs).range
a : α
⊢ a ∈ ⇑(SimpleFunc.map c rs) ⁻¹' {r} → (a ∈ {a | r ≤ f n a} ↔ a ∈ {a | (SimpleFunc.map c rs) a ≤ f n a})

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha : ↑r < 1
⊢ ↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
have ha : r < 1 := ENNReal.coe_lt_coe.1 ha

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
⊢ ↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a => ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ : ↑r < 1
ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a => r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n => ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
⊢ ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r}) =
    ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a})

Tactic:
simp only [(eq _).symm]

Result:
no goals