awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
⊢ ∀ (n : ℕ), MeasurableSet (sets n)
have refine_1 : ∀ (n : ℕ), MeasurableSet (sigma_finite_sets n)
Tactic: refine fun n => MeasurableSet.inter ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
refine_1 : ∀ (n : ℕ), MeasurableSet (sigma_finite_sets n)
⊢ ∀ (n : ℕ), MeasurableSet (sets n)
have refine_2 : ∀ (n : ℕ), MeasurableSet (norm_sets n)
Tactic: refine fun n => MeasurableSet.inter ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, f x ≤ (↑n : ℝ≥0)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
have h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
Tactic: have h_meas : ∀ n, MeasurableSet (sets n) := by
    refine fun n => MeasurableSet.inter ?_ ?_
    · exact measurableSet_spanningSets μ n
    · exact hf measurableSet_Iic
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
⊢ ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sigma_finite_sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine fun n => (measure_mono Set.inter_subset_left).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, f x ≤ (↑n : ℝ≥0)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
have h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h_finite : ∀ n, μ (sets n) < ∞ := by
    refine fun n => (measure_mono Set.inter_subset_left).trans_lt ?_
    exact measure_spanningSets_lt_top μ n
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, f x ≤ (↑n : ℝ≥0)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
have refine_1 : ∀ (n : ℕ), ∀ x ∈ sets n, f x ≤ (↑n : ℝ≥0)
Tactic: refine ⟨sets, fun n => ⟨h_meas n, h_finite n, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : ∀ (n : ℕ), ∀ x ∈ sets n, f x ≤ (↑n : ℝ≥0)
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, f x ≤ (↑n : ℝ≥0)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
Tactic: refine ⟨sets, fun n => ⟨h_meas n, h_finite n, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
    ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)
have refine : ∀ (i j : ℕ) (hij : i ≤ j), ∀ x ∈ norm_sets i, x ∈ norm_sets j
Tactic: refine Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ norm_sets i → x ∈ norm_sets j
have simp : f x ≤ (↑i : ℝ≥0) → f x ≤ (↑j : ℝ≥0)
Tactic: simp only [norm_sets, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
i j : ℕ
hij : i ≤ j
x : α
⊢ f x ≤ (↑i : ℝ≥0) → f x ≤ (↑j : ℝ≥0)
have refine : ∀ (hif : f x ≤ (↑i : ℝ≥0)), LE.le (α := ℝ≥0) (↑i : ℝ≥0) (↑j : ℝ≥0)
Tactic: refine fun hif => hif.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
have this : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
  ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)
Tactic: have :
      ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i := by
      refine Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => ?_
      simp only [norm_sets, Set.mem_setOf_eq]
      refine fun hif => hif.trans ?_
      exact mod_cast hij
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
    ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
have refine_2 : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i) univ
Tactic: rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
    ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)
refine_2 : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i) univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
have refine_2₁ : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ univ) univ
Tactic: rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
    ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)
refine_2 : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i) univ
refine_2₁ : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ univ) univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
have refine_2₂ : Eq.{u_1 + 1} (α := Set α) (univ ∩ univ) univ
Tactic: rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst : SigmaFinite μ
sigma_finite_sets : (i : ℕ) → Set α := spanningSets μ
norm_sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ {x : α | f x ≤ (↑n : ℝ≥0)}
norm_sets_spanning : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ
sets : (n : ℕ) → Set α := fun (n : ℕ) ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
    ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)
refine_2 : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i) univ
refine_2₁ : Eq.{u_1 + 1} (α := Set α) ((⋃ (i : ℕ), sigma_finite_sets i) ∩ univ) univ
refine_2₂ : Eq.{u_1 + 1} (α := Set α) (univ ∩ univ) univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
have refine_2₃ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) {b}) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[>] 0)
  (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) (⋂ (r : ℝ), ⋂ (_ : r > 0), Icc (b - r) (b + r))) : Filter ℝ≥0∞)
