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
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p ↔ ↑(↑(orthogonalProjection 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) p = p ↔ p ∈ s
rw [← orthogonalProjection_eq_self_iff, 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
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 { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) p) = p → ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection 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
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p ↔ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p → ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : 2 = 0 ∨ ↑(↑(orthogonalProjection s) p) -ᵥ p = 0
⊢ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) = p
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub_assoc, ← two_smul ℝ (↑(orthogonalProjection s p) -ᵥ 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : 2 = 0 ∨ ↑(↑(orthogonalProjection s) p) -ᵥ p = 0
⊢ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : ↑(↑(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 { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
⊢ ↑(↑(orthogonalProjection s) p) = p → ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = 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 : AffineSubspace ℝ P
inst✝¹ : Nonempty { x // x ∈ s }
inst✝ : CompleteSpace { x // x ∈ direction s }
p : P
h : ↑(↑(orthogonalProjection s) p) = p
⊢ ↑(↑(orthogonalProjection s) p) -ᵥ p +ᵥ ↑(↑(orthogonalProjection s) p) = p
simp [h]