chore: relax typeclass assumptions in two modular lattice lemmas (#7555)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com> @alreadydone
leanprover-community · Oct 7, 2023 · 7732480 · 7732480
1 parent fb3884a
commit 7732480
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Order/ModularLattice.lean b/Mathlib/Order/ModularLattice.lean
@@ -409,12 +409,12 @@ theorem disjoint_sup_left_of_disjoint_sup_right [Lattice α] [OrderBot α]
   rwa [sup_comm, disjoint_comm] at hsup
 #align disjoint.disjoint_sup_left_of_disjoint_sup_right Disjoint.disjoint_sup_left_of_disjoint_sup_right
 
-theorem isCompl_sup_right_of_isCompl_sup_left [CompleteLattice α] [IsModularLattice α]
+theorem isCompl_sup_right_of_isCompl_sup_left [Lattice α] [BoundedOrder α] [IsModularLattice α]
     (h : Disjoint a b) (hcomp : IsCompl (a ⊔ b) c) :
     IsCompl a (b ⊔ c) :=
   ⟨h.disjoint_sup_right_of_disjoint_sup_left hcomp.disjoint, codisjoint_assoc.mp hcomp.codisjoint⟩
 
-theorem isCompl_sup_left_of_isCompl_sup_right [CompleteLattice α] [IsModularLattice α]
+theorem isCompl_sup_left_of_isCompl_sup_right [Lattice α] [BoundedOrder α] [IsModularLattice α]
     (h : Disjoint b c) (hcomp : IsCompl a (b ⊔ c)) :
     IsCompl (a ⊔ b) c :=
   ⟨h.disjoint_sup_left_of_disjoint_sup_right hcomp.disjoint, codisjoint_assoc.mpr hcomp.codisjoint⟩