awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet h_meas p
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x
have neg : LE.le (α := ℝ≥0∞) (Nonempty.some sorry) (Nonempty.some sorry)
Tactic: simp only [aeSeq, hx, if_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone 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 : Antitone (aeSeq h_meas p)
Tactic: have h_ae_seq_mono : Antitone (aeSeq h_meas p) := by
    intro n m hnm x
    by_cases hx : x ∈ aeSeqSet h_meas p
    · exact aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm
    · simp only [aeSeq, hx, if_false]
      exact le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), (⨅ (i : ℕ), f i) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rw : ∫⁻ (a : α), (⨅ (n : ℕ), aeSeq h_meas p n) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: rw [lintegral_congr_ae (aeSeq.iInf h_meas hp).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), (⨅ (n : ℕ), aeSeq h_meas p n) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have simp_rw : ∫⁻ (a : α), ⨅ (i : ℕ), aeSeq h_meas p i a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: simp_rw [iInf_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), ⨅ (i : ℕ), aeSeq h_meas p i a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rw : Eq (α := ℝ≥0∞) (⨅ (n : ℕ), ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
Tactic: rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
rw : Eq (α := ℝ≥0∞) (⨅ (n : ℕ), ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
⊢ ∫⁻ (a : α), ⨅ (i : ℕ), aeSeq h_meas p i a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rw₁ : ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞
Tactic: rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ Eq (α := ℝ≥0∞) (⨅ (n : ℕ), ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
have e_s : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) fun (n : ℕ) ↦ ∫⁻ (a : α), f n a ∂μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro : ∀ (val : Encodable β), ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: cases nonempty_encodable β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro : IsEmpty β → ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
intro : IsEmpty β → ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro₁ : Nonempty β → ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: cases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro : ∀ (inhabited_h : Inhabited β), ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
⊢ ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
have refine : ∀ (a : α) (b : β),
  f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed (Encodable.encode b + 1)) a ≤ f b 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) ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have this : ∀ (a : α),
  Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
    (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
⊢ ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ =
    ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
have rw : ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) 0 a ∂μ ≠ ∞
Tactic: rw [lintegral_iInf ?_ h_directed.sequence_anti]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
rw : ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) 0 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ =
    ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
have rw₁ : ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n)
Tactic: rw [lintegral_iInf ?_ h_directed.sequence_anti]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
⊢ Eq (α := ℝ≥0∞)
    (⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ)
    (⨅ (b : β), ∫⁻ (a : α), f b a ∂μ)
have refine_1 : ∀ (b : β),
  ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ ≤
    ∫⁻ (a : α), f b a ∂μ
Tactic: refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
refine_1 :
  ∀ (b : β),
    ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ ≤
      ∫⁻ (a : α), f b a ∂μ
⊢ Eq (α := ℝ≥0∞)
    (⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ)
    (⨅ (b : β), ∫⁻ (a : α), f b a ∂μ)
have refine_2 : ∀ (n : ℕ),
  ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ ≤
    ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
Tactic: refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have f₁ : ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ =
  ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
Tactic: calc
    ∫⁻ a, ⨅ b, f b a ∂μ
    _ = ∫⁻ a, ⨅ n, (f ∘ h_directed.sequence f) n a ∂μ := by simp only [this, Function.comp_apply]
    _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _
    _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
      · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)
      · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
f₁ :
  ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ =
    ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have f₂ : ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ =
  ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
Tactic: calc
    ∫⁻ a, ⨅ b, f b a ∂μ
    _ = ∫⁻ a, ⨅ n, (f ∘ h_directed.sequence f) n a ∂μ := by simp only [this, Function.comp_apply]
    _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _
    _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
      · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)
      · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed n) a)
f₁ :
  ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ =
    ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
f₂ :
  ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ =
    ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
have f₃ : Eq (α := ℝ≥0∞)
  (⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ)
  (⨅ (b : β), ∫⁻ (a : α), f b a ∂μ)
Tactic: calc
    ∫⁻ a, ⨅ b, f b a ∂μ
    _ = ∫⁻ a, ⨅ n, (f ∘ h_directed.sequence f) n a ∂μ := by simp only [this, Function.comp_apply]
    _ = ⨅ n, ∫⁻ a, (f ∘ h_directed.sequence f) n a ∂μ := by
      rw [lintegral_iInf ?_ h_directed.sequence_anti]
      · exact hf_int _
      · exact fun n => hf _
    _ = ⨅ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (le_iInf fun b => ?_) (le_iInf fun n => ?_)
      · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)
      · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
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 : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
Tactic: have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦
    lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥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.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥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_iInf this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨅ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
have rw : ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ
Tactic: rw [← lintegral_iInf' hf h_anti h0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ
have refine : F =ᶠ[ae μ] fun (a : α) ↦ ⨅ (n : ℕ), f n a
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ F =ᶠ[ae μ] fun (a : α) ↦ ⨅ (n : ℕ), f n a
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ F x = (fun (a : α) ↦ (⨅ (n : ℕ), f n a : ℝ≥0∞)) x) x}
                x}
          x}
    a
Tactic: filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto
    using tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ F x = (fun (a : α) ↦ (⨅ (n : ℕ), f n a : ℝ≥0∞)) x) x} x}
            x}
      a
⊢ F =ᶠ[ae μ] fun (a : α) ↦ ⨅ (n : ℕ), f n a
have h₁ : ∀ (a : α),
  (Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n a) → Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a)) → F a = ⨅ (n : ℕ), f n a
Tactic: filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto
    using tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
have pos : ∀ (hf₀ : ∫⁻ (a : α), f a ∂μ = 0),
  ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
Tactic: by_cases hf₀ : ∫⁻ a, f a ∂μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
pos :
  ∀ (hf₀ : ∫⁻ (a : α), f a ∂μ = 0),
    ∃ (s : Set α),
      MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
have neg : ∀ (hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0),
  ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
Tactic: by_cases hf₀ : ∫⁻ a, f a ∂μ = 0