no goals
R✝ : Type ?u.168559
A✝ : Type ?u.168562
inst✝¹³ : Semiring R✝
inst✝¹² : StarSemigroup R✝
inst✝¹¹ : TrivialStar R✝
inst✝¹⁰ : AddCommGroup A✝
inst✝⁹ : Module R✝ A✝
inst✝⁸ : StarAddMonoid A✝
inst✝⁷ : StarModule R✝ A✝
inst✝⁶ : Invertible 2
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarSemigroup A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
⊢ ↑(algebraMap R A) (star r) = star (↑(algebraMap R A) r)
simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]