awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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
⊢ LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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
⊢ LE.le (α := ℝ≥0∞) (Nonempty.some ⋯) (Nonempty.some ⋯)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 : ∫⁻ (a : α), (⨅ (n : ℕ), aeSeq h_meas p n) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), (⨅ (i : ℕ), f i) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
rw [lintegral_congr_ae (aeSeq.iInf h_meas hp).symm]

Premises used: MeasureTheory.lintegral_congr_ae, aeSeq.iInf, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
simp_rw : ∫⁻ (a : α), ⨅ (i : ℕ), aeSeq h_meas p i a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), (⨅ (n : ℕ), aeSeq h_meas p n) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [iInf_apply]

Premises used: iInf_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ)
rw₁ : ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ (i : ℕ), aeSeq h_meas p i a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ

Tactic:
rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono]

Premises used: aeSeq.measurable, MeasureTheory.lintegral_iInf
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
e_s : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) fun (n : ℕ) ↦ ∫⁻ (a : α), f n a ∂μ
⊢ Eq (α := ℝ≥0∞) (⨅ (n : ℕ), ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) (⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) fun (n : ℕ) ↦ ∫⁻ (a : α), f n a ∂μ

Tactic:
funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n)

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae, MeasureTheory.lintegral_congr_ae, funext
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), aeSeq h_meas p n a ∂μ) fun (n : ℕ) ↦ ∫⁻ (a : α), f n a ∂μ

Tactic:
exact funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n)

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae, MeasureTheory.lintegral_congr_ae, funext
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
rwa rwa₁ rwa₂ rwa₃ : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), aeSeq h_meas p 0 a ∂μ ≠ ∞

Tactic:
rwa [lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)]

Premises used: aeSeq.aeSeq_n_eq_fun_n_ae, MeasureTheory.lintegral_congr_ae, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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
intro : ∀ (val : Encodable β), ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
cases nonempty_encodable β

Premises used: nonempty_encodable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ
intro₁ : Nonempty β → ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 : IsEmpty β
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
simp only [iInf_of_empty, lintegral_const,
      ENNReal.top_mul (Measure.measure_univ_ne_zero.mpr hμ)]

Premises used: Iff.mpr, MeasureTheory.lintegral_const, iInf_of_empty, MeasureTheory.Measure.measure_univ_ne_zero, ENNReal.top_mul
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 β
intro : ∀ (inhabited_h : Inhabited β), ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨅ (b : β), f b a ∂μ = ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)

Tactic:
fun a =>
      le_antisymm (le_iInf fun n => iInf_le _ _)
        (le_iInf fun b => iInf_le_of_le (Encodable.encode b + 1) ?_)

Premises used: le_iInf, le_antisymm, HAdd.hAdd, Directed.sequence, Encodable.encode, iInf_le_of_le, OfNat.ofNat, iInf_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 β
refine :
  ∀ (a : α) (b : β),
    f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed (Encodable.encode b + 1)) a ≤ f b a
⊢ ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨅ (b : β), f b a)
      (⨅ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) 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) ?_)

Premises used: le_iInf, le_antisymm, HAdd.hAdd, Encodable.encode, iInf_le_of_le, OfNat.ofNat, iInf_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed (Encodable.encode b + 1)) a ≤ f b a

Tactic:
h_directed.sequence_le b a

Premises used: Directed.sequence_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed (Encodable.encode b + 1)) a ≤ f b a

Tactic:
exact h_directed.sequence_le b a

Premises used: Directed.sequence_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)

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
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ =
    ∫⁻ (a : α), ⨅ (n : ℕ), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ

Tactic:
simp only [this, Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ ≠ ∞
rw₁ : ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n)
⊢ ∫⁻ (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:
rw [lintegral_iInf ?_ h_directed.sequence_anti]

Premises used: MeasureTheory.lintegral_iInf, Directed.sequence_anti
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) 0 a ∂μ ≠ ∞

Tactic:
hf_int _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) 0 a ∂μ ≠ ∞

Tactic:
exact hf_int _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
⊢ ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n)

Tactic:
fun n => hf _

Premises used: Directed.sequence
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
⊢ ∀ (n : ℕ), Measurable ((f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n)

Tactic:
exact fun n => hf _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ)

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

Premises used: le_iInf, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ
refine_2 :
  ∀ (n : ℕ),
    ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ ≤
      ∫⁻ (a : α), (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 ∂μ)

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

Premises used: le_iInf, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
b : β
⊢ ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ ≤
    ∫⁻ (a : α), f b a ∂μ

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

Premises used: Directed.sequence_le, MeasureTheory.lintegral_mono, HAdd.hAdd, Encodable.encode, iInf_le_of_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
b : β
⊢ ⨅ (n : ℕ), ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) 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)

Premises used: HAdd.hAdd, Encodable.encode, iInf_le_of_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
n : ℕ
⊢ ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ ≤
    ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ

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

Premises used: iInf_le, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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)
n : ℕ
⊢ ⨅ (b : β), ∫⁻ (a : α), f b a ∂μ ≤
    ∫⁻ (a : α), (f ∘ Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≥ x2) f h_directed) n a ∂μ

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

Premises used: iInf_le, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub
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 ∂μ
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 ∂μ)
⊢ ∫⁻ (a : α), ⨅ (b : β), f b 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 ∂μ) _