no goals
𝕜 : Type ?u.2147195
V : Type u_2
V₁ : Type ?u.2147201
V₂ : Type ?u.2147204
V₃ : Type ?u.2147207
V₄ : Type ?u.2147210
P₁ : Type ?u.2147213
P : Type u_1
P₂ : Type ?u.2147219
P₃ : Type ?u.2147222
P₄ : Type ?u.2147225
inst✝²² : NormedField 𝕜
inst✝²¹ : SeminormedAddCommGroup V
inst✝²⁰ : SeminormedAddCommGroup V₁
inst✝¹⁹ : SeminormedAddCommGroup V₂
inst✝¹⁸ : SeminormedAddCommGroup V₃
inst✝¹⁷ : SeminormedAddCommGroup V₄
inst✝¹⁶ : NormedSpace 𝕜 V
inst✝¹⁵ : NormedSpace 𝕜 V₁
inst✝¹⁴ : NormedSpace 𝕜 V₂
inst✝¹³ : NormedSpace 𝕜 V₃
inst✝¹² : NormedSpace 𝕜 V₄
inst✝¹¹ : PseudoMetricSpace P
inst✝¹⁰ : MetricSpace P₁
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : PseudoMetricSpace P₃
inst✝⁷ : PseudoMetricSpace P₄
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddTorsor V₁ P₁
inst✝⁴ : NormedAddTorsor V₂ P₂
inst✝³ : NormedAddTorsor V₃ P₃
inst✝² : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type ?u.2147749
inst✝¹ : TopologicalSpace α
inst✝ : NormedSpace ℝ V
x y : P
⊢ dist (↑(pointReflection ℝ x) y) y = 2 * dist x y
rw [dist_pointReflection_self, Real.norm_two]