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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
⊢ ↑(affineCombination k (attach s) f) (w ∘ f) = ↑(affineCombination k (image f univ) id) w
simp only [affineCombination, weightedVSubOfPoint_apply, id.def, vadd_right_cancel_iff,
  Function.comp_apply, AffineMap.coe_mk]
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
let g₁ : s → V := fun i => w (f i) • (f i -ᵥ Classical.choice S.Nonempty)
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
let g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice S.Nonempty)
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ Finset.sum univ g₁ = Finset.sum (image f univ) g₂
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
change univ.sum g₁ = (image f univ).sum g₂
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ Finset.sum univ g₁ = Finset.sum (image f univ) g₂
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ Finset.sum univ g₁ = Finset.sum (image f univ) g₂
have hgf : g₁ = g₂ ∘ f := by
  ext
  simp
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ Finset.sum univ (g₂ ∘ f) = ∑ x : { x // x ∈ s }, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P))

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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → ∀ (y : { x // x ∈ s }), y ∈ univ → f x = f y → x = y
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ Finset.sum univ g₁ = Finset.sum (image f univ) g₂
rw [hgf, sum_image]
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → ∀ (y : { x // x ∈ s }), y ∈ univ → f x = f y → x = y
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ Finset.sum univ (g₂ ∘ f) = ∑ x : { x // x ∈ s }, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P))

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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → ∀ (y : { x // x ∈ s }), y ∈ univ → f x = f y → x = y
simp only [Function.comp_apply]
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → ∀ (y : { x // x ∈ s }), y ∈ univ → f x = f y → x = y
exact fun _ _ _ _ hxy => hf hxy
case h
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
x✝ : { x // x ∈ s }
⊢ g₁ x✝ = (g₂ ∘ f) x✝
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ g₁ = g₂ ∘ f
ext
no goals
case h
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.269506
s✝ : Finset ι
ι₂ : Type ?u.269512
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
x✝ : { x // x ∈ s }
⊢ g₁ x✝ = (g₂ ∘ f) x✝
simp