case h
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 }
x✝ : P
⊢ ↑(AffineIsometryEquiv.symm (reflection s)) x✝ = ↑(reflection s) x✝
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 }
⊢ AffineIsometryEquiv.symm (reflection s) = reflection s
ext
case h
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 }
x✝ : P
⊢ ↑(reflection s) (↑(AffineIsometryEquiv.symm (reflection s)) x✝) = ↑(reflection s) (↑(reflection s) x✝)
case h
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 }
x✝ : P
⊢ ↑(AffineIsometryEquiv.symm (reflection s)) x✝ = ↑(reflection s) x✝
rw [← (reflection s).injective.eq_iff]
no goals
case h
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 }
x✝ : P
⊢ ↑(reflection s) (↑(AffineIsometryEquiv.symm (reflection s)) x✝) = ↑(reflection s) (↑(reflection s) x✝)
simp