Tactic: rw [Real.singleton_eq_inter_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) (⋂ (r : ℝ), ⋂ (_ : r > 0), Icc (b - r) (b + r))) : Filter ℝ≥0∞)
have hm : ∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)
Tactic: apply tendsto_measure_biInter_gt (fun r hr ↦ nullMeasurableSet_Icc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
hm : ∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) (⋂ (r : ℝ), ⋂ (_ : r > 0), Icc (b - r) (b + r))) : Filter ℝ≥0∞)
have hf : ∃ r > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply tendsto_measure_biInter_gt (fun r hr ↦ nullMeasurableSet_Icc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b - s ≤ b - r
have linarith : b - r < b - s → r - s + (b - r - (b - s)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b + r ≤ b + s
have linarith : b + s < b + r → r - s + (b + s - (b + r)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[≥] 0)
    (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) {b}) : Filter ℝ≥0∞)
have simp : ∀ (s : Set ℝ≥0∞),
  Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) {b}) : Filter ℝ≥0∞) s →
    Membership.mem (α := ℝ≥0∞) s ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - 0) (b + 0)) : ℝ≥0∞)
Tactic: simp only [← nhdsGT_sup_nhdsWithin_singleton, nhdsWithin_singleton, tendsto_sup,
    tendsto_measure_Icc_nhdsWithin_right' μ b, true_and, tendsto_pure_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝 0) (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧
  Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
Tactic: rw [← nhdsLT_sup_nhdsGE, tendsto_sup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧
    Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
have left : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
left : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0) ∧
    Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
have right : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))) (𝓝[<] 0) (𝓝 0)
have left : EventuallyEq (β := ℝ≥0∞) (𝓝[<] 0) (fun (x : ℝ) ↦ 0) fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
⊢ Membership.mem (γ := Set ℝ) (Iio 0) r →
    Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
have h : ∀ (hr : r < 0), Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
Tactic: (hr : r < 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[<] 0) (fun (x : ℝ) ↦ 0) fun (δ : ℝ) ↦ (μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ))
have h : ∀ (r : ℝ) (hr : r < 0), Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin] with r (hr : r < 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
hr : r < 0
⊢ ¬b - r ≤ b + r
have linarith : b - r ≤ b + r → 2 * (r - 0) + (b - r - (b + r)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
hr : r < 0
linarith : b - r ≤ b + r → 2 * (r - 0) + (b - r - (b + r)) = 0
⊢ ¬b - r ≤ b + r
have linarith₁ : b - r ≤ b + r → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
hr : r < 0
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: rw [Icc_eq_empty (by linarith), measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b r : ℝ
hr : r < 0
h : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [Icc_eq_empty (by linarith), measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
⊢ ∅ ∈ closedCompactCylinders X
have simp_rw : ∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
  ∅ = cylinder (α := X) i i_1
Tactic: simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
⊢ t ∈ closedCompactCylinders X ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
have simp_rw : Membership.mem (γ := Set (Set ((i : ι) → X i)))
    (⋃ (s : Finset ι),
      ⋃ (S : Set ((i : ↥s) → X (↑i : ι))), ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {cylinder (α := X) s S})
    t ↔
  ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
Tactic: simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
t : Set ((i : ι) → X i)
simp_rw :
  Membership.mem (γ := Set (Set ((i : ι) → X i)))
      (⋃ (s : Finset ι),
        ⋃ (S : Set ((i : ↥s) → X (↑i : ι))), ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {cylinder (α := X) s S})
      t ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
⊢ t ∈ closedCompactCylinders X ↔
    ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
have simp_rw₁ : (∃ (i : Finset ι) (i_1 : Set ((i_1 : ↥i) → X (↑i_1 : ι))) (_ : IsClosed i_1) (_ : IsCompact i_1),
    Membership.mem (γ := Set (Set ((i : ι) → X i))) {cylinder (α := X) i i_1} t) ↔
  ∃ (s : Finset ι) (S : Set ((i : ↥s) → X (↑i : ι))), IsClosed S ∧ IsCompact S ∧ t = cylinder (α := X) s S
Tactic: simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff, exists_prop]