apply le_antisymm
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y = x
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y ≤ x

case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ x ⊓ y