Constructing a complete_lattice instance

Stream: new members

[Fingy Soupy]

Hello, I'm trying to construct a complete_lattice instance for my type.
I have already created instances for linear_order, has_sup, and has_bot (classes which complete_lattice extends), however, it seems that I still need to include these fields inside the complete_lattice instance. Is there any easy way to just specify that the new instance should use the other ones rather than repeating all of the fields?

Also, I am looking at the setoid instance for reference and I don't really understand the syntax near the end
https://github.com/leanprover-community/mathlib/blob/5dc8c1cf64737787dff8a3f27f75e9107661a7f0/src/data/setoid/basic.lean#L131
I haven't seen $, ..., or that right arrow carot used anywhere else.
If it's just for ergonomics, I think I'll save wrapping my head around it until I can create a more verbose instance

[Fingy Soupy]

Ah, I was looking at the online source so I did not have an easy way of finding the definition of complete_lattice_of_Inf it seems that the .. syntax is doing what I want to achieve...

[Fingy Soupy]

:duck: