-- 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
tF : MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S
map_zero' : tF.toFun 0 = 0
map_add' : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y
map_one' : { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun 1 = 1
map_mul' :
  ∀ (x y : R),
    { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun (x * y) =
      { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun x *
        { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun y
tG : MulActionHom.{u_1, u_2, u_10, u_12} (M := M) (N := N) (⇑φ : (a : M) → N) R S
map_zero'_1 : tG.toFun 0 = 0
map_add'_1 : ∀ (x y : R), tG.toFun (x + y) = tG.toFun x + tG.toFun y
map_one'_1 : { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun 1 = 1
map_mul'_1 :
  ∀ (x y : R),
    { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun (x * y) =
      { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1 : R →ₑ+[φ] S }.toFun x *
        { toMulActionHom := tG, 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)
      { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one',
        map_mul' := map_mul' })
    ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
      { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1, map_one' := map_one'_1,
        map_mul' := map_mul'_1 })
⊢ { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one', map_mul' := map_mul' :
      R →ₑ+*[φ] S } =
    { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1, map_one' := map_one'_1,
      map_mul' := map_mul'_1 }
have mk : ∀ (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' :
    { 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' :
    ∀ (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' :
    { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun 1 = 1)
  (map_mul' :
    ∀ (x y : R),
      { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun
          (x * y) =
        { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : R →ₑ+[φ] S }.toFun x *
          { toFun := toFun, map_smul' := map_smul', 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', map_add' := map_add', map_one' := map_one',
          map_mul' := map_mul' })
      ((fun (m : R →ₑ+*[φ] S) ↦ m.toFun)
        { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1, map_one' := map_one'_1,
          map_mul' := map_mul'_1 })),
  { toFun := toFun, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_one' := map_one',
      map_mul' := map_mul' : R →ₑ+*[φ] S } =
    { toMulActionHom := tG, map_zero' := map_zero'_1, map_add' := map_add'_1, map_one' := map_one'_1,
      map_mul' := map_mul'_1 }
Tactic: cases tF
Cleared hypotheses: tF, map_zero', map_add', map_one', map_mul', h