no goals
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category C
D : Type u
inst✝² : Category D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y : C
f : X ⟶ Y
r : R
⊢ (lift R F).map (single f r) = r • F.map f
simp