Commit 2020-09-16 09:39 6603c6da

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

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