diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean index c23461c93..2b06a4e44 100644 --- a/library/data/set/filter.lean +++ b/library/data/set/filter.lean @@ -284,14 +284,14 @@ protected definition complete_lattice [reducible] : algebra.complete_lattice (fi le_refl := weakens.refl, le_trans := @weakens.trans A, le_antisymm := @weakens.antisymm A, - inf := inf, - le_inf := @inf_refines A, - inf_le_left := refines_inf_left, - inf_le_right := refines_inf_right, - sup := sup, - sup_le := @refines_sup A, - le_sup_left := sup_refines_left, - le_sup_right := sup_refines_right, +-- inf := inf, +-- le_inf := @inf_refines A, +-- inf_le_left := refines_inf_left, +-- inf_le_right := refines_inf_right, +-- sup := sup, +-- sup_le := @refines_sup A, +-- le_sup_left := sup_refines_left, +-- le_sup_right := sup_refines_right, Inf := Inf, Inf_le := @refines_Inf A, le_Inf := @Inf_refines A