case h
F : Type ?u.529418
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.529430
D : Type ?u.529433
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
x✝ : A
⊢ ↑{
          toAlgHom :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                  map_add' := h₄ },
              commutes' := h₅ },
          map_star' := h₆ }
      x✝ =
    ↑f x✝
F : Type ?u.529418
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.529430
D : Type ?u.529433
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
⊢ {
      toAlgHom :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ },
          commutes' := h₅ },
      map_star' := h₆ } =
    f
ext
no goals
case h
F : Type ?u.529418
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.529430
D : Type ?u.529433
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : A →⋆ₐ[R] B
h₁ : ↑f 1 = 1
h₂ :
  ∀ (x y : A),
    OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) =
      OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y
h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₄ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y
h₅ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
              map_add' := h₄ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h₆ :
  ∀ (x : A),
    OneHom.toFun
        (↑↑↑{
                toRingHom :=
                  { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                    map_add' := h₄ },
                commutes' := h₅ })
        (star x) =
      star
        (OneHom.toFun
          (↑↑↑{
                  toRingHom :=
                    { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                      map_add' := h₄ },
                  commutes' := h₅ })
          x)
x✝ : A
⊢ ↑{
          toAlgHom :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃,
                  map_add' := h₄ },
              commutes' := h₅ },
          map_star' := h₆ }
      x✝ =
    ↑f x✝
rfl