-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter -
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₂ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        HSMul.hSMul (α := ℝ) (↑n : ℝ) ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₃ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        ((↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ))) • (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₄ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 • (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₅ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) +
          HSMul.hSMul (α := ℝ) 1 (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₆ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter))‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₇ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter) -
          HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.centroid -ᵥ s.circumcenter) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₈ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.circumcenter - (s.centroid -ᵥ s.circumcenter)) -
        (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₉ :
  ‖HSMul.hSMul (α := ℝ) (↑n : ℝ) (s.faceOppositeCentroid i -ᵥ s.centroid) - (s.centroid -ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
rw₁₀ : ‖s.centroid -ᵥ s.points i - (s.centroid -ᵥ s.circumcenter)‖ = ‖s.circumcenter -ᵥ s.points i‖
rw₁₁ rw₁₂ : ‖s.circumcenter -ᵥ s.points i‖ = ‖s.circumcenter -ᵥ s.points i‖
⊢ norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖

Tactic:
rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]

Premises used: norm_smul, vsub_vadd_eq_vsub_sub, smul_smul, one_smul, mul_div_cancel₀, sub_sub, smul_sub, vsub_sub_vsub_cancel_left, add_smul, vsub_sub_vsub_cancel_right, Affine.Simplex.centroid_vsub_point_eq_smul_vsub