no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type ?u.279611
s✝ : Finset ι
ι₂ : Type ?u.279617
s₂ : Finset ι₂
s : Finset P
w : P → k
⊢ ↑(affineCombination k (attach s) Subtype.val) (w ∘ Subtype.val) = ↑(affineCombination k s id) w
classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
    univ_eq_attach, attach_image_val]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type ?u.279611
s✝ : Finset ι
ι₂ : Type ?u.279617
s₂ : Finset ι₂
s : Finset P
w : P → k
⊢ ↑(affineCombination k (attach s) Subtype.val) (w ∘ Subtype.val) = ↑(affineCombination k s id) w
rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
univ_eq_attach, attach_image_val]