-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
N : Type u_2
inst_1 : Monoid N
P : Type u_3
inst_2 : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst_3 : Monoid A
inst_4 : MulDistribMulAction M A
B : Type u_5
inst_5 : Monoid B
inst_6 : MulDistribMulAction N B
B₁ : Type u_6
inst_7 : Monoid B₁
inst_8 : MulDistribMulAction M B₁
C : Type u_7
inst_9 : Monoid C
inst_10 : MulDistribMulAction P C
A' : Type u_8
inst_11 : Group A'
inst_12 : MulDistribMulAction M A'
B' : Type u_9
inst_13 : Group B'
inst_14 : MulDistribMulAction N B'
R : Type u_10
inst_15 : Semiring R
inst_16 : MulSemiringAction M R
R' : Type u_11
inst_17 : Ring R'
inst_18 : MulSemiringAction M R'
S : Type u_12
inst_19 : Semiring S
inst_20 : MulSemiringAction N S
S' : Type u_13
inst_21 : Ring S'
inst_22 : MulSemiringAction N S'
T : Type u_14
inst_23 : Semiring T
inst_24 : MulSemiringAction P T
tG : MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S
map_zero' : tG.toFun 0 = 0
map_add' : ∀ (x y : R), tG.toFun (x + y) = tG.toFun x + tG.toFun y
map_one' : { toMulActionHom := tG, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun 1 = 1
map_mul' :
  ∀ (x y : R),
    { toMulActionHom := tG, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun (x * y) =
      { toMulActionHom := tG, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun x *
        { toMulActionHom := tG, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun y
toFun : R → S
map_smul' :
  ∀ (m : M) (x : R), toFun (m • x) = HSMul.hSMul.{u_2, u_12, u_12} (α := N) ((φ : (a : M) → N) m : N) (toFun x)
map_zero'_1 :
  { toFun := toFun, map_smul' := map_smul' :
          MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
      0 =
    0
map_add'_1 :
  ∀ (x y : R),
    { toFun := toFun, map_smul' := map_smul' :
            MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
        (x + y) =
      { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
          x +
        { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
          y
map_one'_1 :
  { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun 1 = 1
map_mul'_1 :
  ∀ (x y : R),
    { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun
        (x * y) =
      { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun
          x *
        { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun
          y
h :
  Eq (α := (a : R) → S)
    ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
      { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1,
        map_one' := map_one'_1, map_mul' := map_mul'_1 })
    ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
      { toMulActionHom := tG, map_zero' := map_zero', map_add' := map_add', map_one' := map_one',
        map_mul' := map_mul' })
⊢ { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1, map_one' := map_one'_1,
      map_mul' := map_mul'_1 : R →ₑ+*[φ] S } =
    { toMulActionHom := tG, map_zero' := map_zero', map_add' := map_add', map_one' := map_one', map_mul' := map_mul' }
have mk : ∀ (toFun_1 : R → S)
  (map_smul'_1 :
    ∀ (m : M) (x : R), toFun_1 (m • x) = HSMul.hSMul.{u_2, u_12, u_12} (α := N) ((φ : (a : M) → N) m : N) (toFun_1 x))
  (map_zero' :
    { toFun := toFun_1, map_smul' := map_smul'_1 :
            MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
        0 =
      0)
  (map_add' :
    ∀ (x y : R),
      { toFun := toFun_1, map_smul' := map_smul'_1 :
              MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
          (x + y) =
        { toFun := toFun_1, map_smul' := map_smul'_1 :
                MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
            x +
          { toFun := toFun_1, map_smul' := map_smul'_1 :
                MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S }.toFun
            y)
  (map_one' :
    { toFun := toFun_1, map_smul' := map_smul'_1, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun 1 =
      1)
  (map_mul' :
    ∀ (x y : R),
      { toFun := toFun_1, map_smul' := map_smul'_1, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun
          (x * y) =
        { toFun := toFun_1, map_smul' := map_smul'_1, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun
            x *
          { toFun := toFun_1, map_smul' := map_smul'_1, map_zero' := map_zero', map_add' := map_add' :
                R →ₑ+[φ] S }.toFun
            y)
  (h :
    Eq (α := (a : R) → S)
      ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
        { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1,
          map_one' := map_one'_1, map_mul' := map_mul'_1 })
      ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
        { toFun := toFun_1, map_smul' := map_smul'_1, map_zero' := map_zero', map_add' := map_add',
          map_one' := map_one', map_mul' := map_mul' })),
  { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero'_1, map_add' := map_add'_1, map_one' := map_one'_1,
      map_mul' := map_mul'_1 : R →ₑ+*[φ] S } =
    { toFun := toFun_1, map_smul' := map_smul'_1, map_zero' := map_zero', map_add' := map_add', map_one' := map_one',
      map_mul' := map_mul' }
Tactic: cases tG
Cleared hypotheses: tG, map_zero', map_add', map_one', map_mul', h