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' := _}
```
