fix: reintroduce to_fun_as_coe as simp lemma (#931)

This is a proposed fix for the broken simp calls in #922. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20calls.20broken.20in.20mathlib4.23922/near/314783451 for more details. Note that `to_fun_as_coe` was a syntactic tautology when it was ported, but this is no longer the case because we now have `FunLike`.

Author: kbuzzard

Mathlib/Algebra/Group/WithOne/Basic.lean

@@ -129,30 +129,33 @@ theorem map_comp (f : α →ₙ* β) (g : β →ₙ* γ) : map (g.comp f) = (map
 #align with_one.map_comp WithOne.map_comp
 #align with_zero.map_comp WithZero.map_comp
 
+-- porting note: this used to have `@[simps apply]` but it was generating lemmas which
+-- weren't in simp normal form.
 /-- A version of `Equiv.optionCongr` for `WithOne`. -/
-@[to_additive "A version of `equiv.option_congr` for `with_zero`.", simps apply]
+@[to_additive "A version of `equiv.option_congr` for `with_zero`."]
 def _root_.MulEquiv.withOneCongr (e : α ≃* β) : WithOne α ≃* WithOne β :=
   { map e.toMulHom with
     toFun := map e.toMulHom, invFun := map e.symm.toMulHom,
     left_inv := fun x => (map_map _ _ _).trans <| by
-      -- porting note: in mathlib3 this worked as: `induction x using WithOne.cases_on <;> simp`
-      induction x using WithOne.cases_on
-      · simp
-      · simp only [map_coe, MulHom.coe_mk, map_comp, MonoidHom.coe_comp, Function.comp_apply,
-          MulEquiv.toEquiv_symm, coe_inj]
-        apply Equiv.symm_apply_apply,
-      -- porting note: I think because of the way coercions are handled, this doesn't get changed
-      -- by `simp` into something where `Equiv.symm_apply_apply` automatically applies.
+      induction x using WithOne.cases_on <;> simp
     right_inv := fun x => (map_map _ _ _).trans <| by
-      -- porting note: in mathlib3 this worked as: `induction x using WithOne.cases_on <;> simp`
-      induction x using WithOne.cases_on
-      · simp
-      · simp only [map_coe, MulHom.coe_mk, MulEquiv.toEquiv_symm, map_comp, MonoidHom.coe_comp,
-          Function.comp_apply, coe_inj]
-        apply Equiv.apply_symm_apply }
+      induction x using WithOne.cases_on <;> simp }
 #align mul_equiv.with_one_congr MulEquiv.withOneCongr
 #align add_equiv.with_zero_congr AddEquiv.withZeroCongr
 
+-- porting note: an approximation to this was being generated by `@[simps apply]` but it
+-- mentioned Equiv.toFun so was not in simp normal form. This might be a bug in `@[simps].
+@[simp] theorem _root_.MulEquiv.withOneCongr_apply {α β : Type _} [Mul α] [Mul β] (e : α ≃* β)
+  (a : WithOne α) : (MulEquiv.withOneCongr e).toEquiv a = (map (MulEquiv.toMulHom e)) a := rfl
+#align mul_equiv.with_one_congr_apply MulEquiv.withOneCongr_apply
+
+-- porting note: `@[to_additive, simps apply]` was not generating this lemma at the
+-- time of writing this note. 
+@[simp] theorem _root_.AddEquiv.withZeroCongr_apply {α β : Type _} [Add α] [Add β] (e : α ≃+ β)
+  (a : WithZero α) :
+    (AddEquiv.withZeroCongr e).toEquiv a = (WithZero.map (AddEquiv.toAddHom e)) a := rfl
+#align add_equiv.with_zero_congr_apply AddEquiv.withZeroCongr_apply
+
 -- porting note: for this declaration and the two below I added the `to_additive` attribute because
 -- it seemed to be missing from mathlib3, hence the lack of additive `#align`s.
 @[simp, to_additive]

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -529,20 +529,31 @@ theorem map_ne_one_iff {M N} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x :
 #align mul_equiv.map_ne_one_iff MulEquiv.map_ne_one_iff
 #align add_equiv.map_ne_zero_iff AddEquiv.map_ne_zero_iff
 
+-- porting note: Mathlib 3 had `@[simps apply]` but right now in Lean 4 it's generating
+-- simp lemmas which don't lint.
 /-- A bijective `Semigroup` homomorphism is an isomorphism -/
-@[to_additive "A bijective `AddSemigroup` homomorphism is an isomorphism", simps apply]
+@[to_additive "A bijective `AddSemigroup` homomorphism is an isomorphism"]
 noncomputable def ofBijective {M N F} [Mul M] [Mul N] [MulHomClass F M N]
 (f : F) (hf : Function.Bijective f) :
     M ≃* N :=
   { Equiv.ofBijective f hf with map_mul' := map_mul f }
 #align mul_equiv.of_bijective MulEquiv.ofBijective
 #align add_equiv.of_bijective AddEquiv.ofBijective
 
-@[simp]
+-- porting note: `@[simps apply]` should be making this lemma but it actually makes
+-- a lemma with `toFun` which isn't in simp normal form.
+@[simp, to_additive] theorem ofBijective_apply {M N F} [Mul M] [Mul N] [MulHomClass F M N]
+    (f : F) (hf : Function.Bijective f) (a : M) : (MulEquiv.ofBijective f hf).toEquiv a = f a :=
+  rfl
+#align mul_equiv.of_bijective_apply MulEquiv.ofBijective_apply
+#align add_equiv.of_bijective_apply AddEquiv.ofBijective_apply
+
+@[simp, to_additive]
 theorem ofBijective_apply_symm_apply {M N} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N)
     (hf : Function.Bijective f) : f ((Equiv.ofBijective f hf).symm n) = n :=
   (MulEquiv.ofBijective f hf).apply_symm_apply n
 #align mul_equiv.of_bijective_apply_symm_apply MulEquiv.ofBijective_apply_symm_apply
+#align add_equiv.of_bijective_apply_symm_apply AddEquiv.ofBijective_apply_symm_apply
 
 /-- Extract the forward direction of a multiplicative equivalence
 as a multiplication-preserving function.
@@ -589,8 +600,9 @@ for multiplicative maps from a monoid to a commutative monoid.
 -/
 @[to_additive
   "An additive analogue of `Equiv.arrowCongr`,
-  for additive maps from an additive monoid to a commutative additive monoid.",
-  simps apply]
+  for additive maps from an additive monoid to a commutative additive monoid."]
+-- porting note: @[simps apply] removed because it was making a lemma which
+-- wasn't in simp normal form.
 def monoidHomCongr {M N P Q} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q]
   (f : M ≃* N) (g : P ≃* Q) :
   (M →* P) ≃* (N →* Q) where
