∀ {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 : ℕ} (s : Affine.Simplex ℝ P n) {i₁ i₂ : Fin (n + 1)},
  i₁ ≠ i₂ →
    (EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter =
      (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
        (Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)