-- Mathlib/Geometry/Euclidean/Basic.lean
theorem reflection_reflection (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) : reflection s (reflection s p) = p

Proof state:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
this :
  ∀ (a : ↥s) (b : V),
    (_root_.orthogonalProjection s.direction) b = 0 → (reflection s) ((reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ (reflection s) ((reflection s) p) = p

Tactic:
rw [← vsub_vadd p (orthogonalProjection s p)]

Result:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
this :
  ∀ (a : ↥s) (b : V),
    (_root_.orthogonalProjection s.direction) 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)

Proof state:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ∀ (a : ↥s) (b : V),
    (_root_.orthogonalProjection s.direction) b = 0 → (reflection s) ((reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a

Tactic:
intro _ _ h

Result:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
a✝ : ↥s
b✝ : V
h : (_root_.orthogonalProjection s.direction) b✝ = 0
⊢ (reflection s) ((reflection s) (b✝ +ᵥ ↑a✝)) = b✝ +ᵥ ↑a✝

Proof state:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
a✝ : ↥s
b✝ : V
h : (_root_.orthogonalProjection s.direction) b✝ = 0
⊢ (reflection s) ((reflection s) (b✝ +ᵥ ↑a✝)) = b✝ +ᵥ ↑a✝

Tactic:
simp [reflection, h]

Result:
no goals

Proof state:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ (reflection s) ((reflection s) p) = p

Tactic:
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]

Result:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
this :
  ∀ (a : ↥s) (b : V),
    (_root_.orthogonalProjection s.direction) b = 0 → (reflection s) ((reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a
⊢ (reflection s) ((reflection s) p) = p

Proof state:
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 ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
this :
  ∀ (a : ↥s) (b : V),
    (_root_.orthogonalProjection s.direction) 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)

Tactic:
exact this (orthogonalProjection s p) _ (orthogonalProjection_vsub_orthogonalProjection s p)

Result:
no goals