no goals
k : Type u₁
G : Type u₂
R : Type ?u.2710730
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2710767
inst✝¹ : Semiring B
inst✝ : Algebra k B
F : Multiplicative G →* A
a : G
b : k
⊢ ↑(↑(lift k G A) F) (single a b) = b • ↑F (↑Multiplicative.ofAdd a)
rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]