diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean index 646e324cf57607..45ee06f4df75f3 100644 --- a/Mathlib/Data/Set/Lattice.lean +++ b/Mathlib/Data/Set/Lattice.lean @@ -239,7 +239,7 @@ theorem mem_iInter₂_of_mem {s : ∀ i, κ i → Set α} {a : α} (h : ∀ i j, mem_iInter₂.2 h #align set.mem_Inter₂_of_mem Set.mem_iInter₂_of_mem -instance Set.completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Set α) := +instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Set α) := { instBooleanAlgebraSet with le_sSup := fun s t t_in a a_in => ⟨t, t_in, a_in⟩ sSup_le := fun s t h a ⟨t', ⟨t'_in, a_in⟩⟩ => h t' t'_in a_in