Diamond for CompleteBooleanAlgebra of Set's

[mattrobball]

From leanprover-community/mathlib3#16932, we have

import Mathlib.Data.Set.Lattice

variable {α : Type*}

-- Succeeds
example : @Set.instBooleanAlgebraSet α = Pi.booleanAlgebra := by
  with_reducible_and_instances rfl

-- Fails
example : (@Set.completeAtomicBooleanAlgebra α).toCompleteBooleanAlgebra = Pi.completeBooleanAlgebra := rfl

See also the Zulip discussion

[urkud]

AFAICT, we intentionally override some fields to have better definitional equalities for a ∈ ⋃₀ S.