case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.207014
D : Type ?u.207017
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
x✝ : A
⊢ ↑{
          toNonUnitalAlgHom :=
            {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ },
          map_star' := h₅ }
      x✝ =
    ↑f x✝
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.207014
D : Type ?u.207017
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
⊢ {
      toNonUnitalAlgHom :=
        {
          toDistribMulActionHom :=
            { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
          map_mul' := h₄ },
      map_star' := h₅ } =
    f
ext
no goals
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.207014
D : Type ?u.207017
inst✝¹² : Monoid R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : DistribMulAction R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : DistribMulAction R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction R C
inst✝³ : Star C
inst✝² : NonUnitalNonAssocSemiring D
inst✝¹ : DistribMulAction R D
inst✝ : Star D
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x
h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0
h₃ :
  ∀ (x y : A),
    MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) =
      MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y
h₄ :
  ∀ (x y : A),
    MulActionHom.toFun
        { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) =
      MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x *
        MulActionHom.toFun
          { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y
h₅ :
  ∀ (a : A),
    MulActionHom.toFun
        {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
        (star a) =
      star
        (MulActionHom.toFun
          {
                toDistribMulActionHom :=
                  { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
                map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom
          a)
x✝ : A
⊢ ↑{
          toNonUnitalAlgHom :=
            {
              toDistribMulActionHom :=
                { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ },
              map_mul' := h₄ },
          map_star' := h₅ }
      x✝ =
    ↑f x✝
rfl