-- Mathlib/Geometry/Euclidean/Basic.lean
theorem reflection_eq_iff_orthogonalProjection_eq (s₁ s₂ : AffineSubspace ℝ P) [Nonempty s₁]
    [Nonempty s₂] [HasOrthogonalProjection s₁.direction] [HasOrthogonalProjection s₂.direction]
    (p : P) :
    reflection s₁ p = reflection s₂ p ↔
      (orthogonalProjection s₁ p : P) = orthogonalProjection s₂ 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p) →
    ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h :
  (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
    (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Tactic:
exact 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p) ↔
    ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p) →
    ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p) →
    (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
    (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)

Tactic:
rw [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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ (reflection s₁) p = (reflection s₂) p ↔ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Tactic:
rw [reflection_apply, 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p) ↔
    ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h : 2 = 0 ∨ ↑((orthogonalProjection s₁) p) -ᵥ ↑((orthogonalProjection s₂) p) = 0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p) →
    (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
      (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : HasOrthogonalProjection s₁.direction
inst✝ : HasOrthogonalProjection s₂.direction
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
    (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)