α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ b ⊔ a → b ⊓ a ⋖ a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ a ⊔ b → a ⊓ b ⋖ a
rw [inf_comm, sup_comm]
no goals
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsLowerModularLattice α
a b : α
⊢ b ⋖ b ⊔ a → b ⊓ a ⋖ a
exact inf_covby_of_covby_sup_left