awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ borel α = MeasurableSpace.generateFrom {s : Set α | IsClosed[inst] s}

Tactic:
le_antisymm
    (generateFrom_le fun _t ht =>
      @MeasurableSet.of_compl α _ (generateFrom { s | IsClosed s })
        (GenerateMeasurable.basic _ <| isClosed_compl_iff.2 ht))
    (generateFrom_le fun _t ht =>
      @MeasurableSet.of_compl α _ (borel α) (GenerateMeasurable.basic _ <| isOpen_compl_iff.2 ht))

Premises used: Iff.mpr, MeasurableSet.of_compl, Compl.compl, MeasurableSpace.GenerateMeasurable.basic, le_antisymm, isOpen_compl_iff, MeasurableSpace.generateFrom_le, isClosed_compl_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : TopologicalSpace β
⊢ borel α = MeasurableSpace.comap f (borel β)

Tactic:
comap_generateFrom.symm

Premises used: Set.Mem, setOf, Set.image, IsOpen, Eq.symm, MeasurableSpace.comap_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ Measurable f

Tactic:
Measurable.of_le_map <|
    generateFrom_le fun s hs => GenerateMeasurable.basic (f ⁻¹' s) (hs.preimage hf)

Premises used: Measurable.of_le_map, MeasurableSpace.GenerateMeasurable.basic, Set.preimage, IsOpen.preimage, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 α
⊢ OpensMeasurableSpace α

Tactic:
⟨ge_of_eq <| BorelSpace.measurable_eq⟩

Premises used: BorelSpace.measurable_eq, ge_of_eq, OpensMeasurableSpace.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
borelize :
  ∀ [hα : BorelSpace α],
    Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (instMeasurableSpace (p := p)) (borel (Subtype p))
⊢ Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (instMeasurableSpace (p := p)) (borel (Subtype p))

Tactic:
borelize α
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 α
symm : Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (borel (Subtype p)) (instMeasurableSpace (p := p))
⊢ Eq.{u_6 + 1} (α := MeasurableSpace (Subtype p)) (instMeasurableSpace (p := p)) (borel (Subtype p))

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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)) (borel (Subtype p)) (instMeasurableSpace (p := p))

Tactic:
apply borel_comap

Premises used: borel_comap
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 α
⊢ ∀ (s : Set α), MeasurableSet s

Tactic:
have : ∀ s, @MeasurableSet α inferInstance s := fun s ↦ s.to_countable.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
⊢ ∀ (s : Set α), MeasurableSet s

Tactic:
have : ∀ s, @MeasurableSet α (borel α) s := fun s ↦ measurableSet_generateFrom (isOpen_discrete s)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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_1 : ∀ (s : Set α), MeasurableSet s
this : ∀ (s : Set α), MeasurableSet s
⊢ inst_1 = borel α

Tactic:
aesop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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_1 : ∀ (s : Set α), MeasurableSet s
this : ∀ (s : Set α), MeasurableSet s
⊢ BorelSpace α

Tactic:
exact ⟨by aesop⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
rw :
  LE.le (α := MeasurableSpace (Subtype p)) (MeasurableSpace.comap (val (p := p)) (borel α))
    (instMeasurableSpace (p := p))
⊢ LE.le.{u_6} (α := MeasurableSpace (Subtype p)) (borel (Subtype p)) (instMeasurableSpace (p := p))

Tactic:
rw [borel_comap]

Premises used: borel_comap
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 (α := MeasurableSpace (Subtype p)) (MeasurableSpace.comap (val (p := p)) (borel α))
    (instMeasurableSpace (p := p))

Tactic:
comap_mono h.1

Premises used: MeasurableSpace.comap_mono, OpensMeasurableSpace.borel_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 (α := MeasurableSpace (Subtype p)) (MeasurableSpace.comap (val (p := p)) (borel α))
    (instMeasurableSpace (p := p))

Tactic:
exact comap_mono h.1

Premises used: MeasurableSpace.comap_mono, OpensMeasurableSpace.borel_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
⊢ OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen[inst] s → MeasurableSet s

Tactic:
⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩

Premises used: OpensMeasurableSpace.mk, Iff.intro, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
refine : ∀ (h : OpensMeasurableSpace α) (s : Set α) (hs : IsOpen[inst] s), MeasurableSet s
⊢ OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen[inst] s → MeasurableSet s

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
h : OpensMeasurableSpace α
s : Set α
hs : IsOpen[inst] s
⊢ MeasurableSet s

