Commit 2025-02-05 17:40 24c59759
View on Github →chore(PresheafedSpace): remove mk_coe and some comments from porting (#21382)
My experience with SimpVarHead is that declarations flagged are something that Lean can handle with eta-reduction/expansion. Either way, this declaration is not used in mathlib and the commented out code doesn't seem to be missed.