k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
⊢ ↑(affineCombination k univ Subtype.val) (centroidWeights k univ) =
    ↑(affineCombination k (attach s) Subtype.val) (centroidWeights k s ∘ Subtype.val)
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
⊢ centroid k univ Subtype.val = centroid k s id
rw [centroid, centroid, ← s.attach_affineCombination_coe]
case h.e_6.h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
⊢ centroidWeights k univ = centroidWeights k s ∘ Subtype.val
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
⊢ ↑(affineCombination k univ Subtype.val) (centroidWeights k univ) =
    ↑(affineCombination k (attach s) Subtype.val) (centroidWeights k s ∘ Subtype.val)
congr
case h.e_6.h.h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
x✝ : { x // x ∈ s }
⊢ centroidWeights k univ x✝ = (centroidWeights k s ∘ Subtype.val) x✝
case h.e_6.h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
⊢ centroidWeights k univ = centroidWeights k s ∘ Subtype.val
ext
no goals
case h.e_6.h.h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.475884
s✝ : Finset ι
ι₂ : Type ?u.475890
s₂ : Finset ι₂
s : Finset P
x✝ : { x // x ∈ s }
⊢ centroidWeights k univ x✝ = (centroidWeights k s ∘ Subtype.val) x✝
simp