Theorem: absorb2 (LeanInRome/S2_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean)

State before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y = x
Tactic:
apply le_antisymm
State after:
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

State before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ x ⊓ y
Tactic:
apply le_sup_left
State after:
no goals

State before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y ≤ x
Tactic:
apply sup_le
State after:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x

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

State before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ y ≤ x
Tactic:
apply inf_le_left
State after:
no goals

State before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x
Tactic:
apply le_refl
State after:
no goals