-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
inst_10 : Semiring D
inst_11 : Algebra R D
inst_12 : Star D
f : A → B
map_one' : f 1 = 1
map_mul' :
  ∀ (x y : A),
    { toFun := f, map_one' := map_one' : OneHom A B }.toFun (x * y) =
      { toFun := f, map_one' := map_one' : OneHom A B }.toFun x *
        { toFun := f, map_one' := map_one' : OneHom A B }.toFun y
map_zero' : (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun 0 = 0
map_add' :
  ∀ (x y : A),
    (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun y
commutes' :
  ∀ (r : R),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    A →+* B } :
                A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
map_star' :
  ∀ (x : A),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
                      commutes' := commutes' : A →ₐ[R] B }.toRingHom :
                A →* B) :
            OneHom A B).toFun
        (star x) =
      star
        ((↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
                        commutes' := commutes' : A →ₐ[R] B }.toRingHom :
                  A →* B) :
              OneHom A B).toFun
          x)
g : A → B
map_one'_1 : g 1 = 1
map_mul'_1 :
  ∀ (x y : A),
    { toFun := g, map_one' := map_one'_1 : OneHom A B }.toFun (x * y) =
      { toFun := g, map_one' := map_one'_1 : OneHom A B }.toFun x *
        { toFun := g, map_one' := map_one'_1 : OneHom A B }.toFun y
map_zero'_1 : (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun 0 = 0
map_add'_1 :
  ∀ (x y : A),
    (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun y
commutes'_1 :
  ∀ (r : R),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 :
                    A →+* B } :
                A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
map_star'_1 :
  ∀ (x : A),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
                      commutes' := commutes'_1 : A →ₐ[R] B }.toRingHom :
                A →* B) :
            OneHom A B).toFun
        (star x) =
      star
        ((↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
                        map_add' := map_add'_1, commutes' := commutes'_1 : A →ₐ[R] B }.toRingHom :
                  A →* B) :
              OneHom A B).toFun
          x)
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →⋆ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
        commutes' := commutes', map_star' := map_star' })
    ((fun (f : A →⋆ₐ[R] B) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
        commutes' := commutes'_1, map_star' := map_star'_1 })
⊢ { toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
      commutes' := commutes', map_star' := map_star' : A →⋆ₐ[R] B } =
    { toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
      commutes' := commutes'_1, map_star' := map_star'_1 }

Tactic:
congr