awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
this : Ioi a = ⋃ b ∈ t, Ici b
refine_1 : MeasurableSet.{u_1} (α := α) (⋃ b ∈ t, (Iio b)ᶜ)
⊢ MeasurableSet (Ioi a)

Tactic:
simp only [this, ← compl_Iio]

Premises used: Set.compl_Iio
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
this : Ioi a = ⋃ b ∈ t, Ici b
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ t, (Iio b)ᶜ)

Tactic:
.biUnion htc <| fun _ _ ↦ (H _).compl

Premises used: MeasurableSet.compl, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this_1 : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
hcovBy : ¬∃ (b : α), a ⋖ b
t : Set α
hat : t ⊆ Ioi a
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ t, Ioi i) (⋃ i ∈ Ioi a, Ioi i)
this : Ioi a = ⋃ b ∈ t, Ici b
⊢ MeasurableSet.{u_1} (α := α) (⋃ b ∈ t, (Iio b)ᶜ)

Tactic:
exact .biUnion htc <| fun _ _ ↦ (H _).compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
this : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
H : ∀ (a : α), MeasurableSet (Iio a)
a : α
⊢ MeasurableSet (Iio a)

Tactic:
apply H
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_2 : ∀ (i : α), MeasurableSet (Iio i)
⊢ ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (range Iio) t → MeasurableSet t

Tactic:
rw [forall_mem_range]

Premises used: Set.forall_mem_range
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
⊢ MeasurableSet (Iio a)

Tactic:
GenerateMeasurable.basic _ isOpen_Iio

Premises used: MeasurableSet, isOpen_Iio, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
⊢ MeasurableSet (Iio a)

Tactic:
exact GenerateMeasurable.basic _ isOpen_Iio

Premises used: isOpen_Iio, MeasurableSpace.GenerateMeasurable.basic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ SecondCountableTopology α

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
rw :
  Eq.{u_1 + 1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))
⊢ borel α = MeasurableSpace.generateFrom (range Iic)

Tactic:
rw [borel_eq_generateFrom_Ioi]

Premises used: borel_eq_generateFrom_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_1 :
  LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))
refine_2 :
  LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Iic))
    (MeasurableSpace.generateFrom (range Ioi))
⊢ Eq.{u_1 + 1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))

Tactic:
MeasurableSpace.generateFrom_le fun t ht => ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_1 : ∀ (t : Set α) (ht : Membership.mem (γ := Set (Set α)) (range Ioi) t), MeasurableSet t
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Ioi))
    (MeasurableSpace.generateFrom (range Iic))

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
t : Set α
ht : Membership.mem (γ := Set (Set α)) (range Ioi) t
refine_1 : ∀ (u : α), MeasurableSet (Ioi u)
⊢ MeasurableSet t

Tactic:
obtain ⟨u, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
refine_1 : MeasurableSet (Iic u)ᶜ
⊢ MeasurableSet (Ioi u)

Tactic:
rw [← compl_Iic]

Premises used: Set.compl_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)ᶜ

Tactic:
(MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Premises used: Iff.mpr, Set.mem_range, MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
⊢ MeasurableSet (Iic u)ᶜ

Tactic:
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Premises used: Iff.mpr, Set.mem_range, MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Iic))
    (MeasurableSpace.generateFrom (range Ioi))

Tactic:
MeasurableSpace.generateFrom_le fun t ht => ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
refine_2 : ∀ (t : Set α) (ht : Membership.mem (γ := Set (Set α)) (range Iic) t), MeasurableSet t
⊢ LE.le.{u_1} (α := MeasurableSpace α) (MeasurableSpace.generateFrom (range Iic))
    (MeasurableSpace.generateFrom (range Ioi))

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => ?_

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
t : Set α
ht : Membership.mem (γ := Set (Set α)) (range Iic) t
refine_2 : ∀ (u : α), MeasurableSet (Iic u)
⊢ MeasurableSet t

Tactic:
obtain ⟨u, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
refine_2 : MeasurableSet (Ioi u)ᶜ
⊢ MeasurableSet (Iic u)

Tactic:
rw [← compl_Ioi]

Premises used: Set.compl_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)ᶜ

