What happened for "extends" under the hood?

Stream: general

[Erika Su]

suppose

class C (a  : Sort u) extends A a, B a where

Does the lean automatically implement something like

instance (a : Sort u) : Coe (C a) (A a)

underneath?
I wondered because i found that i C.methodsOfA doesn't exist, whereas C.methodsOfC exist.

[Kevin Buzzard]

Is this lean 3 or lean 4?

[Erika Su]

it's lean4.

[Scott Morrison]

Have a look at the output of

import Mathlib.Util.WhatsNew

class A (α : Sort u)
class B (α : Sort u)

whatsnew in
class C (α  : Sort u) extends A α, B α where

variable (i : C α) in
#synth B α

There's no coercion being generated, but instead instances are being provided. You just use the methods from A (i.e. as A.method, or just method after open A).