α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ b ⊔ a → b ⋖ b ⊔ a → b ⊓ a ⋖ b
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
rw [sup_comm, inf_comm]
no goals
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakLowerModularLattice α
a b : α
⊢ a ⋖ b ⊔ a → b ⋖ b ⊔ a → b ⊓ a ⋖ b
exact fun ha hb => inf_covby_of_covby_sup_of_covby_sup_left hb ha