k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
⊢ (∃ r, ∀ (i : ι), i ∈ s → (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ r, ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i

k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
⊢ ∑ i in s, (w - w₁) i = 0
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
⊢ ↑(Finset.affineCombination k s p) w ∈
      affineSpan k {↑(Finset.affineCombination k s p) w₁, ↑(Finset.affineCombination k s p) w₂} ↔
    ∃ r, ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
rw [← vsub_vadd (s.affineCombination k p w) (s.affineCombination k p w₁),
  AffineSubspace.vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _),
  direction_affineSpan, s.affineCombination_vsub, Set.pair_comm,
  weightedVSub_mem_vectorSpan_pair h _ hw₂ hw₁]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
⊢ (∃ r, ∀ (i : ι), i ∈ s → (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ r, ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
simp only [Pi.sub_apply, sub_eq_iff_eq_add]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
⊢ ∑ i in s, (w - w₁) i = 0
simp_all only [Pi.sub_apply, Finset.sum_sub_distrib, sub_self]