Tactic:
(MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Premises used: Iff.mpr, Set.mem_range, MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
u : α
⊢ MeasurableSet (Ioi u)ᶜ

Tactic:
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl

Premises used: Iff.mpr, Set.mem_range, MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom (range Ici)

Tactic:
@borel_eq_generateFrom_Iic αᵒᵈ _ _ _ _

Premises used: Set.Ici, setOf, OrderDual, borel_eq_generateFrom_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : Preorder α
a : α
inst_3 : ClosedIciTopology α
⊢ MeasurableSet (Ici a)

Tactic:
isClosed_Ici.measurableSet

Premises used: IsClosed.measurableSet, isClosed_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : Preorder α
a : α
μ : Measure α
inst_3 : ClosedIciTopology α
⊢ NullMeasurableSet (Ici a) μ

Tactic:
measurableSet_Ici.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : Preorder α
a : α
inst_3 : ClosedIicTopology α
⊢ MeasurableSet (Iic a)

Tactic:
isClosed_Iic.measurableSet

Premises used: IsClosed.measurableSet, isClosed_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : Preorder α
a : α
μ : Measure α
inst_3 : ClosedIicTopology α
⊢ NullMeasurableSet (Iic a) μ

Tactic:
measurableSet_Iic.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : Preorder α
a b : α
inst_3 : OrderClosedTopology α
⊢ MeasurableSet (Icc a b)

Tactic:
isClosed_Icc.measurableSet

Premises used: IsClosed.measurableSet, isClosed_Icc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : Preorder α
a b : α
μ : Measure α
inst_3 : OrderClosedTopology α
⊢ NullMeasurableSet (Icc a b) μ

Tactic:
measurableSet_Icc.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_Icc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : ClosedIciTopology α
⊢ (𝓝[Ici b] a).IsMeasurablyGenerated

Tactic:
measurableSet_Ici.nhdsWithin_isMeasurablyGenerated _

Premises used: MeasurableSet.nhdsWithin_isMeasurablyGenerated, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : ClosedIicTopology α
⊢ (𝓝[Iic b] a).IsMeasurablyGenerated

Tactic:
measurableSet_Iic.nhdsWithin_isMeasurablyGenerated _

Premises used: measurableSet_Iic, MeasurableSet.nhdsWithin_isMeasurablyGenerated
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : OrderClosedTopology α
rw : (𝓝[Ici a] x ⊓ 𝓝[Iic b] x).IsMeasurablyGenerated
⊢ (𝓝[Icc a b] x).IsMeasurablyGenerated

Tactic:
rw [← Ici_inter_Iic, nhdsWithin_inter]

Premises used: nhdsWithin_inter, Set.Ici_inter_Iic
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : OrderClosedTopology α
⊢ (𝓝[Ici a] x ⊓ 𝓝[Iic b] x).IsMeasurablyGenerated

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : ClosedIciTopology α
⊢ IsMeasurablyGenerated.{u_1} (α := α) atTop

Tactic:
@Filter.iInf_isMeasurablyGenerated _ _ _ _ fun a =>
    (measurableSet_Ici : MeasurableSet (Ici a)).principal_isMeasurablyGenerated

Premises used: Filter.iInf_isMeasurablyGenerated, Filter.atTop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : ClosedIicTopology α
⊢ IsMeasurablyGenerated.{u_1} (α := α) atBot

Tactic:
@Filter.iInf_isMeasurablyGenerated _ _ _ _ fun a =>
    (measurableSet_Iic : MeasurableSet (Iic a)).principal_isMeasurablyGenerated

Premises used: Filter.iInf_isMeasurablyGenerated, Filter.atBot
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : R1Space α
s_1 : Set α
hs : s_1 ∈ cocompact α
obtain : ∀ (t : Set α) (ht : IsCompact t) (hts : tᶜ ⊆ s_1), ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s_1
⊢ ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s_1

Tactic:
obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs

Premises used: Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t_1 u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : R1Space α
s_1 : Set α
hs : s_1 ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s_1
⊢ ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s_1

Tactic:
⟨(closure t)ᶜ, ht.closure.compl_mem_cocompact, isClosed_closure.measurableSet.compl,
      (compl_subset_compl.2 subset_closure).trans hts⟩

Premises used: Iff.mpr, subset_closure, Compl.compl, IsCompact.compl_mem_cocompact, IsCompact.closure, HasSubset.Subset.trans, IsClosed.measurableSet, MeasurableSet.compl, Set.compl_subset_compl, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t_1 u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : Preorder α
a b x : α
μ : Measure α
inst_3 : R1Space α
s_1 : Set α
hs : s_1 ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s_1
⊢ ∃ t ∈ cocompact α, MeasurableSet t ∧ t ⊆ s_1

Tactic:
exact ⟨(closure t)ᶜ, ht.closure.compl_mem_cocompact, isClosed_closure.measurableSet.compl,
      (compl_subset_compl.2 subset_closure).trans hts⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : PartialOrder α
inst_3 : OrderClosedTopology α
inst_4 : SecondCountableTopology α
⊢ MeasurableSet.{u_1} (α := α × α) {p : α × α | p.1 ≤ p.2}

Tactic:
OrderClosedTopology.isClosed_le'.measurableSet

Premises used: OrderClosedTopology.isClosed_le', IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : PartialOrder α
inst_3 : OrderClosedTopology α
inst_4 : SecondCountableTopology α
⊢ Measurable (β := Prop) fun (p : α × α) ↦ p.1 ≤ p.2

Tactic:
measurableSet_setOf.mp measurableSet_le'

Premises used: measurableSet_setOf, measurableSet_le', Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : PartialOrder α
inst_3 : OrderClosedTopology α
inst_4 : SecondCountableTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet.{u_4} (α := δ) {a : δ | f a ≤ g a}

Tactic:
hf.prodMk hg measurableSet_le'

Premises used: Set.Mem, setOf, Measurable.prodMk, Set.preimage, measurableSet_le'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : PartialOrder α
inst_3 : OrderClosedTopology α
inst_4 : SecondCountableTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := Prop) fun (a : δ) ↦ f a ≤ g a

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a : α
inst_3 : ClosedIciTopology α
⊢ MeasurableSet (Iio a)

