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
this :
  ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ ↑(reflection s) (↑(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
⊢ ↑(reflection s) (↑(reflection s) p) = p
have : ∀ a : s, ∀ b : V, (_root_.orthogonalProjection s.direction) b = 0 →
    reflection s (reflection s (b +ᵥ (a : P))) = b +ᵥ (a : P) := by
  intro _ _ h
  simp [reflection, 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 }
p : P
this :
  ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ ↑(reflection s) (↑(reflection s) (p -ᵥ ↑(↑(orthogonalProjection s) p) +ᵥ ↑(↑(orthogonalProjection s) p))) =
    p -ᵥ ↑(↑(orthogonalProjection s) p) +ᵥ ↑(↑(orthogonalProjection 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
this :
  ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ ↑(reflection s) (↑(reflection s) p) = p
rw [← vsub_vadd p (orthogonalProjection 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
this :
  ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ ↑(reflection s) (↑(reflection s) (p -ᵥ ↑(↑(orthogonalProjection s) p) +ᵥ ↑(↑(orthogonalProjection s) p))) =
    p -ᵥ ↑(↑(orthogonalProjection s) p) +ᵥ ↑(↑(orthogonalProjection s) p)
exact this (orthogonalProjection s p) _ (orthogonalProjection_vsub_orthogonalProjection 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
a✝ : { x // x ∈ s }
b✝ : V
h : ↑(_root_.orthogonalProjection (direction s)) b✝ = 0
⊢ ↑(reflection s) (↑(reflection s) (b✝ +ᵥ ↑a✝)) = b✝ +ᵥ ↑a✝
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
⊢ ∀ (a : { x // x ∈ s }) (b : V),
    ↑(_root_.orthogonalProjection (direction s)) b = 0 → ↑(reflection s) (↑(reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
intro _ _ h
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
a✝ : { x // x ∈ s }
b✝ : V
h : ↑(_root_.orthogonalProjection (direction s)) b✝ = 0
⊢ ↑(reflection s) (↑(reflection s) (b✝ +ᵥ ↑a✝)) = b✝ +ᵥ ↑a✝
simp [reflection, h]