fix(simps): use coercion for algebra morphisms (#4155)

Previously it tried to apply whnf on an open expression, which failed, so it wouldn't find the coercion. Now it applied whnf before opening the expression.

Also use `simps` for `fixed_points.to_alg_hom`. The generated lemmas are
```lean
fixed_points.to_alg_hom_to_fun : ∀ (G : Type u) (F : Type v) [_inst_4 : group G] [_inst_5 : field F]
[_inst_6 : faithful_mul_semiring_action G F],
  ⇑(to_alg_hom G F) =
    λ (g : G),
      {to_fun := (mul_semiring_action.to_semiring_hom G F g).to_fun,
       map_one' := _,
       map_mul' := _,
       map_zero' := _,
       map_add' := _,
       commutes' := _}
```

src/field_theory/fixed.lean

@@ -238,21 +238,14 @@ lemma findim_alg_hom (K : Type u) (V : Type v)
 fintype_card_le_findim_of_linear_independent $ linear_independent_to_linear_map K V
 
 namespace fixed_points
-
 /-- Embedding produced from a faithful action. -/
+@[simps to_fun {fully_applied := ff}]
 def to_alg_hom (G : Type u) (F : Type v) [group G] [field F]
   [faithful_mul_semiring_action G F] : G ↪ (F →ₐ[fixed_points G F] F) :=
 { to_fun := λ g, { commutes' := λ x, x.2 g,
     .. mul_semiring_action.to_semiring_hom G F g },
   inj' := λ g₁ g₂ hg, injective_to_semiring_hom G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, }
 
-@[simp] lemma coe_to_alg_hom (G : Type u) (F : Type v) [group G] [field F]
-  [faithful_mul_semiring_action G F] :
-  (to_alg_hom G F : G → F →ₐ[fixed_points G F] F) =
-    λ g, { commutes' := λ x, x.2 g,
-      .. mul_semiring_action.to_semiring_hom G F g } :=
-rfl
-
 lemma to_alg_hom_apply {G : Type u} {F : Type v} [group G] [field F]
   [faithful_mul_semiring_action G F] (g : G) (x : F) :
   to_alg_hom G F g x = g • x :=

src/tactic/simps.lean

@@ -128,29 +128,31 @@ meta def simps_get_raw_projections (e : environment) (str : name) :
       is_def_eq custom_proj raw_expr <|>
         fail!"Invalid custom projection:\n {custom_proj}\nExpression is not definitionally equal to {raw_expr}.",
       return custom_proj),
-    /- check for other coercions and type-class arguments to use as projections instead. -/
+    /- Check for other coercions and type-class arguments to use as projections instead. -/
     (args, _) ← open_pis d_str.type,
     let e_str := (expr.const str raw_levels).mk_app args,
     automatic_projs ← attribute.get_instances `notation_class,
     raw_exprs ← automatic_projs.mfoldl (λ (raw_exprs : list expr) class_nm, (do
       (is_class, proj_nm) ← notation_class_attr.get_param class_nm,
       proj_nm ← proj_nm <|> (e.structure_fields_full class_nm).map list.head,
+      /- For this class, find the projection. `raw_expr` is the projection found applied to `args`,
+        and `lambda_raw_expr` has the arguments `args` abstracted. -/
       (raw_expr, lambda_raw_expr) ← if is_class then (do
         guard $ args.length = 1,
         let e_inst_type := (expr.const class_nm raw_levels).mk_app args,
         (hyp, e_inst) ← try_for 1000 (mk_conditional_instance e_str e_inst_type),
         raw_expr ← mk_mapp proj_nm [args.head, e_inst],
         clear hyp,
-        raw_expr_lambda ← lambdas [hyp] raw_expr, -- expr.bind_lambda doesn't give the correct type
+        raw_expr_lambda ← lambdas [hyp] raw_expr, -- `expr.bind_lambda` doesn't give the correct type
         return (raw_expr, raw_expr_lambda.lambdas args))
       else (do
         e_inst_type ← to_expr ((expr.const class_nm []).app (pexpr.of_expr e_str)),
         e_inst ← try_for 1000 (mk_instance e_inst_type),
         raw_expr ← mk_mapp proj_nm [e_str, e_inst],
         return (raw_expr, raw_expr.lambdas args)),
-      raw_expr_whnf ← whnf raw_expr.binding_body,
-      let relevant_proj := raw_expr_whnf.get_app_fn.const_name,
-      /- use this as projection, if the function reduces to a projection, and this projection has
+      raw_expr_whnf ← whnf raw_expr,
+      let relevant_proj := raw_expr_whnf.binding_body.get_app_fn.const_name,
+      /- Use this as projection, if the function reduces to a projection, and this projection has
         not been overrriden by the user. -/
       guard (projs.any (= relevant_proj) ∧ ¬ e.contains (str ++ `simps ++ relevant_proj.last)),
       let pos := projs.find_index (= relevant_proj),

test/simps.lean

@@ -497,8 +497,7 @@ run_cmd do e ← get_env, success_if_fail (simps_get_raw_projections e `faulty_m
 end failty_manual_coercion
 
 namespace manual_initialize
-/- defining a manual coercion. This should be made more easily. -/
-
+/- defining a manual coercion. -/
 variables {α β γ : Sort*}
 
 structure equiv (α : Sort*) (β : Sort*) :=
@@ -606,3 +605,24 @@ structure needs_prop_class (n : ℕ) [prop_class n] :=
 
 @[simps] def test_prop_class : needs_prop_class 1 :=
 { t := trivial }
+
+/- check that when the coercion is given in eta-expanded form, we can also find the coercion. -/
+structure alg_hom (R A B : Type*) :=
+(to_fun : A → B)
+
+instance (R A B : Type*) : has_coe_to_fun (alg_hom R A B) := ⟨_, λ f, f.to_fun⟩
+
+@[simps] def my_alg_hom : alg_hom unit bool bool :=
+{ to_fun := id }
+
+example (x : bool) : my_alg_hom x = id x := by simp only [my_alg_hom_to_fun]
+
+structure ring_hom (A B : Type*) :=
+(to_fun : A → B)
+
+instance (A B : Type*) : has_coe_to_fun (ring_hom A B) := ⟨_, λ f, f.to_fun⟩
+
+@[simps] def my_ring_hom : ring_hom bool bool :=
+{ to_fun := id }
+
+example (x : bool) : my_ring_hom x = id x := by simp only [my_ring_hom_to_fun]