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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
hs : ∃ r, ∀ (i : ι), 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)
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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
hs :
  ↑(Finset.affineCombination k s p) w ∈
    affineSpan k {↑(Finset.affineCombination k s p) w₁, ↑(Finset.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)
rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs
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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in 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 : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ ↑SignType.sign (w i) = ↑SignType.sign (w j)
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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
hs : ∃ r, ∀ (i : ι), 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)
rcases hs with ⟨r, hr⟩
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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in 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 : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ ↑SignType.sign (w i) = ↑SignType.sign (w j)
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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in 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 : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ ↑SignType.sign (w i) = ↑SignType.sign (w j)
dsimp only at hr
no goals
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 in s, w i = 1
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in 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 : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i
⊢ ↑SignType.sign (w i) = ↑SignType.sign (w j)
rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]