k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s₁ s₂ : Simplex k P n
h✝ : s₁.points '' Set.univ = s₂.points '' Set.univ
h : s₁.points '' ↑Finset.univ = s₂.points '' ↑Finset.univ
⊢ Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s₁ s₂ : Simplex k P n
h : Set.range s₁.points = Set.range s₂.points
⊢ Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points
rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s₁ s₂ : Simplex k P n
h✝ : s₁.points '' Set.univ = s₂.points '' Set.univ
h : s₁.points '' ↑Finset.univ = s₂.points '' ↑Finset.univ
⊢ Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points
exact
  Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
    (fun _ _ _ _ he => AffineIndependent.injective s₁.Independent he)
    (fun _ _ _ _ he => AffineIndependent.injective s₂.Independent he) h