no goals
k : Type ?u.707847
P₁ : Type u_1
P₂ : Type ?u.707853
P₃ : Type ?u.707856
P₄ : Type ?u.707859
V₁ : Type u_2
V₂ : Type ?u.707865
V₃ : Type ?u.707868
V₄ : Type ?u.707871
inst✝¹⁴ : Ring k
inst✝¹³ : AddCommGroup V₁
inst✝¹² : Module k V₁
inst✝¹¹ : AffineSpace V₁ P₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : Module k V₂
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AffineSpace V₃ P₃
inst✝⁴ : AddCommGroup V₄
inst✝³ : Module k V₄
inst✝² : AffineSpace V₄ P₄
R' : Type u_3
inst✝¹ : CommRing R'
inst✝ : Module R' V₁
c p : P₁
⊢ ↑(homothety c (-1)) p = ↑(pointReflection R' c) p
simp [(homothety_apply), pointReflection_apply _, (neg_vsub_eq_vsub_rev)]