-- 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'
tG : MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B
map_one' : tG.toFun 1 = 1
map_mul' : ∀ (x y : A), tG.toFun (x * y) = tG.toFun x * tG.toFun y
toFun : A → B
map_smul' : ∀ (m : M) (x : A), toFun (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((φ : (a : M) → N) m : N) (toFun x)
map_one'_1 :
  { toFun := toFun, map_smul' := map_smul' :
          MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
      1 =
    1
map_mul'_1 :
  ∀ (x y : A),
    { toFun := toFun, map_smul' := map_smul' :
            MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
        (x * y) =
      { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          x *
        { toFun := toFun, map_smul' := map_smul' :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          y
h :
  Eq (α := (a : A) → B)
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun)
      { toFun := toFun, map_smul' := map_smul', map_one' := map_one'_1, map_mul' := map_mul'_1 })
    ((fun (m : A →ₑ*[φ] B) ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one', map_mul' := map_mul' })
⊢ { toFun := toFun, map_smul' := map_smul', map_one' := map_one'_1, map_mul' := map_mul'_1 : A →ₑ*[φ] B } =
    { toMulActionHom := tG, map_one' := map_one', map_mul' := map_mul' }
have mk : ∀ (toFun_1 : A → B)
  (map_smul'_1 :
    ∀ (m : M) (x : A), toFun_1 (m • x) = HSMul.hSMul.{u_2, u_5, u_5} (α := N) ((φ : (a : M) → N) m : N) (toFun_1 x))
  (map_one' :
    { toFun := toFun_1, map_smul' := map_smul'_1 :
            MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
        1 =
      1)
  (map_mul' :
    ∀ (x y : A),
      { toFun := toFun_1, map_smul' := map_smul'_1 :
              MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
          (x * y) =
        { toFun := toFun_1, map_smul' := map_smul'_1 :
                MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
            x *
          { toFun := toFun_1, map_smul' := map_smul'_1 :
                MulActionHom.{u_1, u_2, u_4, u_5} (M := M) (N := N) (⇑φ : (a : M) → N) A B }.toFun
            y)
  (h :
    Eq (α := (a : A) → B)
      ((fun (m : A →ₑ*[φ] B) ↦ m.toFun)
        { toFun := toFun, map_smul' := map_smul', map_one' := map_one'_1, map_mul' := map_mul'_1 })
      ((fun (m : A →ₑ*[φ] B) ↦ m.toFun)
        { toFun := toFun_1, map_smul' := map_smul'_1, map_one' := map_one', map_mul' := map_mul' })),
  { toFun := toFun, map_smul' := map_smul', map_one' := map_one'_1, map_mul' := map_mul'_1 : A →ₑ*[φ] B } =
    { toFun := toFun_1, map_smul' := map_smul'_1, map_one' := map_one', map_mul' := map_mul' }
Tactic: cases tG
Cleared hypotheses: tG, map_one', map_mul', h