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
hp₁✝ : p₁ ∈ s
hp₁ : ↑(reflection s) p₁ = p₁
p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist 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
hp₁ : p₁ ∈ s
p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist p₁ p₂
rw [← reflection_eq_self_iff p₁] at hp₁
case h.e'_2.h.e'_3
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
hp₁✝ : p₁ ∈ s
hp₁ : ↑(reflection s) p₁ = p₁
p₂ : P
⊢ p₁ = ↑(reflection s) 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
hp₁✝ : p₁ ∈ s
hp₁ : ↑(reflection s) p₁ = p₁
p₂ : P
⊢ dist p₁ (↑(reflection s) p₂) = dist p₁ p₂
convert(reflection s).dist_map p₁ p₂
no goals
case h.e'_2.h.e'_3
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
hp₁✝ : p₁ ∈ s
hp₁ : ↑(reflection s) p₁ = p₁
p₂ : P
⊢ p₁ = ↑(reflection s) p₁
rw [hp₁]