failed to synthesize SupSet ℝ

Stream: new members

[Alvise Sembenico]

Hi, I am playing with a toy example because I am using supremum in a project but the following fails with the error failed to synthesize SupSet R..

example (A : Set ℝ ) (hne : A.Nonempty) (hbdd : BddAbove A) :
    ⨆ (a ∈ A), (a+1) =  1+ ⨆ (a ∈ A), a:=
  by
    sorry

I tried many solutions but none seems to work and I would love to understand where the problem is.
Thanks!

[Alvise Sembenico]

the solution was just to import import Mathlib.Order.ConditionallyCompleteLattice.Basic. The error is quite confusing which makes it quite hard to debug

[Eric Wieser]

This type of problem will go away if you start with import Mathlib