-- Module: Mathlib.Algebra.Algebra.NonUnitalHom
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
f : A → B
map_smul' : ∀ (m : R) (x : A), f (m • x) = HSMul.hSMul.{u₁, w, w} (α := S) ((φ : (a : R) → S) m : S) (f x)
map_zero' :
  { toFun := f, map_smul' := map_smul' : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun 0 =
    0
map_add' :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul' : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := f, map_smul' := map_smul' : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := f, map_smul' := map_smul' :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
map_mul' :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →ₑ+[φ] B }.toFun (x * y) =
      { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →ₑ+[φ] B }.toFun x *
        { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →ₑ+[φ] B }.toFun y
g : A → B
map_smul'_1 : ∀ (m : R) (x : A), g (m • x) = HSMul.hSMul.{u₁, w, w} (α := S) ((φ : (a : R) → S) m : S) (g x)
map_zero'_1 :
  { toFun := g, map_smul' := map_smul'_1 : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
      0 =
    0
map_add'_1 :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'_1 : MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
        (x + y) =
      { toFun := g, map_smul' := map_smul'_1 :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          x +
        { toFun := g, map_smul' := map_smul'_1 :
              MulActionHom.{u, u₁, v, w} (M := R) (N := S) (⇑φ : (a : R) → S) A B }.toFun
          y
map_mul'_1 :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₑ+[φ] B }.toFun
        (x * y) =
      { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₑ+[φ] B }.toFun x *
        { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₑ+[φ] B }.toFun y
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₛₙₐ[φ] B) ↦ f.toFun)
      { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul' })
    ((fun (f : A →ₛₙₐ[φ] B) ↦ f.toFun)
      { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
        map_mul' := map_mul'_1 })
⊢ { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul' :
      A →ₛₙₐ[φ] B } =
    { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1, map_mul' := map_mul'_1 }

Tactic:
congr