Commit 2025-01-13 17:00 90fd1e09
View on Github →chore: address some porting notes about coercions of equivs (#20714)
I came across a few porting notes about removing toFun_eq_coe. We in fact do want to have this lemma for rewriting, but not as a @[simp] lemma. So readd the missing toFun_eq_coe lemmas, and turn some porting notes into doc comments.
In those files, also clean up some other porting notes about coercions: it looks like there were some workarounds that are now unnecessary.