V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p₁ p₂ : P
⊢ dist (↑(reflection s) (↑(reflection s) p₁)) (↑(reflection s) p₂) = dist (↑(reflection s) p₁) p₂
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p₁ p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist (↑(reflection s) p₁) p₂
conv_lhs => rw [← reflection_reflection s p₁]
no goals
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p₁ p₂ : P
⊢ dist (↑(reflection s) (↑(reflection s) p₁)) (↑(reflection s) p₂) = dist (↑(reflection s) p₁) p₂
exact (reflection s).dist_map _ _