Tactic:
OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs

Premises used: OpensMeasurableSpace.borel_le, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
h : OpensMeasurableSpace α
s : Set α
hs : IsOpen[inst] s
⊢ MeasurableSet s

Tactic:
exact OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs

Premises used: OpensMeasurableSpace.borel_le, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 α
obtain : ∀ (b : Set (Set α)) (bct : b.Countable) (hb : IsTopologicalBasis b), CountablyGenerated α
⊢ CountablyGenerated α

Tactic:
obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α

Premises used: TopologicalSpace.exists_countable_basis
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 α

Tactic:
⟨⟨b, bct, ?_⟩⟩

Premises used: MeasurableSpace.CountablyGenerated.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
refine : inst_1 = MeasurableSpace.generateFrom b
⊢ CountablyGenerated α

Tactic:
refine ⟨⟨b, bct, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
borelize : ∀ [BorelSpace α], borel α = MeasurableSpace.generateFrom b
⊢ inst_1 = MeasurableSpace.generateFrom b

Tactic:
borelize α
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
inst_2 : BorelSpace α
this : MeasurableSpace α := borel α
⊢ borel α = MeasurableSpace.generateFrom b

Tactic:
hb.borel_eq_generateFrom

Premises used: TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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 : SecondCountableTopology α
b : Set (Set α)
bct : b.Countable
hb : IsTopologicalBasis b
inst_2 : BorelSpace α
this : MeasurableSpace α := borel α
⊢ borel α = MeasurableSpace.generateFrom b

Tactic:
exact hb.borel_eq_generateFrom

Premises used: TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
h : IsOpen[inst] s
⊢ MeasurableSet s

Tactic:
OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ h

Premises used: OpensMeasurableSpace.borel_le, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
h : IsOpen[inst] s
⊢ NullMeasurableSet s μ

Tactic:
h.measurableSet.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
C : (s : Set γ) → MeasurableSet s → Prop
isOpen : ∀ (U : Set γ) (hU : IsOpen[inst] U), C U ⋯
compl : ∀ (t : Set γ) (ht : MeasurableSet t), C t ht → C tᶜ ⋯
iUnion :
  ∀ (f : ℕ → Set γ),
    Pairwise (Disjoint on f) → ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯
⊢ ∀ (t : Set γ) (ht : MeasurableSet t), C t ht

Tactic:
fun t ht ↦
  MeasurableSpace.induction_on_inter BorelSpace.measurable_eq isPiSystem_isOpen
    (isOpen _ isOpen_empty) isOpen compl iUnion t ht

Premises used: BorelSpace.measurable_eq, MeasurableSpace.induction_on_inter, isPiSystem_isOpen
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
rw : HasCountableSeparatingOn α MeasurableSet s
⊢ CountablySeparated.{u_1} (↑s : Type u_1)

Tactic:
rw [CountablySeparated.subtype_iff]

Premises used: MeasurableSpace.CountablySeparated.subtype_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
.mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl

Premises used: HasCountableSeparatingOn.mono, IsOpen.measurableSet, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
⊢ HasCountableSeparatingOn α MeasurableSet s

Tactic:
exact .mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
⊢ MeasurableSet (interior s)

Tactic:
isOpen_interior.measurableSet

Premises used: isOpen_interior, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
h : IsGδ s
rcases : ∀ (S : Set (Set α)) (hSo : ∀ t ∈ S, IsOpen[inst] t) (hSc : S.Countable), MeasurableSet (⋂₀ S)
⊢ MeasurableSet s

Tactic:
rcases h with ⟨S, hSo, hSc, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
S : Set (Set α)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSc : S.Countable
⊢ MeasurableSet (⋂₀ S)

Tactic:
MeasurableSet.sInter hSc fun t ht => (hSo t ht).measurableSet

Premises used: MeasurableSet.sInter, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
S : Set (Set α)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSc : S.Countable
⊢ MeasurableSet (⋂₀ S)

Tactic:
exact MeasurableSet.sInter hSc fun t ht => (hSo t ht).measurableSet

