-- Mathlib/Analysis/Convex/Between.lean
theorem Sbtw.affineCombination_of_mem_affineSpan_pair [NoZeroDivisors R] [NoZeroSMulDivisors R V]
    {ι : Type*} {p : ι → P} (ha : AffineIndependent R p) {w w₁ w₂ : ι → R} {s : Finset ι}
    (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1)
    (h : s.affineCombination R p w ∈
      line[R, s.affineCombination R p w₁, s.affineCombination R p w₂])
    {i : ι} (his : i ∈ s) (hs : Sbtw R (w₁ i) (w i) (w₂ i)) :
    Sbtw R (s.affineCombination R p w₁) (s.affineCombination R p w)
      (s.affineCombination R p w₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ 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₂)

Tactic:
rw [affineCombination_mem_affineSpan_pair ha hw hw₁ hw₂] at h

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : ∃ r, ∀ 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₂)

Proof state:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ (s.weightedVSub p) (w₁ - w₂) ≠ 0

Tactic:
intro hz

Result:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : (s.weightedVSub p) (w₁ - w₂) = 0
⊢ False

Proof state:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) (r • (w₂ - w₁) + w₁))
    ((Finset.affineCombination R s p) w₂)

Tactic:
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]

Result:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ (s.weightedVSub p) (w₁ - w₂) ≠ 0

Proof state:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ 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₂)

Tactic:
rw [hr i his, sbtw_mul_sub_add_iff] at hs

Result:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ 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₂)

Proof state:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ 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₂)

Tactic:
change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr

Result:
case intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ 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₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : OrderedRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NoZeroDivisors R
inst✝ : NoZeroSMulDivisors R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : (s.weightedVSub p) (w₁ - w₂) = 0
⊢ ∑ i ∈ s, (w₁ - w₂) i = 0

Tactic:
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]

Result:
no goals