-- Module: Mathlib.GroupTheory.GroupAction.Hom
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 })
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 }
⊢ { 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 }

Tactic:
cases tF