Commit 2022-01-04 03:53 8f391aa5

chore(algebra/module/submodule): switch subtype_eq_val to coe_subtype (#11210) Change the name and form of a lemma, from

lemma subtype_eq_val : ((submodule.subtype p) : p → M) = subtype.val := rfl

to

lemma coe_subtype : ((submodule.subtype p) : p → M) = coe := rfl

The latter is the simp-normal form so I claim it should be preferred.