Commit 2025-02-11 15:35 399891fd

refactor: don't use lambdas in CoeFun instances (#21405) Hiding the lambdas behind a non-reducible toFun or changing the CoeFun instance to FunLike prevents many lemmas (some simp) to have a lambda as their head symbol. Arguably, those were misports because Lean 3's has_coe_to_fun was not reducible. Whether or not those should have become FunLike or CoeFun := ⟨semireducibleDef⟩ back then is unclear. Zulip