awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)}
x : α
⊢ ∃ (i : ℕ), x ∈ norm_sets i

Tactic:
exact exists_nat_ge (f x)

Premises used: exists_nat_ge
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)}
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), norm_sets n) univ

Tactic:
have norm_sets_spanning : ⋃ n, norm_sets n = Set.univ := by
    ext1 x
    simp only [Set.mem_iUnion, Set.mem_univ, iff_true]
    exact exists_nat_ge (f x)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)

Tactic:
fun n => MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)
refine_2 : ∀ (n : ℕ), MeasurableSet (norm_sets n)
⊢ ∀ (n : ℕ), MeasurableSet (sets n)

Tactic:
refine fun n => MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 (sigma_finite_sets n)

Tactic:
measurableSet_spanningSets μ n

Premises used: MeasureTheory.measurableSet_spanningSets
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 (sigma_finite_sets n)

Tactic:
exact measurableSet_spanningSets μ n

Premises used: MeasureTheory.measurableSet_spanningSets
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 (norm_sets n)

Tactic:
hf measurableSet_Iic

Premises used: Set.Mem, setOf, measurableSet_Iic, Set.preimage, Set.Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 (norm_sets n)

Tactic:
exact hf measurableSet_Iic

Premises used: measurableSet_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)

Tactic:
have h_meas : ∀ n, MeasurableSet (sets n) := by
    refine fun n => MeasurableSet.inter ?_ ?_
    · exact measurableSet_spanningSets μ n
    · exact hf measurableSet_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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∞)

Tactic:
fun n => (measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)
refine : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sigma_finite_sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine fun n => (measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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∞) (sigma_finite_sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_spanningSets_lt_top μ n

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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∞) (sigma_finite_sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_spanningSets_lt_top μ n

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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∞)

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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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

Tactic:
⟨sets, fun n => ⟨h_meas n, h_finite n, ?_⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)
refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ
⊢ ∃ (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

Tactic:
refine ⟨sets, fun n => ⟨h_meas n, h_finite n, ?_⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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∞)
n : ℕ
⊢ ∀ x ∈ sets n, f x ≤ (↑n : ℝ≥0)

Tactic:
fun x hx => hx.2

Premises used: Set.Mem, setOf, And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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∞)
n : ℕ
⊢ ∀ x ∈ sets n, f x ≤ (↑n : ℝ≥0)

Tactic:
exact fun x hx => hx.2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)

Tactic:
Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => ?_

Premises used: MeasureTheory.monotone_spanningSets, Set.iUnion_inter_of_monotone
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 : ∀ (i j : ℕ) (hij : i ≤ j), ∀ x ∈ norm_sets i, x ∈ norm_sets j
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sigma_finite_sets i ∩ norm_sets i)
    ((⋃ (i : ℕ), sigma_finite_sets i) ∩ ⋃ (i : ℕ), norm_sets i)

Tactic:
refine Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => ?_

Premises used: MeasureTheory.monotone_spanningSets, Set.iUnion_inter_of_monotone
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 : α
simp : f x ≤ (↑i : ℝ≥0) → f x ≤ (↑j : ℝ≥0)
⊢ x ∈ norm_sets i → x ∈ norm_sets j

Tactic:
simp only [norm_sets, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)

Tactic:
fun hif => hif.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 : α
refine : ∀ (hif : f x ≤ (↑i : ℝ≥0)), LE.le (α := ℝ≥0) (↑i : ℝ≥0) (↑j : ℝ≥0)
⊢ f x ≤ (↑i : ℝ≥0) → f x ≤ (↑j : ℝ≥0)

Tactic:
refine fun hif => hif.trans ?_
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 : α
hif : f x ≤ (↑i : ℝ≥0)
⊢ LE.le (α := ℝ≥0) (↑i : ℝ≥0) (↑j : ℝ≥0)

Tactic:
mod_cast hij

Premises used: cast, Nat.cast_le._simp_1, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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 : α
hif : f x ≤ (↑i : ℝ≥0)
⊢ LE.le (α := ℝ≥0) (↑i : ℝ≥0) (↑j : ℝ≥0)

Tactic:
exact mod_cast hij
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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)

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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
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
refine_2₃ refine_2₄ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), sets i) univ

Tactic:
rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]

Premises used: Set.inter_univ, MeasureTheory.iUnion_spanningSets
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) {b}) : Filter ℝ≥0∞)

Tactic:
rw [Real.singleton_eq_inter_Icc]

Premises used: Real.singleton_eq_inter_Icc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
hm : ∀ (i j : ℝ), 0 < i → i ≤ j → Icc (b - i) (b + i) ⊆ Icc (b - j) (b + j)
hf : ∃ r > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 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:
apply tendsto_measure_biInter_gt (fun r hr ↦ nullMeasurableSet_Icc)

Premises used: nullMeasurableSet_Icc, MeasureTheory.tendsto_measure_biInter_gt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
linarith : b - r < b - s → r - s + (b - r - (b - s)) = 0
⊢ b - s ≤ b - r

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
linarith : b + s < b + r → r - s + (b + s - (b + r)) = 0
⊢ b + r ≤ b + s

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ Icc (b - r) (b + r) ⊆ Icc (b - s) (b + s)

Tactic:
exact Icc_subset_Icc (by linarith) (by linarith)

Premises used: Set.Icc_subset_Icc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∃ r > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩

Premises used: CompactIccSpace.isCompact_Icc, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∃ r > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - r) (b + r)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
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∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((μ : (a : Set ℝ) → ℝ≥0∞) (Icc (b - δ) (b + δ)) : ℝ≥0∞)) (𝓝[≥] 0)
    (𝓝 ((μ : (a : Set ℝ) → ℝ≥0∞) {b}) : Filter ℝ≥0∞)

Tactic:
simp only [← nhdsGT_sup_nhdsWithin_singleton, nhdsWithin_singleton, tendsto_sup,
    tendsto_measure_Icc_nhdsWithin_right' μ b, true_and, tendsto_pure_left]

Premises used: nhdsWithin_singleton, Filter.tendsto_pure_left, Filter.tendsto_sup, tendsto_measure_Icc_nhdsWithin_right', nhdsGT_sup_nhdsWithin_singleton, true_and
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
b : ℝ
s : Set ℝ≥0∞
hs : 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:
simpa using mem_of_mem_nhds hs

Premises used: mem_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
μ : Measure ℝ
inst : IsFiniteMeasureOnCompacts μ
inst_1 : NoAtoms μ
b : ℝ
rw :
  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)

Tactic:
rw [← nhdsLT_sup_nhdsGE, tendsto_sup]

Premises used: nhdsLT_sup_nhdsGE, Filter.tendsto_sup