subtype.coe_fn_coe

Stream: Is there code for X?

[Eric Wieser]

Do we have a lemma unfolding docs#coe_fn_trans anywhere?

lemma subtype.coe_fn_coe {α β γ} {p : α → Prop} (G : α → Sort*) (g : subtype p)
  [has_coe_to_fun α (λ _, β → γ)] :
  ⇑g = (g : α) := rfl

[Eric Wieser]

Ah, it's docs#coe_fn_coe_trans. Is there a reason that's not simp?

[Anne Baanen]

IIRC, coe_fn_coe_trans and coe_fn_coe_base didn't work with simp because the dependent function type is too high-order to infer, so we (Yury and I) had to add docs#coe_fn_coe_trans' and docs#coe_fn_coe_base'.

[Anne Baanen]

According to #2066, coe_fn_coe_trans was a duplicate simp lemma and got removed.