awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
A : ∀ x ∈ s, ∃ y ∈ Ioi x, Ioo x y ⊆ s
choose! : ∀ (y : (x : α) → α) (hy : ∀ x ∈ s, y x ∈ Ioi x) (h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s), (s \ interior s).Countable
⊢ (s \ interior s).Countable

Tactic:
choose! y hy h'y using A
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
inl : ∀ (h' : x < x'), Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
inr : ∀ (h' : x' < x), Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'

Tactic:
rcases lt_or_gt_of_ne hxx' with (h' | h')

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'

Tactic:
disjoint_left.2 fun z hz h'z => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
inl :
  ∀ (z : α) (hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z)
    (h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z), False
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'

Tactic:
refine disjoint_left.2 fun z hz h'z => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
⊢ x' ∈ interior s

Tactic:
have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
this : x' ∈ interior s
⊢ False

Tactic:
False.elim (hx'.2 this)

Premises used: False.elim, And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x < x'
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
this : x' ∈ interior s
⊢ False

Tactic:
exact False.elim (hx'.2 this)

Premises used: False.elim, And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'

Tactic:
disjoint_left.2 fun z hz h'z => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
inr :
  ∀ (z : α) (hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z)
    (h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z), False
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (y x)) x x'

Tactic:
refine disjoint_left.2 fun z hz h'z => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
⊢ x ∈ interior s

Tactic:
have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
this : x ∈ interior s
⊢ False

Tactic:
False.elim (hx.2 this)

Premises used: False.elim, And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
x : α
hx : x ∈ s \ interior s
x' : α
hx' : x' ∈ s \ interior s
hxx' : x ≠ x'
h' : x' < x
z : α
hz : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x) z
h'z : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (y x)) x') z
this : x ∈ interior s
⊢ False

Tactic:
exact False.elim (hx.2 this)

Premises used: False.elim, And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
⊢ (s \ interior s).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)

Tactic:
have B : Set.PairwiseDisjoint (s \ interior s) fun x => Ioo x (y x) := by
    intro x hx x' hx' hxx'
    rcases lt_or_gt_of_ne hxx' with (h' | h')
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x' ∈ interior s :=
        mem_interior.2 ⟨Ioo x (y x), h'y _ hx.1, isOpen_Ioo, ⟨h', h'z.1.trans hz.2⟩⟩
      exact False.elim (hx'.2 this)
    · refine disjoint_left.2 fun z hz h'z => ?_
      have : x ∈ interior s :=
        mem_interior.2 ⟨Ioo x' (y x'), h'y _ hx'.1, isOpen_Ioo, ⟨h', hz.1.trans h'z.2⟩⟩
      exact False.elim (hx.2 this)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
B : (s \ interior s).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)
⊢ (s \ interior s).Countable

Tactic:
B.countable_of_Ioo fun x hx => hy x hx.1

Premises used: Set.PairwiseDisjoint.countable_of_Ioo, And.left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
M : (x : α) → α
hM : ∀ x ∈ s, x < M x
y : (x : α) → α
hy : ∀ x ∈ s, y x ∈ Ioi x
h'y : ∀ x ∈ s, Ioo x (y x) ⊆ s
B : (s \ interior s).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)
⊢ (s \ interior s).Countable

Tactic:
exact B.countable_of_Ioo fun x hx => hy x hx.1

Premises used: Set.PairwiseDisjoint.countable_of_Ioo, And.left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
pos : ∀ (H : ∃ x ∈ s, IsTop x), MeasurableSet s
neg : ∀ (H : ¬∃ x ∈ s, IsTop x), MeasurableSet s
⊢ MeasurableSet s

Tactic:
by_cases H : ∃ x ∈ s, IsTop x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ∃ x ∈ s, IsTop x
pos : ∀ (x₀ : α) (x₀s : x₀ ∈ s) (h₀ : IsTop x₀), MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases H with ⟨x₀, x₀s, h₀⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
rw rw₁ : s = s
⊢ s = {x₀} ∪ s \ {x₀}

Tactic:
rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ s = {x₀} ∪ s \ {x₀}

Tactic:
have : s = { x₀ } ∪ s \ { x₀ } := by rw [union_diff_cancel (singleton_subset_iff.2 x₀s)]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
pos : MeasurableSet ({x₀} ∪ s \ {x₀})
⊢ MeasurableSet s

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ MeasurableSet ({x₀} ∪ s \ {x₀})

Tactic:
(measurableSet_singleton _).union ?_

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
pos : MeasurableSet (s \ {x₀})
⊢ MeasurableSet ({x₀} ∪ s \ {x₀})

Tactic:
refine (measurableSet_singleton _).union ?_

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
x : α
hx : x ∈ s \ {x₀}
⊢ x ≠ x₀

