no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a✝ b✝ : α
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t
cases' le_total a b with h h <;> simp [h, ha.1, hb.1]