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

Proof state:
case mpr
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
⊢ ↑((orthogonalProjection s) p) = p → (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p

Tactic:
intro h

Result:
case mpr
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
h : ↑((orthogonalProjection s) p) = p
⊢ (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection 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
⊢ (reflection s) p = p ↔ p ∈ s

Tactic:
rw [← orthogonalProjection_eq_self_iff, reflection_apply]

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
⊢ (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p ↔ ↑((orthogonalProjection s) p) = p

Proof state:
case mp
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
h : ↑((orthogonalProjection s) p) = p
⊢ ↑((orthogonalProjection s) p) = p

Tactic:
exact h

Result:
no goals

Proof state:
case mp
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
⊢ (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p → ↑((orthogonalProjection s) p) = p

Tactic:
intro h

Result:
case mp
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
h : (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p
⊢ ↑((orthogonalProjection s) p) = p

Proof state:
case mp
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
h : 2 = 0 ∨ ↑((orthogonalProjection s) p) -ᵥ p = 0
⊢ ↑((orthogonalProjection s) p) = p

Tactic:
norm_num at h

Result:
case mp
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
h : ↑((orthogonalProjection s) p) = p
⊢ ↑((orthogonalProjection 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
⊢ (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p ↔ ↑((orthogonalProjection s) p) = p

Tactic:
constructor

Result:
case mp
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
⊢ (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p → ↑((orthogonalProjection s) p) = p

case mpr
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
⊢ ↑((orthogonalProjection s) p) = p → (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p

Proof state:
case mpr
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
h : ↑((orthogonalProjection s) p) = p
⊢ (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p

Tactic:
simp [h]

Result:
no goals

Proof state:
case mp
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
h : (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p) = p
⊢ ↑((orthogonalProjection s) p) = p

Tactic:
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub_assoc, ← two_smul ℝ (↑(orthogonalProjection s p) -ᵥ p),
  smul_eq_zero] at h

Result:
case mp
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
h : 2 = 0 ∨ ↑((orthogonalProjection s) p) -ᵥ p = 0
⊢ ↑((orthogonalProjection s) p) = p