α : Type u_1
β : Type ?u.164586
γ : Type ?u.164589
ι : Sort ?u.164592
κ : ι → Sort ?u.164597
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ OrdConnected s
α : Type u_1
β : Type ?u.164586
γ : Type ?u.164589
ι : Sort ?u.164592
κ : ι → Sort ?u.164597
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
⊢ OrdConnected s ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
refine' ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => _⟩
α : Type u_1
β : Type ?u.164586
γ : Type ?u.164589
ι : Sort ?u.164592
κ : ι → Sort ?u.164597
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ OrdConnected (↑(upperClosure s) ∩ ↑(lowerClosure s))
α : Type u_1
β : Type ?u.164586
γ : Type ?u.164589
ι : Sort ?u.164592
κ : ι → Sort ?u.164597
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ OrdConnected s
rw [← h]
no goals
α : Type u_1
β : Type ?u.164586
γ : Type ?u.164589
ι : Sort ?u.164592
κ : ι → Sort ?u.164597
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
x : α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ OrdConnected (↑(upperClosure s) ∩ ↑(lowerClosure s))
exact (UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected