-- 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
g : R →ₑ+*[φ] S
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
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) g)
⊢ { toMulActionHom := tF, map_zero' := map_zero', map_add' := map_add', map_one' := map_one', map_mul' := map_mul' :
      R →ₑ+*[φ] S } =
    g
have rcases : ∀ (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 }
Tactic: rcases g with ⟨⟨tG, _, _⟩, _, _⟩
Cleared hypotheses: g, h