R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
h : ∃ r, ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
h :
  ↑(Finset.affineCombination R s p) w ∈
    affineSpan R {↑(Finset.affineCombination R s p) w₁, ↑(Finset.affineCombination R s p) w₂}
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
rw [affineCombination_mem_affineSpan_pair ha hw hw₁ hw₂] at h
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
h : ∃ r, ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
rcases h with ⟨r, hr⟩
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
dsimp only at hr
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
rw [hr i his, sbtw_mul_sub_add_iff] at hs
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁)
    (↑(Finset.affineCombination R s fun x => p x) fun i => (r • (w₂ - w₁) + w₁) i)
    (↑(Finset.affineCombination R s p) w₂)
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁) (↑(Finset.affineCombination R s p) w)
    (↑(Finset.affineCombination R s p) w₂)
rw [s.affineCombination_congr hr fun _ _ => rfl]
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁)
    (↑(Finset.affineCombination R s fun x => p x) fun i => (r • (w₂ - w₁) + w₁) i)
    (↑(Finset.affineCombination R s p) w₂)
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁)
    (↑(Finset.affineCombination R s fun x => p x) fun i => (r • (w₂ - w₁) + w₁) i)
    (↑(Finset.affineCombination R s p) w₂)
dsimp only
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ ↑(Finset.weightedVSub s p) (w₁ - w₂) ≠ 0
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R (↑(Finset.affineCombination R s p) w₁)
    (↑(Finset.affineCombination R s fun x => p x) fun i => (r • (w₂ - w₁) + w₁) i)
    (↑(Finset.affineCombination R s p) w₂)
rw [← s.weightedVSub_vadd_affineCombination, s.weightedVSub_const_smul,
  ← s.affineCombination_vsub, ← lineMap_apply, sbtw_lineMap_iff, and_iff_left hs.2,
  ← @vsub_ne_zero V, s.affineCombination_vsub]
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
⊢ False
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
⊢ ↑(Finset.weightedVSub s p) (w₁ - w₂) ≠ 0
intro hz
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i in s, (w₁ - w₂) i = 0
⊢ False
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
⊢ False
have hw₁w₂ : (∑ i in s, (w₁ - w₂) i) = 0 := by
  simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i in s, (w₁ - w₂) i = 0
⊢ w₁ i = w₂ i
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i in s, (w₁ - w₂) i = 0
⊢ False
refine' hs.1 _
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i in s, (w₁ - w₂) i = 0
ha' : (w₁ - w₂) i = 0
⊢ w₁ i = w₂ i
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i in s, (w₁ - w₂) i = 0
⊢ w₁ i = w₂ i
have ha' := ha s (w₁ - w₂) hw₁w₂ hz i his
no goals
case intro
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i in s, (w₁ - w₂) i = 0
ha' : (w₁ - w₂) i = 0
⊢ w₁ i = w₂ i
rwa [Pi.sub_apply, sub_eq_zero] at ha'
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.333838
P : Type u_4
P' : Type ?u.333844
inst✝⁸ : OrderedRing R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup V'
inst✝³ : Module R V'
inst✝² : AddTorsor V' P'
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_3
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ (i : ι), i ∈ s → w i = (r • (w₂ - w₁) + w₁) i
hz : ↑(Finset.weightedVSub s p) (w₁ - w₂) = 0
⊢ ∑ i in s, (w₁ - w₂) i = 0
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]