Question with a notation of type-classes?

Stream: mathlib4

[Sina Hazratpour 𓃵]

I am not sure if I understand the square brackets around the field exact : ExactPairing X rightDual in the type class below correctly. And, I could not find anything related to it on the Lean Language Reference.

class HasLeftDual (Y : C) where
  /-- The left dual of the object `X`. -/
  leftDual : C
  [exact : ExactPairing leftDual Y]

Is it supposed to be the same as exact : ExactPairing leftDual Y := by infer_instance or does something different?

[Soundwave]

Indeed, all the binders work in the class context as they do in others:

class Foo (α : Type) where
  foo : α

class Bar (α : Type) where
  {bar : Prop}
  baz : bar
  bax : α

class Qux (α : Type) where
  qux : α
  [foo : Foo α]


instance foo : Foo Nat where
  foo := 2

instance bar : Bar Nat where
  baz : 2 = 2 := by rfl
  bax := 2

instance qux : Qux Nat where
  qux := 1

#eval qux.foo.foo