-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem sign_eq_of_affineCombination_mem_affineSpan_pair {p : ι → P} (h : AffineIndependent k p)
    {w w₁ w₂ : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1)
    (hw₂ : ∑ i ∈ s, w₂ i = 1)
    (hs :
      s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂])
    {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0) (hj0 : w₁ j = 0)
    (hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)) :
    SignType.sign (w i) = SignType.sign (w j)

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedRing 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 ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (w i) = SignType.sign (w j)

Tactic:
rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedRing 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 ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
hs : (affineCombination k s p) w ∈ affineSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂}
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
⊢ SignType.sign (w i) = SignType.sign (w j)

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

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedRing 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 ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
hs : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
⊢ SignType.sign (w i) = SignType.sign (w j)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedRing 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 ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
hs : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
⊢ SignType.sign (w i) = SignType.sign (w j)

Tactic:
rcases hs with ⟨r, hr⟩

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedRing 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 ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (w i) = SignType.sign (w j)