[GOAL]
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TrivialStar R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : StarAddMonoid A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousStar A
src✝ : A ≃+ A := AddEquiv.refl A
r : R
a : A
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : A), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • a) =
    ↑(starRingEnd R) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : A), Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        a
[PROOFSTEP]
simp [starRingEnd_apply]
