-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
inst_10 : NonUnitalNonAssocSemiring D
inst_11 : DistribMulAction R D
inst_12 : Star D
f : A → B
map_smul' : ∀ (m : R) (x : A), f (m • x) = HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) m : R) (f x)
map_zero' :
  { toFun := f, map_smul' := map_smul' : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
      0 =
    0
map_add' :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul' : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
        (x + y) =
      { toFun := f, map_smul' := map_smul' :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          x +
        { toFun := f, map_smul' := map_smul' :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          y
map_mul' :
  ∀ (x y : A),
    { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →+[R] B }.toFun (x * y) =
      { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →+[R] B }.toFun x *
        { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add' : A →+[R] B }.toFun y
map_star' :
  ∀ (a : A),
    { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul' :
            A →ₙₐ[R] B }.toFun
        (star a) =
      star
        ({ toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul' :
              A →ₙₐ[R] B }.toFun
          a)
g : A → B
map_smul'_1 : ∀ (m : R) (x : A), g (m • x) = HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) m : R) (g x)
map_zero'_1 :
  { toFun := g, map_smul' := map_smul'_1 : MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
      0 =
    0
map_add'_1 :
  ∀ (x y : A),
    { toFun := g, map_smul' := map_smul'_1 :
            MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
        (x + y) =
      { toFun := g, map_smul' := map_smul'_1 :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          x +
        { toFun := g, map_smul' := map_smul'_1 :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) 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 →+[R] B }.toFun
        (x * y) =
      { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →+[R] B }.toFun x *
        { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →+[R] B }.toFun y
map_star'_1 :
  ∀ (a : A),
    { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1, map_mul' := map_mul'_1 :
            A →ₙₐ[R] B }.toFun
        (star a) =
      star
        ({ toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
              map_mul' := map_mul'_1 : A →ₙₐ[R] B }.toFun
          a)
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →⋆ₙₐ[R] B) ↦ f.toFun)
      { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul',
        map_star' := map_star' })
    ((fun (f : A →⋆ₙₐ[R] 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,
        map_star' := map_star'_1 })
⊢ { toFun := f, map_smul' := map_smul', map_zero' := map_zero', map_add' := map_add', map_mul' := map_mul',
      map_star' := map_star' : A →⋆ₙₐ[R] B } =
    { toFun := g, map_smul' := map_smul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1, map_mul' := map_mul'_1,
      map_star' := map_star'_1 }

Tactic:
congr