Premises used: MeasurableSet.sInter, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
β : Type u_6
inst_3 : PseudoEMetricSpace β
f : α → β
⊢ MeasurableSet.{u_1} (α := α) {x : α | ContinuousAt f x}

Tactic:
(IsGδ.setOf_continuousAt f).measurableSet

Premises used: IsGδ.setOf_continuousAt, IsGδ.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
h : IsClosed[inst] s
⊢ MeasurableSet s

Tactic:
h.isOpen_compl.measurableSet.of_compl

Premises used: MeasurableSet.of_compl, IsClosed.isOpen_compl, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
μ : Measure α
h : IsClosed[inst] s
⊢ NullMeasurableSet s μ

Tactic:
h.measurableSet.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : T2Space α
h : IsCompact s
⊢ MeasurableSet s

Tactic:
h.isClosed.measurableSet

Premises used: IsClosed.measurableSet, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : T2Space α
μ : Measure α
h : IsCompact s
⊢ NullMeasurableSet s μ

Tactic:
h.isClosed.nullMeasurableSet

Premises used: IsClosed.nullMeasurableSet, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
x y : γ
h_1 : Inseparable x y
s : Set γ
hs : MeasurableSet s
x_1 : ℕ → Set γ
h_2 : Pairwise (Function.onFun Disjoint x_1)
h_3 : ∀ (i : ℕ), MeasurableSet (x_1 i)
h : ∀ (i : ℕ), x ∈ x_1 i ↔ y ∈ x_1 i
⊢ Membership.mem (γ := Set γ) (⋃ (i : ℕ), x_1 i) x ↔ Membership.mem (γ := Set γ) (⋃ (i : ℕ), x_1 i) y

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
rw : ∀ (i : γ) (j : i ∈ K), {y : γ | Inseparable i y} ⊆ s
⊢ closure[inst] K ⊆ s

Tactic:
rw [hK.closure_eq_biUnion_inseparable, iUnion₂_subset_iff]

Premises used: IsCompact.closure_eq_biUnion_inseparable, Set.iUnion₂_subset_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
⊢ ∀ (i : γ) (j : i ∈ K), {y : γ | Inseparable i y} ⊆ s

Tactic:
fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)

Premises used: Inseparable.mem_measurableSet_iff, Set.Subset, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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
⊢ ∀ (i : γ) (j : i ∈ K), {y : γ | Inseparable i y} ⊆ s

Tactic:
exact fun x hx y hy ↦ (hy.mem_measurableSet_iff hs).1 (hKs hx)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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∞)

Tactic:
le_antisymm ?_ (measure_mono subset_closure)

Premises used: subset_closure, le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (closure[inst] K) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (closure[inst] K) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ (measure_mono subset_closure)

Premises used: subset_closure, le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (closure[inst] K) : ℝ≥0∞)
    ((μ : (a : Set γ) → ℝ≥0∞) (toMeasurable μ K) : ℝ≥0∞)

Tactic:
measure_mono <|
      hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)

Premises used: MeasureTheory.subset_toMeasurable, IsCompact.closure_subset_measurableSet, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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∞) (toMeasurable μ K) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
measure_toMeasurable ..

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : R1Space γ
K : Set γ
hK : IsCompact K
μ : Measure γ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) (closure[inst] K) : ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
calc
    μ (closure K) ≤ μ (toMeasurable μ K) := measure_mono <|
      hK.closure_subset_measurableSet (measurableSet_toMeasurable ..) (subset_toMeasurable ..)
    _ = μ K := measure_toMeasurable ..

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, IsCompact.closure_subset_measurableSet, MeasureTheory.measurableSet_toMeasurable, closure, MeasureTheory.measure_mono, MeasureTheory.toMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
⊢ MeasurableSet (closure[inst] s)

Tactic:
isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, isClosed_closure
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
s : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
⊢ MeasurableSet (frontier s)

Tactic:
measurableSet_closure.diff measurableSet_interior

Premises used: MeasurableSet.diff, frontier, measurableSet_closure, measurableSet_interior
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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)
rw : Measurable f
⊢ Measurable f

Tactic:
rw [‹BorelSpace γ›.measurable_eq]

Premises used: BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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

Tactic:
measurable_generateFrom hf

Premises used: measurable_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
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

Tactic:
exact measurable_generateFrom hf

Premises used: measurable_generateFrom