-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iSup_directed_of_measurable [Countable β] {f : β → α → ℝ≥0∞}
    (hf : ∀ b, Measurable (f b)) (h_directed : Directed (· ≤ ·) f) :
    ∫⁻ a, ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ a, f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
cases nonempty_encodable β

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f b a ≤ ⨆ n, f (Directed.sequence f h_directed n) a

Tactic:
exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
⊢ ⨆ n, ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ ≤ ⨆ b, ∫⁻ (a : α), f b a ∂μ

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
b : β
⊢ ∫⁻ (a : α), f b a ∂μ ≤ ⨆ n, ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : IsEmpty β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
simp [iSup_of_empty]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ∫⁻ (a : α), ⨆ n, f (Directed.sequence f h_directed n) a ∂μ

Tactic:
simp only [this]

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
inhabit β

Result:
case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
⊢ ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a

Tactic:
refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
b : β
⊢ f b a ≤ ⨆ n, f (Directed.sequence f h_directed n) a

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
a : α
⊢ ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ ≤ ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
b : β
⊢ ∫⁻ (a : α), f b a ∂μ ≤ ⨆ n, ∫⁻ (a : α), f (Directed.sequence f h_directed n) a ∂μ

Tactic:
exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
have : ∀ a, ⨆ b, f b a = ⨆ n, f (h_directed.sequence f n) a := by
  intro a
  refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
  exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)

Result:
case intro.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun x1 x2 => x1 ≤ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨆ b, f b a = ⨆ n, f (Directed.sequence f h_directed n) a
⊢ ∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