Is this any theorems to solve this problem

Stream: new members

[yulia wang]

I have some difficulities in proving sum_simplex_points_vsub_points_i_eq_sum_faceOpposite_points_i_vsub_points_i , Is this any theorems to solve this problem?

theorem sum_simplex_points_vsub_points_i_eq_sum_faceOpposite_points_i_vsub_points_i (s : Simplex ℝ P n) (i : Fin (n + 1)) :
  ∑ x, ((s.faceOpposite i).points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i) - (s.points i -ᵥ s.points i) := by
  have h: (Set.range (s.faceOpposite i).points) ∪ {s.points i} = Set.range s.points := by
    simp only [range_faceOpposite_points, Set.union_singleton]
    exact Set.insert_image_compl_eq_range s.points i
  sorry

[Ruben Van de Velde]

Please edit your message so the code is a #mwe (you're missing at least the imports)

[yulia wang]

import Mathlib.Geometry.Euclidean.Simplex
import Mathlib.Analysis.Convex.Combination
import Mathlib.Analysis.Normed.Affine.Convex
noncomputable section
namespace Affine
open Finset AffineSubspace EuclideanGeometry
variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [MetricSpace P] [NormedAddTorsor V P]
variable {n : ℕ}
namespace Simplex
abbrev centroid  {n : ℕ} (t : Affine.Simplex ℝ P n) : P :=
  Finset.univ.centroid ℝ t.points
theorem sum_simplex_points_vsub_points_i_eq_sum_faceOpposite_points_i_vsub_points_i (s : Simplex ℝ P n) (i : Fin (n + 1)) :
  ∑ x, ((s.faceOpposite i).points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i) - (s.points i -ᵥ s.points i) := by
  have h: (Set.range (s.faceOpposite i).points) ∪ {s.points i} = Set.range s.points := by
    simp only [range_faceOpposite_points, Set.union_singleton]
    exact Set.insert_image_compl_eq_range s.points i
  sorry