Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        (centroidWeightsWithCircumcenter {i₁, i₂} (pointIndex x) •
                (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) -
              circumcenterWeightsWithCircumcenter n (pointIndex x) •
                (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
            centroidWeightsWithCircumcenter {i₁, i₂} (pointIndex x) •
              (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) -
          reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (pointIndex x) •
            (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)) +
      (centroidWeightsWithCircumcenter {i₁, i₂} circumcenterIndex •
              (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
            circumcenterWeightsWithCircumcenter n circumcenterIndex •
              (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) +
          centroidWeightsWithCircumcenter {i₁, i₂} circumcenterIndex •
            (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
        reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ circumcenterIndex •
          (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0

Tactic:
centroidWeightsWithCircumcenter,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then (↑(#{i₁, i₂}))⁻¹ else 0) •
                (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) -
              circumcenterWeightsWithCircumcenter n (pointIndex x) •
                (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
            (if x ∈ {i₁, i₂} then (↑(#{i₁, i₂}))⁻¹ else 0) •
              (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) -
          reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (pointIndex x) •
            (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)) +
      (0 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
            circumcenterWeightsWithCircumcenter n circumcenterIndex •
              (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) +
          0 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
        reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ circumcenterIndex •
          (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0