no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t✝ : Set α
a✝ b a : α
s t : Set α
⊢ IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]