Tactic:
simpa using hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
⊢ ∀ x ∈ s \ {x₀}, x < x₀

Tactic:
have A : ∀ x ∈ s \ { x₀ }, x < x₀ := fun x hx => lt_of_le_of_ne (h₀ _) (by simpa using hx.2)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
⊢ MeasurableSet (s \ {x₀})

Tactic:
.of_mem_nhdsGT_aux (fun x hx => ?_) fun x hx => ⟨x₀, A x hx⟩

Premises used: MeasurableSet.of_mem_nhdsGT_aux, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
pos : ∀ (x : α) (hx : x ∈ s \ {x₀}), s \ {x₀} ∈ 𝓝[>] x
⊢ MeasurableSet (s \ {x₀})

Tactic:
refine .of_mem_nhdsGT_aux (fun x hx => ?_) fun x hx => ⟨x₀, A x hx⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
⊢ ∃ u ∈ Ioi x, Ioo x u ⊆ s

Tactic:
(mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)

Premises used: mem_nhdsGT_iff_exists_Ioo_subset', And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
pos : ∀ (u : α) (hu : u ∈ Ioi x) (us : Ioo x u ⊆ s), s \ {x₀} ∈ 𝓝[>] x
⊢ s \ {x₀} ∈ 𝓝[>] x

Tactic:
obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s :=
      (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)

Premises used: Set.Ioi, mem_nhdsGT_iff_exists_Ioo_subset', And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
⊢ s \ {x₀} ∈ 𝓝[>] x

Tactic:
(mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, ?_⟩⟩

Premises used: Iff.mpr, mem_nhdsGT_iff_exists_Ioo_subset', And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
pos : ∀ (y : α) (hy : y ∈ Ioo x u), y ∉ {x₀}
⊢ s \ {x₀} ∈ 𝓝[>] x

Tactic:
refine (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
y : α
hy : y ∈ Ioo x u
⊢ y ∉ {x₀}

Tactic:
ne_of_lt (hy.2.trans_le (h₀ _))

Premises used: Set.Mem, setOf, And.right, LT.lt.trans_le, Set.singleton, ne_of_lt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
this : s = {x₀} ∪ s \ {x₀}
A : ∀ x ∈ s \ {x₀}, x < x₀
x : α
hx : x ∈ s \ {x₀}
u : α
hu : u ∈ Ioi x
us : Ioo x u ⊆ s
y : α
hy : y ∈ Ioo x u
⊢ y ∉ {x₀}

Tactic:
exact ne_of_lt (hy.2.trans_le (h₀ _))

Premises used: And.right, LT.lt.trans_le, ne_of_lt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ¬∃ x ∈ s, IsTop x
⊢ MeasurableSet s

Tactic:
.of_mem_nhdsGT_aux h ?_

Premises used: MeasurableSet.of_mem_nhdsGT_aux
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ¬∃ x ∈ s, IsTop x
neg : ∀ x ∈ s, ∃ (y : α), x < y
⊢ MeasurableSet s

Tactic:
refine .of_mem_nhdsGT_aux h ?_
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ¬∃ x ∈ s, ∀ (b : α), b ≤ x
⊢ ∀ (x : α) (_ : x ∈ s), ∃ (b : α), x < b

Tactic:
push Not at H

Premises used: Not
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ∀ (x : α) (_ : x ∈ s), ∃ (b : α), x < b
⊢ ∀ x ∈ s, ∃ (y : α), x < y

Tactic:
H
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ∀ (x : α) (_ : x ∈ s), ∃ (b : α), x < b
⊢ ∀ x ∈ s, ∃ (y : α), x < y

Tactic:
exact H
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
inl : ∀ (hα : IsEmpty α), MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
inr : ∀ (hα : Nonempty α), MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : IsEmpty α
⊢ ∀ (b : δ), Eq.{u_1 + 1} (α := Set α) (range fun (i : ι) ↦ f i b) ∅

Tactic:
have : ∀ b, range (fun i ↦ f i b) = ∅ := fun b ↦ eq_empty_of_isEmpty _
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : IsEmpty α
this : ∀ (b : δ), Eq.{u_1 + 1} (α := Set α) (range fun (i : ι) ↦ f i b) ∅
⊢ MeasurableSet.{u_4} (α := δ) {b : δ | BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ f i b)}

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
i : ι
c : α
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}

Tactic:
measurableSet_le (hf i) measurable_const

Premises used: measurableSet_le, measurable_const
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : LinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Sort u_5
inst_5 : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hα : Nonempty α
i : ι
c : α
⊢ MeasurableSet.{u_4} (α := δ) {x : δ | f i x ≤ c}

Tactic:
exact measurableSet_le (hf i) measurable_const

Premises used: measurableSet_le, measurable_const