-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
h : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂
mp :
  ∀
    (h :
      HPow.hPow (β := ℕ) (dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)) 2 =
        HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₁ :
  ∀
    (h :
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
          dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
        HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₂ :
  ∀
    (h :
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
          dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
        dist p₁ p₂ * dist p₁ p₂),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₃ :
  ∀
    (h :
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
          dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
        dist p₂ p₁ * dist p₂ p₁),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₄ :
  ∀
    (h :
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
          dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
            dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) +
          dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
            dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₅ :
  ∀
    (h :
      dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
          dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
        0),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₆ :
  ∀
    (h :
      dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = 0 ∨
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = 0),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₇ :
  ∀
    (h :
      p₂ = (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) ∨
        p₂ = (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₈ :
  ∀ (h : p₂ = (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₉ mp₁₀ mp₁₁ mp₁₂ :
  ∀ (h : (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂

Tactic:
rwa [← sq_eq_sq₀ dist_nonneg dist_nonneg, pow_two, pow_two, dist_comm _ p₂,
      dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ hp₂,
      right_eq_add, mul_eq_zero, dist_eq_zero, or_self, eq_comm] at h

Premises used: pow_two, dist_nonneg, dist_comm, eq_comm, mul_eq_zero, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, dist_eq_zero, or_self, sq_eq_sq₀, right_eq_add