awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have 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₂
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mp₈ : ∀ (h : p₂ = (↑((orthogonalProjection s : (a : P) → ↥s) 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mp₉ : ∀ (h : (↑((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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
⊢ dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂
have mpr : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
  dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)
Tactic: nth_rw 4 [← h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = Metric.infDist p (↑s : Set P)
have refine : dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ Metric.infDist p (↑s : Set P)
Tactic: refine le_antisymm ?_ (Metric.infDist_le_dist_of_mem (orthogonalProjection_mem _))
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ Metric.infDist p (↑s : Set P)
have rw : dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ ⨅ (y : (↑(↑s : Set P) : Type u_3)), dist p (↑y : P)
Tactic: rw [Metric.infDist_eq_iInf]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤ ⨅ (y : (↑(↑s : Set P) : Type u_3)), dist p (↑y : P)
have refine : ∀ (x : (↑(↑s : Set P) : Type u_3)),
  HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
    HPow.hPow (β := ℕ) (dist p (↑x : P)) 2
Tactic: refine le_ciInf fun x ↦ le_of_sq_le_sq ?_ dist_nonneg
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
x : (↑(↑s : Set P) : Type u_3)
⊢ HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
    HPow.hPow (β := ℕ) (dist p (↑x : P)) 2
have rw : HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
  HPow.hPow (β := ℕ) (dist (↑x : P) p) 2
Tactic: rw [dist_comm _ (x : P)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
x : (↑(↑s : Set P) : Type u_3)
⊢ HPow.hPow (β := ℕ) (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) 2 ≤
    HPow.hPow (β := ℕ) (dist (↑x : P) p) 2
have simp_rw : dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) ≤
  dist (↑x : P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
      dist (↑x : 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)
Tactic: simp_rw [pow_two,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p x.property]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ nndist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = Metric.infNndist p (↑s : Set P)
have rw : (↑(nndist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : ℝ) = (↑(Metric.infNndist p (↑s : Set P)) : ℝ)
Tactic: rw [← NNReal.coe_inj]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
have rw : ‖(r₁ • v +ᵥ p₁) -ᵥ (r₂ • v +ᵥ p₂)‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ (r₂ • v +ᵥ p₂)‖ =
  ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
Tactic: rw [dist_eq_norm_vsub V (r₁ • v +ᵥ p₁), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul,
        add_comm, add_sub_assoc]