feat(group_theory/group_action/units): simp lemma for scalar action o…

…f `is_unit.unit h` (#14006)

src/algebra/group_with_zero/basic.lean

@@ -7,6 +7,7 @@ import algebra.group.inj_surj
 import algebra.group_with_zero.defs
 import algebra.hom.units
 import logic.nontrivial
+import group_theory.group_action.units
 
 /-!
 # Groups with an adjoined zero element
@@ -722,6 +723,10 @@ begin
     simpa only [eq_comm] using units.exists_iff_ne_zero.mpr h }
 end
 
+@[simp] lemma smul_mk0 {α : Type*} [has_scalar G₀ α] {g : G₀} (hg : g ≠ 0) (a : α) :
+  (mk0 g hg) • a = g • a :=
+rfl
+
 end units
 
 section group_with_zero

src/group_theory/group_action/units.lean

@@ -32,6 +32,10 @@ instance [monoid M] [has_scalar M α] : has_scalar Mˣ α :=
 lemma smul_def [monoid M] [has_scalar M α] (m : Mˣ) (a : α) :
   m • a = (m : M) • a := rfl
 
+@[simp] lemma smul_is_unit [monoid M] [has_scalar M α] {m : M} (hm : is_unit m) (a : α) :
+  hm.unit • a = m • a :=
+rfl
+
 lemma _root_.is_unit.inv_smul [monoid α] {a : α} (h : is_unit a) :
   (h.unit)⁻¹ • a = 1 :=
 h.coe_inv_mul

src/ring_theory/witt_vector/isocrystal.lean

@@ -192,11 +192,9 @@ begin
   intros c,
   rw [linear_equiv.trans_apply, linear_equiv.trans_apply,
       linear_equiv.smul_of_ne_zero_apply, linear_equiv.smul_of_ne_zero_apply,
-      show F (units.mk0 b hb • Φ(p,k) c) = _, from linear_equiv.map_smul _ _ _,
-      show F (units.mk0 b hb • c) = _, from linear_equiv.map_smul _ _ _],
-  simp only [hax, units.coe_mk0, linear_equiv.of_bijective_apply,
-    linear_map.to_span_singleton_apply, linear_equiv.map_smulₛₗ,
-    standard_one_dim_isocrystal.frobenius_apply, algebra.id.smul_eq_mul],
+      linear_equiv.map_smul, linear_equiv.map_smul],
+  simp only [hax, linear_equiv.of_bijective_apply, linear_map.to_span_singleton_apply,
+    linear_equiv.map_smulₛₗ, standard_one_dim_isocrystal.frobenius_apply, algebra.id.smul_eq_mul],
   simp only [←mul_smul],
   congr' 1,
   linear_combination (hmb, φ(p,k) c),