-- Mathlib/Geometry/Euclidean/Basic.lean
/-- The distance between a point and its orthogonal projection to a subspace equals the distance
to that subspace as given by `Metric.infDist`. This is not a `simp` lemma since the simplest form
depends on the context (if any calculations are to be done with the distance, the version with
the orthogonal projection gives access to more lemmas about orthogonal projections that may be
useful). -/
lemma dist_orthogonalProjection_eq_infDist (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    dist p (orthogonalProjection s p) = Metric.infDist p s

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
x : ↑↑s
⊢ dist p ↑((orthogonalProjection s) p) ^ 2 ≤ dist (↑x) p ^ 2

Tactic:
simp_rw [pow_two,
  dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p x.property]

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
x : ↑↑s
⊢ dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p) ≤
    dist ↑x ↑((orthogonalProjection s) p) * dist ↑x ↑((orthogonalProjection s) p) +
      dist p ↑((orthogonalProjection s) p) * dist 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
⊢ dist p ↑((orthogonalProjection s) p) ≤ Metric.infDist p ↑s

Tactic:
rw [Metric.infDist_eq_iInf]

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
⊢ dist p ↑((orthogonalProjection s) p) ≤ ⨅ y, dist p ↑y

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
⊢ dist p ↑((orthogonalProjection s) p) ≤ ⨅ y, dist p ↑y

Tactic:
refine le_ciInf fun x ↦ le_of_sq_le_sq ?_ dist_nonneg

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
x : ↑↑s
⊢ dist p ↑((orthogonalProjection s) p) ^ 2 ≤ dist p ↑x ^ 2

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
⊢ dist p ↑((orthogonalProjection s) p) = Metric.infDist p ↑s

Tactic:
refine le_antisymm ?_ (Metric.infDist_le_dist_of_mem (orthogonalProjection_mem _))

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
⊢ dist p ↑((orthogonalProjection s) p) ≤ Metric.infDist p ↑s

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
x : ↑↑s
⊢ dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p) ≤
    dist ↑x ↑((orthogonalProjection s) p) * dist ↑x ↑((orthogonalProjection s) p) +
      dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)

Tactic:
simp [mul_self_nonneg]

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
x : ↑↑s
⊢ dist p ↑((orthogonalProjection s) p) ^ 2 ≤ dist p ↑x ^ 2

Tactic:
rw [dist_comm _ (x : 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
x : ↑↑s
⊢ dist p ↑((orthogonalProjection s) p) ^ 2 ≤ dist (↑x) p ^ 2