Tactic:
isOpen_Iio.measurableSet

Premises used: isOpen_Iio, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a : α
μ : Measure α
inst_3 : ClosedIciTopology α
⊢ NullMeasurableSet (Iio a) μ

Tactic:
measurableSet_Iio.nullMeasurableSet

Premises used: measurableSet_Iio, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a : α
inst_3 : ClosedIicTopology α
⊢ MeasurableSet (Ioi a)

Tactic:
isOpen_Ioi.measurableSet

Premises used: IsOpen.measurableSet, isOpen_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a : α
μ : Measure α
inst_3 : ClosedIicTopology α
⊢ NullMeasurableSet (Ioi a) μ

Tactic:
measurableSet_Ioi.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
inst_3 : OrderClosedTopology α
⊢ MeasurableSet (Ioo a b)

Tactic:
isOpen_Ioo.measurableSet

Premises used: isOpen_Ioo, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
μ : Measure α
inst_3 : OrderClosedTopology α
⊢ NullMeasurableSet (Ioo a b) μ

Tactic:
measurableSet_Ioo.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
inst_3 : ClosedIicTopology α
⊢ MeasurableSet (Ioc a b)

Tactic:
measurableSet_Ioi.inter measurableSet_Iic

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, measurableSet_Iic, Set.inter, measurableSet_Ioi, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
μ : Measure α
inst_3 : ClosedIicTopology α
⊢ NullMeasurableSet (Ioc a b) μ

Tactic:
measurableSet_Ioc.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
inst_3 : ClosedIciTopology α
⊢ MeasurableSet (Ico a b)

Tactic:
measurableSet_Ici.inter measurableSet_Iio

Premises used: Set.Ici, Set.Mem, measurableSet_Iio, setOf, Set.inter, Set.Ico, measurableSet_Ici, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : LinearOrder α
a b : α
μ : Measure α
inst_3 : ClosedIciTopology α
⊢ NullMeasurableSet (Ico a b) μ

Tactic:
measurableSet_Ico.nullMeasurableSet

Premises used: measurableSet_Ico, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
a b x : α
μ : Measure α
inst_3 : ClosedIicTopology α
⊢ (𝓝[Ioi b] a).IsMeasurablyGenerated

Tactic:
measurableSet_Ioi.nhdsWithin_isMeasurablyGenerated _

Premises used: measurableSet_Ioi, MeasurableSet.nhdsWithin_isMeasurablyGenerated
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
a b x : α
μ : Measure α
inst_3 : ClosedIciTopology α
⊢ (𝓝[Iio b] a).IsMeasurablyGenerated

Tactic:
measurableSet_Iio.nhdsWithin_isMeasurablyGenerated _

Premises used: measurableSet_Iio, MeasurableSet.nhdsWithin_isMeasurablyGenerated