awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
h₁ : MeasurableSet (f ⁻¹' t ∩ s)
⊢ MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
have h₂ : MeasurableSet (g ⁻¹' t \ s)
Tactic: apply MeasurableSet.union
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
⊢ MeasurableSet (f ⁻¹' t ∩ s)
have h₁ : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s), MeasurableSet (f ⁻¹' t ∩ s)
Tactic: rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (f ⁻¹' t ∩ s)
have h₁ : MeasurableSet (u ∩ s)
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
⊢ MeasurableSet (g ⁻¹' t \ s)
have h₂ : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ), MeasurableSet (g ⁻¹' t \ s)
Tactic: rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (g ⁻¹' t \ s)
have h₂ : MeasurableSet (u ∩ sᶜ)
Tactic: rw [diff_eq_compl_inter, inter_comm, hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
ι : Type u_6
X : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), BorelSpace.{u_7} (X i)
⊢ LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))
have this : inst_1 = fun (i : ι) ↦ borel (X i)
Tactic: have : ‹∀ i, MeasurableSpace (X i)› = fun i => borel (X i) :=
    funext fun i => BorelSpace.measurable_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
ι : Type u_6
X : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), BorelSpace.{u_7} (X i)
this : inst_1 = fun (i : ι) ↦ borel (X i)
⊢ LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))
have rw : LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))
have rw : LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))
Tactic: rw [‹BorelSpace α›.measurable_eq, ‹BorelSpace β›.measurable_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))
have refine_1 : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (borel α)) (borel (α × β))
Tactic: refine sup_le ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
refine_1 : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (borel α)) (borel (α × β))
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))
have refine_2 : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.snd (borel β)) (borel (α × β))
Tactic: refine sup_le ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ BorelSpace α
have measurable_eq : inst = borel α
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ inst = borel α
have this : MeasurableSpace.comap e (borel β) = inst
Tactic: have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst
⊢ inst = borel α
have measurable_eq : MeasurableSpace.comap e (borel β) = borel α
Tactic: rw [← this, ← borel_comap, h''e.eq_induced]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst
measurable_eq : MeasurableSpace.comap e (borel β) = borel α
⊢ inst = borel α
have measurable_eq₁ : borel α = borel α
Tactic: rw [← this, ← borel_comap, h''e.eq_induced]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst
measurable_eq : MeasurableSpace.comap e (borel β) = borel α
measurable_eq₁ : borel α = borel α
⊢ inst = borel α
have measurable_eq₂ : borel α = borel α
Tactic: rw [← this, ← borel_comap, h''e.eq_induced]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α_1
inst : TopologicalSpace α_1
mα : MeasurableSpace α_1
inst_1 : BorelSpace α_1
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
α : Type u_6
inst_8 : TopologicalSpace α
inst_9 : DiscreteTopology α
inst_10 : MeasurableSpace α
inst_11 : DiscreteMeasurableSpace α
⊢ BorelSpace α
have measurable_eq : inst_10 = borel α
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α_1
inst : TopologicalSpace α_1
mα : MeasurableSpace α_1
inst_1 : BorelSpace α_1
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
α : Type u_6
inst_8 : TopologicalSpace α
inst_9 : DiscreteTopology α
inst_10 : MeasurableSpace α
inst_11 : DiscreteMeasurableSpace α
⊢ inst_10 = borel α
have measurable_eq : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
⊢ IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_2) (map (⇑f : (a : α) → β) μ)
have refine : ∀ (K : Set β) (hK : IsCompact K),
  LT.lt (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fun K hK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f.toMeasurableEquiv : (a : α) → β) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← f.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
⊢ Measurable (edist x)
have funProp : inst_1 ≤ inst_1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
funProp : inst_1 ≤ inst_1
⊢ Measurable (edist x)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a : α) ↦ edist x a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ edist y x
have funProp : inst_1 ≤ inst_1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
x : α
funProp : inst_1 ≤ inst_1
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ edist y x
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (y : α) ↦ edist y x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ s)) : Filter ℝ≥0∞)
Tactic: rw [closure_eq_iInter_cthickening]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
have A : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
Tactic: have A : Tendsto (fun r => μ (cthickening r s)) (𝓝[Ioi 0] 0) (𝓝 (μ (closure s))) := by
    rw [closure_eq_iInter_cthickening]
    exact
      tendsto_measure_biInter_gt (fun r _ => isClosed_cthickening.nullMeasurableSet)
        (fun i j _ ij => cthickening_mono ij _) hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
have apply : EventuallyEq (β := ℝ≥0∞) (𝓝[≤] 0)
  (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s))
  fun (r : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (cthickening r s)
Tactic: apply Tendsto.congr' _ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[≤] 0)
    (fun (x : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s))
    fun (r : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) (cthickening r s)
have h : ∀ (a : ℝ) (hr : Membership.mem (γ := Set ℝ) (Iic 0) a),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (cthickening a s) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
a : ℝ
hr : Membership.mem (γ := Set ℝ) (Iic 0) a
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (cthickening a s) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
Tactic: rw [cthickening_of_nonpos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
have B : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
Tactic: have B : Tendsto (fun r => μ (cthickening r s)) (𝓝[Iic 0] 0) (𝓝 (μ (closure s))) := by
    apply Tendsto.congr' _ tendsto_const_nhds
    filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr
    rw [cthickening_of_nonpos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝[≤] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
have h : Eq (α := Filter ℝ) (𝓝 0) (𝓝[≤] 0 ⊔ 𝓝[>] 0)
Tactic: convert! B.sup A
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (cthickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have h : s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: convert! tendsto_measure_cthickening hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s)) : Filter ℝ≥0∞)
Tactic: rw [closure_eq_iInter_thickening]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (thickening R s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h's : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (thickening r s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have h : s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: convert! tendsto_measure_thickening hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablyGenerated α
inst_1 : MeasurableSpace.SeparatesPoints α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
have rcases : ∀ (s : Set (ℕ → Bool)) (f : α ≃ᵐ (↑s : Type)),
  ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
Tactic: rcases measurableEquiv_nat_bool_of_countablyGenerated α with ⟨s, ⟨f⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablySeparated α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
have rcases : ∀ (m' : MeasurableSpace α),
  CountablyGenerated α →
    MeasurableSpace.SeparatesPoints α →
      ∀ (m'le : m' ≤ m), ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
Tactic: rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (goal)
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
have rcases : ∀ (τ : TopologicalSpace α),
  SecondCountableTopology α →
    T4Space α →
      ∀ (τm' : BorelSpace α), ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
Tactic: rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable g
have hf₁ : ∀ (s : Set β), IsClosed[inst_1] s → s.Nonempty → s ≠ Set.univ → MeasurableSet (g ⁻¹' s)
Tactic: apply measurable_of_isClosed'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
have suffices : Tendsto.{u_3, u_1} (β := (x : α) → ℝ≥0) (fun (i : ι) (x : α) ↦ infNndist (f i x) s) u
  (𝓝 fun (x : α) ↦ infNndist (g x) s)
Tactic: suffices Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s) from
      NNReal.measurable_of_tendsto' u (fun i => (hf i).infNndist) this