Theorem: absorb2 (LeanInRome/S2_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean)

State before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y = x
Tactic:
sorry
State after:
no goals