no goals
R : Type ?u.819565
k : Type u_3
V1 : Type u_1
P1 : Type u_2
V2 : Type ?u.819577
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
r₁ r₂ : k
⊢ homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂
simp only [homothety_def, add_smul, vadd_vadd]