-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
p₁ : P
hp₁ : p₁ ∈ ps
h :
  dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) *
        dist p₁
          (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) +
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
          (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) *
        dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
          (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) =
    cr * cr + ycc₂ * ycc₂
h₁ :
  dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) *
        dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) +
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) *
        dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) =
    cr * cr + ycc₂ * ycc₂
h₂ :
  dist p₁ cc * dist p₁ cc +
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) cc *
        dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) cc =
    cr * cr + ycc₂ * ycc₂
h₃ :
  cr * cr +
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) cc *
        dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) cc =
    cr * cr + ycc₂ * ycc₂
h₄ : cr * cr + ‖cc₂ -ᵥ cc‖ * ‖cc₂ -ᵥ cc‖ = cr * cr + ycc₂ * ycc₂
h₅ :
  cr * cr +
      ‖(ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))‖ *
        ‖(ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))‖ =
    cr * cr + ycc₂ * ycc₂
h₆ :
  cr * cr +
      ‖ycc₂ / y‖ * ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖ *
        (‖ycc₂ / y‖ * ‖p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)‖) =
    cr * cr + ycc₂ * ycc₂
h₇ :
  cr * cr +
      ‖ycc₂ / y‖ * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        (‖ycc₂ / y‖ * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + ycc₂ * ycc₂
h₈ :
  cr * cr +
      |ycc₂ / y| * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        (|ycc₂ / y| * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + ycc₂ * ycc₂
⊢ dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂
have h₉ : cr * cr +
    |ycc₂| / |y| * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
      (|ycc₂| / |y| * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
  cr * cr + ycc₂ * ycc₂
Tactic: rw [dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp₁),
          orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc, Subtype.coe_mk,
          dist_of_mem_subset_mk_sphere hp₁ hcr, dist_eq_norm_vsub V cc₂ cc, vadd_vsub, norm_smul, ←
          dist_eq_norm_vsub V, Real.norm_eq_abs, abs_div, abs_of_nonneg dist_nonneg,
          div_mul_cancel₀ _ hy0, abs_mul_abs_self]