diamond in ConditionallyCompleteLattice

Stream: mathlib4

[Alex Meiburg]

The following demos a diamond:

instance {α : Type*} [Preorder α] (a b : α) [Fact (a ≤ b)] : Inhabited (Set.Icc a b) :=
  ⟨⟨a, by simp [Fact.out]⟩⟩

example {α : Type*} [ConditionallyCompleteLinearOrder α] {a b : α} [Fact (a ≤ b)] :
    let t : Type _ := Set.Icc a b
    let i1 : CompleteLinearOrder t := instCompleteLinearOrderElemIccOfFactLe
    let i2 : ConditionallyCompleteLinearOrder t := ordConnectedSubsetConditionallyCompleteLinearOrder _
    i1.toConditionallyCompleteLattice = i2.toConditionallyCompleteLattice := by
  rfl

That Inhabited instance isn't in Mathlib (although maybe it should be), but I can hit this diamond also without that, e.g.

example {α : Type*} [ConditionallyCompleteLinearOrder α] [Zero α] [One α] [ZeroLEOneClass α] :
    let t : Type _ := Set.Icc 0 1
    let i1 : CompleteLinearOrder t := instCompleteLinearOrderElemIccOfFactLe
    let i2 : ConditionallyCompleteLinearOrder t := ordConnectedSubsetConditionallyCompleteLinearOrder _
    i1.toConditionallyCompleteLattice = i2.toConditionallyCompleteLattice := by
  rfl --Fails, so, they're not defeq

and both of those instances I'm explicitly naming are unscoped instances. I don't have the context though to know how this should be fixed.

[Violeta Hernández]

Can instCompleteLinearOrderElemIccOfFactLe be made to extend ordConnectedSubsetConditionallyCompleteLinearOrder?