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