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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
⊢ ↑(reflection s₁) p = ↑(reflection s₂) p ↔ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
rw [reflection_apply, reflection_apply]
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p) →
    ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ 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₁ s₂ : AffineSubspace ℝ P
inst✝³ : Nonempty { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p) ↔
    ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
constructor
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h :
  ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
    ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p) →
    ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
intro h
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h : 2 = 0 ∨ ↑(↑(orthogonalProjection s₁) p) -ᵥ ↑(↑(orthogonalProjection s₂) p) = 0
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h :
  ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
    ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
  vsub_sub_vsub_cancel_right, ←
  two_smul ℝ ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p), smul_eq_zero] at h
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h : ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h : 2 = 0 ∨ ↑(↑(orthogonalProjection s₁) p) -ᵥ ↑(↑(orthogonalProjection s₂) p) = 0
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
norm_num at h
no goals
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h : ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
exact h
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h : ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
    ↑(↑(orthogonalProjection s₂) p) -ᵥ 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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
⊢ ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p) →
    ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
      ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
intro h
no goals
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 { x // x ∈ s₁ }
inst✝² : Nonempty { x // x ∈ s₂ }
inst✝¹ : CompleteSpace { x // x ∈ direction s₁ }
inst✝ : CompleteSpace { x // x ∈ direction s₂ }
p : P
h : ↑(↑(orthogonalProjection s₁) p) = ↑(↑(orthogonalProjection s₂) p)
⊢ ↑(↑(orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₁) p) =
    ↑(↑(orthogonalProjection s₂) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s₂) p)
rw [h]