rw [min_def]
α✝ : Type ?u.5660
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ min a b ∈ s
α✝ : Type ?u.5660
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then a else b) ∈ s