awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
hinf :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
hsup :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
h :
  autoParam (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) L fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E)
    tendsto_of_le_liminf_of_limsup_le._auto_1
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μs i : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
have h' : autoParam (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) L fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E)
  tendsto_of_le_liminf_of_limsup_le._auto_3
Tactic: apply tendsto_of_le_liminf_of_limsup_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞) (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞)
have E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
Tactic: have E₀_ae_eq_E : E₀ =ᵐ[μ] E :=
      EventuallyLE.antisymm E₀_subset.eventuallyLE
        (subset_E₁.eventuallyLE.trans (ae_le_set.mpr nulldiff))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (E₁ \ E₀) : ℝ≥0∞) (0 : ℝ≥0∞)
h_E₀ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E₀ : ℝ≥0∞)
    (liminf (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₀) L : ℝ≥0∞)
h_E₁ :
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E₁) L : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) E₁ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) E) L : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) E : ℝ≥0∞)
have E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
Tactic: have E_ae_eq_E₁ : E =ᵐ[μ] E₁ :=
      EventuallyLE.antisymm subset_E₁.eventuallyLE
        ((ae_le_set.mpr nulldiff).trans E₀_subset.eventuallyLE)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have inl : ∀ (μs_lim : Tendsto μs ⊥ (𝓝 μ)),
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) ⊥ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | hne
Cleared hypotheses: L, μs_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
inl :
  ∀ (μs_lim : Tendsto μs ⊥ (𝓝 μ)),
    LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) ⊥ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have inr : ∀ (hne : L.NeBot),
  LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: rcases L.eq_or_neBot with rfl | hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have inr : ∀ (ε : ℝ≥0),
  0 < ε →
    LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞) →
      limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
        HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: apply ENNReal.le_of_forall_pos_le_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
Tactic: have ε_pos' := (ENNReal.half_pos (ENNReal.coe_ne_zero.mpr ε_pos.ne.symm)).ne.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have key₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
  (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: have key₁ : Tendsto (fun n ↦ ∫⁻ ω, (fs n ω : ℝ≥0∞) ∂μ) atTop (𝓝 ((μ : Measure Ω) F)) :=
    HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed (μ : Measure Ω)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have room₁ : ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
  HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
Tactic: have room₁ : (μ : Measure Ω) F < (μ : Measure Ω) F + ε / 2 :=
    ENNReal.lt_add_right (measure_lt_top (μ : Measure Ω) F).ne ε_pos'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inr : ∀ (M : ℕ)
  (hM :
    ∀ b ≥ M,
      ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
        HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)),
  limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have key₂ : Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
  (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
Tactic: have key₂ := FiniteMeasure.tendsto_iff_forall_lintegral_tendsto.mp μs_lim (fs M)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have room₂ : ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
Tactic: have room₂ :
    (lintegral (μ : Measure Ω) fun a ↦ fs M a) <
      (lintegral (μ : Measure Ω) fun a ↦ fs M a) + ε / 2 :=
    ENNReal.lt_add_right (ne_of_lt ((fs M).lintegral_lt_top_of_nnreal _)) ε_pos'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have ev_near : ∀ᶠ (a : ι) in L,
  ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
Tactic: have ev_near := key₂.eventually_le_const room₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have ev_near' : ∀ᶠ (x : ι) in L,
  ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
Tactic: have ev_near' := ev_near.mono
    (fun n ↦ le_trans (HasOuterApproxClosed.measure_le_lintegral F_closed (μs n) M))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
⊢ limsup (fun (i : ι) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inr : limsup (fun (x : ι) ↦ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2) L ≤
  HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: apply (Filter.limsup_le_limsup ev_near').trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
⊢ limsup (fun (x : ι) ↦ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2) L ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inr : ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2 ≤
  HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: rw [limsup_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst_1] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
h : LT.lt (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (∞ : ℝ≥0∞)
ε_pos' : (↑ε : ℝ≥0∞) / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq (F := F)
key₁ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
room₁ :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F <
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
M : ℕ
hM :
  ∀ b ≥ M,
    ∫⁻ (ω : Ω), (↑((fs b : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2)
key₂ :
  Tendsto (fun (i : ι) ↦ ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
room₂ :
  ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) <
    ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near :
  ∀ᶠ (a : ι) in L,
    ∫⁻ (x : Ω), (↑((fs M : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs a) : Measure Ω) ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
ev_near' :
  ∀ᶠ (x : ι) in L,
    ((↑(μs x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F ≤
      ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2
⊢ ∫⁻ (a : Ω), (↑((fs M : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ∂(↑μ : Measure Ω) + (↑ε : ℝ≥0∞) / 2 ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
have inr : HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((↑ε : ℝ≥0∞) / 2) + (↑ε : ℝ≥0∞) / 2 ≤
  HAdd.hAdd (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) (↑ε : ℝ≥0∞)
Tactic: apply le_trans (add_le_add (hM M rfl.le).le (le_refl (ε / 2 : ℝ≥0∞)))