@@ -602,6 +614,14 @@ def monoidHomCongr {M N P Q} [MulOneClass M] [MulOneClass N] [CommMonoid P] [Com
 #align mul_equiv.monoid_hom_congr MulEquiv.monoidHomCongr
 #align add_equiv.add_monoid_hom_congr AddEquiv.addMonoidHomCongr
 
+@[simp, to_additive] theorem monoidHomCongr_apply {M N P Q} [MulOneClass M] [MulOneClass N]
+    [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
+    (MulEquiv.monoidHomCongr f g).toEquiv h = MonoidHom.comp (MulEquiv.toMonoidHom g)
+    (MonoidHom.comp h (MulEquiv.toMonoidHom (MulEquiv.symm f))) :=
+  rfl
+#align mul_equiv.monoid_hom_congr_apply MulEquiv.monoidHomCongr_apply
+#align add_equiv.add_monoid_hom_congr_apply AddEquiv.addMonoidHomCongr_apply
+
 /-- A family of multiplicative equivalences `Π j, (Ms j ≃* Ns j)` generates a
 multiplicative equivalence between `Π j, Ms j` and `Π j, Ns j`.
 
@@ -647,14 +667,29 @@ theorem piCongrRight_trans {η : Type _} {Ms Ns Ps : η → Type _} [∀ j, Mul
 index. -/
 @[to_additive
   "A family indexed by a nonempty subsingleton type is
-  equivalent to the element at the single index.",
-  simps]
+  equivalent to the element at the single index."]
 def piSubsingleton {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)] [Subsingleton ι]
   (i : ι) : (∀ j, M j) ≃* M i :=
   { Equiv.piSubsingleton M i with map_mul' := fun _ _ => Pi.mul_apply _ _ _ }
 #align mul_equiv.Pi_subsingleton MulEquiv.piSubsingleton
 #align add_equiv.Pi_subsingleton AddEquiv.piSubsingleton
 
+-- porting note: the next two lemmas should be being generated by `@[to_additive, simps]`.
+-- They are added manually because `@[simps]` is currently generating lemmas with `toFun` in
+@[simp, to_additive] theorem piSubsingleton_apply {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)]
+    [Subsingleton ι] (i : ι) (f : (x : ι) → M x) : (MulEquiv.piSubsingleton M i).toEquiv f = f i :=
+  rfl
+#align mul_equiv.Pi_subsingleton_apply MulEquiv.piSubsingleton_apply
+#align add_equiv.Pi_subsingleton_apply AddEquiv.piSubsingleton_apply
+
+@[simp, to_additive] theorem piSubsingleton_symmApply {ι : Type _} (M : ι → Type _) [∀ j, Mul (M j)]
+    [Subsingleton ι] (i : ι) (x : M i) (b : ι) :
+    (MulEquiv.symm (MulEquiv.piSubsingleton M i)) x b =
+    cast (Subsingleton.elim i b ▸ rfl : M i = M b) x :=
+rfl
+#align mul_equiv.Pi_subsingleton_symmApply MulEquiv.piSubsingleton_symmApply
+#align add_equiv.Pi_subsingleton_symmApply AddEquiv.piSubsingleton_symmApply
+
 /-!
 # Groups
 -/
@@ -677,6 +712,10 @@ protected theorem map_div [Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G)
 
 end MulEquiv
 
+-- porting note: we want to add
+-- `@[simps (config := { fullyApplied := false })]`
+-- here, but it generates simp lemmas which aren't in simp normal form
+-- (they have `toFun` in)
 /-- Given a pair of multiplicative homomorphisms `f`, `g` such that `g.comp f = id` and
 `f.comp g = id`, returns an multiplicative equivalence with `toFun = f` and `invFun = g`. This
 constructor is useful if the underlying type(s) have specialized `ext` lemmas for multiplicative
@@ -685,8 +724,7 @@ homomorphisms. -/
   "Given a pair of additive homomorphisms `f`, `g` such that `g.comp f = id` and
   `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`. This
   constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
-  homomorphisms.",
-  simps (config := { fullyApplied := false })]
+  homomorphisms."]
 def MulHom.toMulEquiv [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = MulHom.id _)
   (h₂ : f.comp g = MulHom.id _) : M ≃* N where
   toFun := f
@@ -697,15 +735,32 @@ def MulHom.toMulEquiv [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁
 #align mul_hom.to_mul_equiv MulHom.toMulEquiv
 #align add_hom.to_add_equiv AddHom.toAddEquiv
 
+-- porting note: the next two lemmas were added manually because `@[simps]` is generating
+-- lemmas with `toFun` in
+@[simp, to_additive] theorem MulHom.toMulEquiv_apply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
+    (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.id _) :
+    ((MulHom.toMulEquiv f g h₁ h₂).toEquiv : M → N) = f :=
+  rfl
+#align mul_hom.to_mul_equiv_apply MulHom.toMulEquiv_apply
+#align add_hom.to_add_equiv_apply AddHom.toAddEquiv_apply
+
+@[simp, to_additive] theorem MulHom.toMulEquiv_symmApply [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M)
+    (h₁ : g.comp f = MulHom.id _) (h₂ : f.comp g = MulHom.id _) :
+    (MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂) : N → M) = ↑g :=
+  rfl
+#align mul_hom.to_mul_equiv_symm_apply MulHom.toMulEquiv_symmApply
+#align add_hom.to_add_equiv_symm_apply AddHom.toAddEquiv_symmApply
+
+-- porting note: `@[simps (config := { fullyApplied := false })]` generates a simp lemma
+-- which is not in simp normal form, so we add them manually
 /-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
 returns an multiplicative equivalence with `toFun = f` and `invFun = g`.  This constructor is
 useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms. -/
 @[to_additive
   "Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id`
   and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`.  This
   constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
-  monoid homomorphisms.",
-  simps (config := { fullyApplied := false })]
+  monoid homomorphisms."]
 def MonoidHom.toMulEquiv [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M)
   (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) : M ≃* N where
   toFun := f
@@ -716,6 +771,23 @@ def MonoidHom.toMulEquiv [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N 
 #align monoid_hom.to_mul_equiv MonoidHom.toMulEquiv
 #align add_monoid_hom.to_add_mul_equiv AddMonoidHom.toAddEquiv
 
+-- porting note: the next 2 lemmas should be being generated by
+-- `@[to_additive, simps (config := { fullyApplied := false })]`
+-- but right now it's generating `simp` lemmas which aren't in `simp` normal form.
+@[simp, to_additive] theorem MonoidHom.toMulEquiv_apply [MulOneClass M] [MulOneClass N] (f : M →* N)
+    (g : N →* M) (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) :
+    ((MonoidHom.toMulEquiv f g h₁ h₂).toEquiv : M → N) = ↑f :=
+  rfl
+#align monoid_hom.to_mul_equiv_apply MonoidHom.toMulEquiv_apply
+#align add_monoid_hom.to_add_equiv_apply AddMonoidHom.toAddEquiv_apply
+
+@[simp, to_additive] theorem MonoidHom.toMulEquiv_symmApply [MulOneClass M] [MulOneClass N]
+    (f : M →* N) (g : N →* M) (h₁ : g.comp f = MonoidHom.id _) (h₂ : f.comp g = MonoidHom.id _) :
+    (MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂) : N → M) = g :=
+  rfl
+#align monoid_hom.to_mul_equiv_symm_apply MonoidHom.toMulEquiv_symmApply
+#align add_monoid_hom.to_add_equiv_symm_apply AddMonoidHom.toAddEquiv_symmApply
+
 namespace Equiv
 
 section InvolutiveInv

Mathlib/Algebra/Hom/Equiv/Units/Basic.lean

@@ -220,14 +220,28 @@ end Equiv
 
 -- Porting note: we don't put `@[simp]` on the additive version;
 -- mysteriously simp can already prove that one (although not the multiplicative one)!
+-- porting note: `@[simps apply]` removed because right now it's generating lemmas which
+-- aren't in simp normal form (they contain a `toFun`)
 /-- In a `division_comm_monoid`, `equiv.inv` is a `mul_equiv`. There is a variant of this
 `mul_equiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case. -/
-@[to_additive "When the `add_group` is commutative, `equiv.neg` is an `add_equiv`.", simps apply]
+@[to_additive "When the `add_group` is commutative, `equiv.neg` is an `add_equiv`."]
 def MulEquiv.inv (G : Type _) [DivisionCommMonoid G] : G ≃* G :=
   { Equiv.inv G with toFun := Inv.inv, invFun := Inv.inv, map_mul' := mul_inv }
 #align mul_equiv.inv MulEquiv.inv
 #align add_equiv.neg AddEquiv.neg
 
+-- porting note: this lemma and the next are added manually because `simps` was
+-- not quite generating the right thing
+@[simp] theorem MulEquiv.inv_apply (G : Type _) [DivisionCommMonoid G] (a : G) :
+    (MulEquiv.inv G).toEquiv a = a⁻¹ :=
+  rfl
+#align mul_equiv.inv_apply MulEquiv.inv_apply
+
+@[simp] theorem AddEquiv.neg_apply (G : Type _) [SubtractionCommMonoid G] (a : G) :
+    (AddEquiv.neg G).toEquiv a = -a :=
+  rfl
+#align add_equiv.neg_apply AddEquiv.neg_apply
+
 @[simp]
 theorem MulEquiv.inv_symm (G : Type _) [DivisionCommMonoid G] :
     (MulEquiv.inv G).symm = MulEquiv.inv G :=

Mathlib/Logic/Equiv/Defs.lean

@@ -158,8 +158,15 @@ protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 instance : Trans Equiv Equiv Equiv where
   trans := Equiv.trans
 
--- porting note: this lemma is now useless since coercions are eagerly unfolded
--- @[simp] theorem to_fun_as_coe (e : α ≃ β) : e.toFun = e := rfl
+-- porting note: this is not a syntactic tautology any more because
+-- the coercion from `e` to a function is now `FunLike.coe` not `e.toFun`
+@[simp] theorem to_fun_as_coe (e : α ≃ β) : e.toFun = e := rfl
+
+-- porting note: `simp` should prove this using `to_fun_as_coe`, but it doesn't.
+-- This might be a bug in `simp` -- see https://github.com/leanprover/lean4/issues/1937
+-- If this issue is fixed then the simp linter probably will start complaining, and
+-- this theorem can be deleted hopefully without breaking any `simp` proofs.
+@[simp] theorem to_fun_as_coe_apply (e : α ≃ β) (x : α) : e.toFun x = e x := rfl
 
 @[simp] theorem inv_fun_as_coe (e : α ≃ β) : e.invFun = e.symm := rfl
 

Mathlib/Order/RelIso/Group.lean

@@ -30,14 +30,14 @@ instance : Group (r ≃r r) where
   mul_left_inv f := ext f.symm_apply_apply
 
 @[simp]
-theorem toFun_one : (1 : r ≃r r).toFun = id :=
+theorem coe_one : ((1 : r ≃r r) : α → α) = id :=
   rfl
-#align rel_iso.coe_one RelIso.toFun_one
+#align rel_iso.coe_one RelIso.coe_one
 
 @[simp]
-theorem toFun_mul (e₁ e₂ : r ≃r r) : (e₁ * e₂).toFun = e₁ ∘ e₂ :=
+theorem coe_mul (e₁ e₂ : r ≃r r) : ((e₁ * e₂) : α → α) = e₁ ∘ e₂ :=
   rfl
-#align rel_iso.coe_mul RelIso.toFun_mul
+#align rel_iso.coe_mul RelIso.coe_mul
 
 theorem mul_apply (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x) :=
   rfl