awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
⊢ ∀ s ∈ f, IsOpen[t] s
have rwa : ∀ s_1 ∈ f, IsOpen[TopologicalSpace.generateFrom s] s_1
Tactic: rwa [hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
⊢ MeasurableSet (⋃₀ f)
have sUnion : ∀ (v : Set (Set α)) (hv : v.Countable) (vf : v ⊆ f) (vu : ⋃₀ v = ⋃₀ f), MeasurableSet (⋃₀ f)
Tactic: rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
v : Set (Set α)
hv : v.Countable
vf : v ⊆ f
vu : ⋃₀ v = ⋃₀ f
⊢ MeasurableSet (⋃₀ f)
have sUnion : MeasurableSet (⋃₀ v)
Tactic: rw [← vu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
⊢ MeasurableSet u
have basic : ∀ (u : Set α) (hu : u ∈ s), MeasurableSet u
Tactic: induction hu with
      | basic u hu => exact GenerateMeasurable.basic u hu
      | univ => exact @MeasurableSet.univ α (generateFrom s)
      | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
      | sUnion f hf ih =>
        rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
        rw [← vu]
        exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
basic : ∀ (u : Set α) (hu : u ∈ s), MeasurableSet u
⊢ MeasurableSet u
have univ : MeasurableSet.{u_1} (α := α) univ
Tactic: induction hu with
      | basic u hu => exact GenerateMeasurable.basic u hu
      | univ => exact @MeasurableSet.univ α (generateFrom s)
      | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
      | sUnion f hf ih =>
        rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
        rw [← vu]
        exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
basic : ∀ (u : Set α) (hu : u ∈ s), MeasurableSet u
univ : MeasurableSet.{u_1} (α := α) Set.univ
⊢ MeasurableSet u
have inter : ∀ (s₁ s₂ : Set α),
  GenerateOpen s s₁ → GenerateOpen s s₂ → ∀ (hs₁ : MeasurableSet s₁) (hs₂ : MeasurableSet s₂), MeasurableSet (s₁ ∩ s₂)
Tactic: induction hu with
      | basic u hu => exact GenerateMeasurable.basic u hu
      | univ => exact @MeasurableSet.univ α (generateFrom s)
      | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
      | sUnion f hf ih =>
        rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
        rw [← vu]
        exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : TopologicalSpace.IsOpen u
basic : ∀ (u : Set α) (hu : u ∈ s), MeasurableSet u
univ : MeasurableSet.{u_1} (α := α) Set.univ
inter :
  ∀ (s₁ s₂ : Set α),
    GenerateOpen s s₁ → GenerateOpen s s₂ → ∀ (hs₁ : MeasurableSet s₁) (hs₂ : MeasurableSet s₂), MeasurableSet (s₁ ∩ s₂)
⊢ MeasurableSet u
have sUnion : ∀ (f : Set (Set α)) (hf : ∀ s_1 ∈ f, GenerateOpen s s_1) (ih : ∀ s_1 ∈ f, MeasurableSet s_1), MeasurableSet (⋃₀ f)
Tactic: induction hu with
      | basic u hu => exact GenerateMeasurable.basic u hu
      | univ => exact @MeasurableSet.univ α (generateFrom s)
      | inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
      | sUnion f hf ih =>
        rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
        rw [← vu]
        exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv)
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
hu : u ∈ s
⊢ TopologicalSpace.IsOpen u
have rw : TopologicalSpace.IsOpen u
Tactic: rw [hs]
-- 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
α : Type u_6
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
hα : BorelSpace α
p : α → Prop
⊢ Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (instMeasurableSpace (p := p)) (borel (Subtype p))
have borelize : ∀ [hα : BorelSpace α],
  Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (instMeasurableSpace (p := p)) (borel (Subtype p))
Tactic: borelize α
Cleared hypotheses: inst_1, hα
-- 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
α : Type u_6
inst : TopologicalSpace α
p : α → Prop
hα : BorelSpace α
this : MeasurableSpace α := borel α
⊢ Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (instMeasurableSpace (p := p)) (borel (Subtype p))
have symm : Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (borel (Subtype p)) (instMeasurableSpace (p := p))
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
inst_3 : TopologicalSpace α
inst_4 : DiscreteTopology α
⊢ BorelSpace α
have this : ∀ (s : Set α), MeasurableSet s
Tactic: have : ∀ s, @MeasurableSet α inferInstance s := fun s ↦ s.to_countable.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : Countable α
inst_1 : MeasurableSpace α
inst_2 : MeasurableSingletonClass α
inst_3 : TopologicalSpace α
inst_4 : DiscreteTopology α
this : ∀ (s : Set α), MeasurableSet s
⊢ BorelSpace α
have this₁ : ∀ (s : Set α), MeasurableSet s
Tactic: have : ∀ s, @MeasurableSet α (borel α) s := fun s ↦ measurableSet_generateFrom (isOpen_discrete s)
-- 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
α : Type u_6
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
h : OpensMeasurableSpace α
p : α → Prop
⊢ LE.le.{u_6} (α := MeasurableSpace (Subtype p)) (borel (Subtype p)) (instMeasurableSpace (p := p))
have rw : LE.le (α := MeasurableSpace (Subtype p)) (MeasurableSpace.comap (val (p := p)) (borel α)) (instMeasurableSpace (p := p))
Tactic: rw [borel_comap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
⊢ OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen[inst] s → MeasurableSet s
have refine : ∀ (h : OpensMeasurableSpace α) (s : Set α) (hs : IsOpen[inst] s), MeasurableSet s
Tactic: refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩
-- 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
α : Type u_6
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : SecondCountableTopology α
⊢ CountablyGenerated α
have obtain : ∀ (b : Set (Set α)) (bct : b.Countable) (hb : IsTopologicalBasis b), CountablyGenerated α
Tactic: obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α
-- 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
α : Type u_6
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
⊢ CountablyGenerated α
have refine : inst_1 = MeasurableSpace.generateFrom b
Tactic: refine ⟨⟨b, bct, ?_⟩⟩
-- 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
α : Type u_6
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
⊢ inst_1 = MeasurableSpace.generateFrom b
have borelize : ∀ [BorelSpace α], borel α = MeasurableSpace.generateFrom b
Tactic: borelize α
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s_1 t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
s : Set α
h : HasCountableSeparatingOn α IsOpen[inst] s
⊢ CountablySeparated.{u_1} (↑s : Type u_1)
have rw : HasCountableSeparatingOn α MeasurableSet s
Tactic: rw [CountablySeparated.subtype_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
h : IsGδ s
⊢ MeasurableSet s
have rcases : ∀ (S : Set (Set α)) (hSo : ∀ t ∈ S, IsOpen[inst] t) (hSc : S.Countable), MeasurableSet (⋂₀ S)
Tactic: rcases h with ⟨S, hSo, hSc, rfl⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : R1Space γ
K s : Set γ
hK : IsCompact K
hs : MeasurableSet s
hKs : K ⊆ s
⊢ closure[inst] K ⊆ s
have rw : ∀ (i : γ) (j : i ∈ K), {y : γ | Inseparable i y} ⊆ s
Tactic: rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (closure[inst] K) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) K : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (closure[inst] K) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: refine le_antisymm ?_ (measure_mono subset_closure)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen[inst] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
have rw : Measurable f
Tactic: rw [‹BorelSpace γ›.measurable_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
have hf₁ : ∀ (s : Set γ), IsOpen[inst] s → MeasurableSet (f ⁻¹' s)
Tactic: apply measurable_of_isOpen
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst] s
⊢ MeasurableSet (f ⁻¹' s)
have hf₁ : MeasurableSet (f ⁻¹' sᶜ)
Tactic: rw [← MeasurableSet.compl_iff, ← preimage_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsOpen[inst] s
⊢ MeasurableSet (f ⁻¹' sᶜ)
have hf₁ : IsClosed[inst] sᶜ
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
⊢ Measurable f
have hf₁ : ∀ (s : Set γ), IsClosed[inst] s → MeasurableSet (f ⁻¹' s)
Tactic: apply measurable_of_isClosed
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
⊢ MeasurableSet (f ⁻¹' s)
have hf₁ : ∀ (h1 : s = ∅), MeasurableSet (f ⁻¹' s)
Tactic: rcases eq_empty_or_nonempty s with h1 | h1
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
hf₁ : ∀ (h1 : s = ∅), MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet (f ⁻¹' s)
have hf₂ : ∀ (h1 : s.Nonempty), MeasurableSet (f ⁻¹' s)
Tactic: rcases eq_empty_or_nonempty s with h1 | h1
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s.Nonempty
⊢ MeasurableSet (f ⁻¹' s)
have pos : ∀ (h2 : s = univ), MeasurableSet (f ⁻¹' s)
Tactic: by_cases h2 : s = univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsClosed[inst] s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)
s : Set γ
hs : IsClosed[inst] s
h1 : s.Nonempty
pos : ∀ (h2 : s = univ), MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet (f ⁻¹' s)
have neg : ∀ (h2 : ¬s = univ), MeasurableSet (f ⁻¹' s)
Tactic: by_cases h2 : s = univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
a : α
⊢ (𝓝 a).IsMeasurablyGenerated
have rw : IsMeasurablyGenerated.{u_1} (α := α)
  (⨅ (x : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})), 𝓟 (↑x : Set α))
Tactic: rw [nhds, iInf_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
a : α
⊢ IsMeasurablyGenerated.{u_1} (α := α)
    (⨅ (x : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})), 𝓟 (↑x : Set α))
have refine : ∀ (i : Subtype (Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[inst] s})),
  (𝓟 (↑i : Set α)).IsMeasurablyGenerated
Tactic: refine @Filter.iInf_isMeasurablyGenerated α _ _ _ fun i => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
inst_13 : T0Space α
⊢ MeasurableSpace.SeparatesPoints α
have rw : ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
Tactic: rw [separatesPoints_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
inst_13 : T0Space α
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y
have h : Inseparable x y
Tactic: apply Inseparable.eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
inst_13 : T0Space α
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ Inseparable x y
have h : ∀ (s : Set α), IsOpen[inst] s → (x ∈ s ↔ y ∈ s)
Tactic: rw [inseparable_iff_forall_isOpen]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
⊢ borel α = ⊤
have refine : ∀ (s : Set α), MeasurableSet s → MeasurableSet s
Tactic: refine top_unique fun s _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
α : Type u_6
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : Countable α
s : Set α
h : MeasurableSet s
⊢ MeasurableSet s
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
⊢ OpensMeasurableSpace ((i : ι) → X i)
have borel_le : LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst_13 : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst_14 : (i : ι) → MeasurableSpace (X i)
inst_15 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_16 : ∀ (i : ι), OpensMeasurableSpace.{u_7} (X i)
⊢ LE.le (α := MeasurableSpace ((i : ι) → X i)) (borel ((i : ι) → X i)) (MeasurableSpace.pi (X := X))
have this : Eq (α := TopologicalSpace ((i : ι) → X i)) (topologicalSpace (Y := X))
  (TopologicalSpace.generateFrom
    {t : Set ((i : ι) → X i) |
      ∃ (s : (a : ι) → Set (X a)) (i : Finset ι),
        (∀ a ∈ i, Membership.mem (γ := Set (Set (X a))) (countableBasis (X a)) (s a)) ∧ t = (↑i : Set ι).pi (α := X) s})
Tactic: have : Pi.topologicalSpace = .generateFrom { t | ∃ (s : ∀ a, Set (X a)) (i : Finset ι),
      (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = pi (↑i) s } := by
    simp +instances only [funext fun a => @eq_generateFrom_countableBasis (X a) _ _,
      pi_generateFrom_eq]