-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Set.OrdConnected.measurableSet (h : OrdConnected s) : MeasurableSet s

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet (u ∪ s \ u)

Tactic:
exact humeas.union hfinite.measurableSet

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
⊢ MeasurableSet s

Tactic:
have : u ⊆ s := iUnion₂_subset fun x hx => iUnion₂_subset fun y hy =>
  Ioo_subset_Icc_self.trans (h.out hx hy)

Result:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet s

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
⊢ MeasurableSet s

Tactic:
have humeas : MeasurableSet u := huopen.measurableSet

Result:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
⊢ MeasurableSet s

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
⊢ MeasurableSet s

Tactic:
have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo

Result:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
⊢ MeasurableSet s

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
⊢ MeasurableSet s

Tactic:
let u := ⋃ (x ∈ s) (y ∈ s), Ioo x y

Result:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
⊢ MeasurableSet s

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet s

Tactic:
rw [← union_diff_cancel this]

Result:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
humeas : MeasurableSet u
hfinite : (s \ u).Finite
this : u ⊆ s
⊢ MeasurableSet (u ∪ s \ u)

Proof state:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
⊢ MeasurableSet s

Tactic:
have huopen : IsOpen u := isOpen_biUnion fun _ _ => isOpen_biUnion fun _ _ => isOpen_Ioo

Result:
α : Type u_1
s : Set α
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
h : s.OrdConnected
u : Set α := ⋃ x ∈ s, ⋃ y ∈ s, Ioo x y
huopen : IsOpen u
⊢ MeasurableSet s