awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
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₂ : 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]
    _ = ⨆ n, ∫⁻ a, f (h_directed.sequence f n) a ∂μ :=
      (lintegral_iSup (fun n => hf _) h_directed.sequence_mono)
    _ = ⨆ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
      · exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
      · exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have simp_rw : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: simp_rw [← iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
⊢ ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
have h : ∀ (x : α) (i j : β),
  ∃ (z : β),
    LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)
Tactic: filter_upwards [] with x i j
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
x : α
i j : β
⊢ ∃ (z : β),
    LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)
have h : ∀ (z : β) (hz₁ : f i ≤ f z) (hz₂ : f j ≤ f z),
  ∃ (z : β),
    LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) i) ((fun (i : β) ↦ f i x) z) ∧
      LE.le (α := ℝ≥0∞) ((fun (i : β) ↦ f i x) j) ((fun (i : β) ↦ f i x) z)
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
Tactic: have hp : ∀ᵐ x ∂μ, p x fun i => f i x := by
    filter_upwards [] with x i j
    obtain ⟨z, hz₁, hz₂⟩ := h_directed i j
    exact ⟨z, hz₁ x, hz₂ x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ : β
⊢ ∃ (z : β), aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
have obtain : ∀ (z : β) (hz₁ : f b₁ ≤ f z) (hz₂ : f b₂ ≤ f z), ∃ (z : β), aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h_directed b₁ b₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
⊢ ∃ (z : β), aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
have refine_1 : aeSeq hf p b₁ ≤ aeSeq hf p z
Tactic: refine ⟨z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
refine_1 : aeSeq hf p b₁ ≤ aeSeq hf p z
⊢ ∃ (z : β), aeSeq hf p b₁ ≤ aeSeq hf p z ∧ aeSeq hf p b₂ ≤ aeSeq hf p z
have refine_2 : aeSeq hf p b₂ ≤ aeSeq hf p z
Tactic: refine ⟨z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x
have pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p b₁ x ≤ aeSeq hf p z x
Tactic: by_cases hx : x ∈ aeSeqSet hf p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p b₁ x ≤ aeSeq hf p z x
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x
have neg : ∀ (hx : x ∉ aeSeqSet hf p), aeSeq hf p b₁ x ≤ aeSeq hf p z x
Tactic: by_cases hx : x ∈ aeSeqSet hf p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x
have pos : f b₁ x ≤ aeSeq hf p z x
Tactic: rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₁ x ≤ aeSeq hf p z x
have pos : f b₁ x ≤ f z x
Tactic: rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z x
have pos : f b₁ x ≤ f z x
Tactic: repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₁ x ≤ aeSeq hf p z 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.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
have pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p b₂ x ≤ aeSeq hf p z x
Tactic: by_cases hx : x ∈ aeSeqSet hf p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
pos : ∀ (hx : x ∈ aeSeqSet hf p), aeSeq hf p b₂ x ≤ aeSeq hf p z x
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
have neg : ∀ (hx : x ∉ aeSeqSet hf p), aeSeq hf p b₂ x ≤ aeSeq hf p z x
Tactic: by_cases hx : x ∈ aeSeqSet hf p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
have pos : f b₂ x ≤ aeSeq hf p z x
Tactic: rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ f b₂ x ≤ aeSeq hf p z x
have pos : f b₂ x ≤ f z x
Tactic: rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z x
have pos : f b₂ x ≤ f z x
Tactic: repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
b₁ b₂ z : β
hz₁ : f b₁ ≤ f z
hz₂ : f b₂ ≤ f z
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p b₂ x ≤ aeSeq hf p z 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.Add (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have h_ae_seq_directed : Directed LE.le (aeSeq hf p)
Tactic: have h_ae_seq_directed : Directed LE.le (aeSeq hf p) := by
    intro b₁ b₂
    obtain ⟨z, hz₁, hz₂⟩ := h_directed b₁ b₂
    refine ⟨z, ?_, ?_⟩ <;>
      · intro x
        by_cases hx : x ∈ aeSeqSet hf p
        · repeat rw [aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet hf hx]
          apply_rules [hz₁, hz₂]
        · simp only [aeSeq, hx, if_false]
          exact le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have h : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂μ
Tactic: convert! lintegral_iSup_directed_of_measurable (aeSeq.measurable hf p) h_ae_seq_directed using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
h : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂μ
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have h₁ : Eq (α := ℝ≥0∞) (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ) (⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂μ)
Tactic: convert! lintegral_iSup_directed_of_measurable (aeSeq.measurable hf p) h_ae_seq_directed using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), ⨆ (b : β), aeSeq hf p b a ∂μ
have h : ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), (⨆ (i : β), aeSeq hf p i) a ∂μ
Tactic: simp_rw [← iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ ∫⁻ (a : α), (⨆ (i : β), f i) a ∂μ = ∫⁻ (a : α), (⨆ (i : β), aeSeq hf p i) a ∂μ
have h : ∫⁻ (a : α), (⨆ (n : β), aeSeq hf p n) a ∂μ = ∫⁻ (a : α), (⨆ (i : β), aeSeq hf p i) a ∂μ
Tactic: rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ Eq (α := ℝ≥0∞) (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ) (⨆ (b : β), ∫⁻ (a : α), aeSeq hf p b a ∂μ)
have h : Eq.{u_2 + 1} (α := β → ℝ≥0∞) (fun (b : β) ↦ ∫⁻ (a : α), f b a ∂μ) fun (b : β) ↦ ∫⁻ (a : α), aeSeq hf p b a ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
⊢ Eq.{u_2 + 1} (α := β → ℝ≥0∞) (fun (b : β) ↦ ∫⁻ (a : α), f b a ∂μ) fun (b : β) ↦ ∫⁻ (a : α), aeSeq hf p b a ∂μ
have h : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a : α), aeSeq hf p b a ∂μ
Tactic: ext1 b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a : α), aeSeq hf p b a ∂μ
have h : f b =ᶠ[ae μ] aeSeq hf p b
Tactic: rw [lintegral_congr_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun (x : α) (f' : β → ℝ≥0∞) ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : β) ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ f b =ᶠ[ae μ] aeSeq hf p b
have h : aeSeq hf p b =ᶠ[ae μ] f b
Tactic: apply EventuallyEq.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
have pos : ∀ (hu : ¬u.NeBot), ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
Tactic: by_cases! hu : ¬ u.NeBot
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
pos : ∀ (hu : ¬u.NeBot), ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
have neg : ∀ (hu : u.NeBot), ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
Tactic: by_cases! hu : ¬ u.NeBot
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
have neg : ∀ (g : ℕ → ι)
  (hg :
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), f (g n) a ∂μ) atTop
        (𝓝 (liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u)) ∧
      Tendsto g atTop u),
  ∫⁻ (a : α), liminf (fun (i : ι) ↦ f i a) u ∂μ ≤ liminf (fun (i : ι) ↦ ∫⁻ (a : α), f i a ∂μ) u
Tactic: obtain ⟨g, hg⟩ : ∃ g : ℕ → ι,
        Tendsto (fun n => ∫⁻ a, f (g n) a ∂μ) atTop (𝓝 (liminf (fun i => ∫⁻ a, f i a ∂μ) u)) ∧
        Tendsto g atTop u :=
      exists_seq_tendsto_liminf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ
have e_f : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ f a) fun (a : α) ↦ ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ f a) fun (a : α) ↦
    ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
have e_f : ∀ (a : α), f a = ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ f a = ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
have e_f : f a = f a
Tactic: rw [iSup_eapprox_apply hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ
have hf₁ : ∀ (n : ℕ), Measurable (α := α) (β := ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
Tactic: apply lintegral_iSup
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hf₁ : ∀ (n : ℕ), Measurable (α := α) (β := ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ
have h_mono : Monotone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) ↦ (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
Tactic: apply lintegral_iSup
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ)
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
have e_s : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ) fun (n : ℕ) ↦
  SimpleFunc.lintegral (eapprox f n) μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ) fun (n : ℕ) ↦
    SimpleFunc.lintegral (eapprox f n) μ
have e_s : ∀ (n : ℕ), ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ = SimpleFunc.lintegral (eapprox f n) μ
Tactic: ext n