-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Countable β]
    {f : β → α → ℝ≥0∞} {μ : Measure α} (hμ : μ ≠ 0) (hf : ∀ b, Measurable (f b))
    (hf_int : ∀ b, ∫⁻ a, f b a ∂μ ≠ ∞) (h_directed : Directed (· ≥ ·) f) :
    ∫⁻ a, ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ a, f b a ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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 fun a =>
  le_antisymm (le_iInf fun n => iInf_le _ _)
    (le_iInf fun b => iInf_le_of_le (Encodable.encode b + 1) ?_)

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

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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 α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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 α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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 : ℕ), Measurable ((f ∘ Directed.sequence f h_directed) n)

Tactic:
exact fun n => hf _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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 : β
⊢ ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ ≤ ∫⁻ (a : α), f b a ∂μ

Tactic:
exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)

Result:
no goals

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

Tactic:
exact h_directed.sequence_le b a

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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
  refine fun a =>
    le_antisymm (le_iInf fun n => iInf_le _ _)
      (le_iInf fun b => iInf_le_of_le (Encodable.encode b + 1) ?_)
  exact h_directed.sequence_le b a

Result:
case intro.inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤
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 ∂μ