Theorem: absorb1 (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