OK so adding to_fun_as_coe_apply made the linter go nuts because @[simps] is generating lemmas which aren't in simp normal form now. It's also not generating the additive versions of the lemmas, and furthermore the autoporter is not generating the #aligns for simps-generated lemmas anyway, so I am fixing several problems at once here.

In an ideal world, someone (unfortunately not me) will make @[simps] generate lemmas which don't mention toFun, and will also make @[to_additive, simps] work, and someone (unfortunately also not me) will make the autoporter generate #align statements for all the lemmas generated by @[simps] . This PR can be thought of as a workaround for all of these issues. Even if it's thought of as not a good idea to make to_fun_as_coe a simp lemma, the rest of this PR is still independently of some use while we wait for these fixes (which I've not opened issues for).

I don't think it's a good idea to proceed with this. I suggest a work-around for having simps produce the right lemmas at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.40.5Bsimps.5D.20making.20lemmas.20not.20in.20simp.20normal.20form/near/315268553

If we don't simp away toFun to a coercion, then what do we do with examples like the following?

import Mathlib.Algebra.Group.WithOne.Basic

/-
from mathlib:

@[simp, to_additive]
theorem MulHom.coe_mk [Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f := rfl
-/
-- this goal shows up in the middle of a chain of rewrites done by `simp`
example [Mul α] [Mul β] (e : α ≃* β) (x : α) :
    Function.comp (↑(MulEquiv.toMulHom (MulEquiv.symm e)))
      (↑(MulEquiv.toMulHom e)) x = x := by
  -- goal contains no `toFun`
  rw [MulHom.coe_mk] -- this lemma contains no `toFun` and is a `simp` lemma
  -- goal now contains `MulHom.toFun` (the first `↑`)
  sorry

I don't know how to stop simp creating goals which mention toFun and right now it doesn't know what to do with them.

I don't understand why this is tagged awaiting-author -- I don't know what I am supposed to do with it. I'll change it back to awaiting-review. My understanding is that the community is happy with the idea that e.toFun is not the simp normal form. So now we either tell simp to change e.toFun into the simp normal form, or we absolutely guarantee that simp never produces an e.toFun term, which I don't know how to do (see previous example, which simp produced and which caused ported simp proofs to break in #922 -- see the second point in the first post). I don't really understand the disadvantage of telling simp what e.toFun should look like. If I'm supposed to be doing something, let me know!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style