Theorem: absorb1 (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_inf
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 ≤ x ⊔ y

State before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ 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 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