-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
rw :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)
rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - w₁ i) + w₁ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - w₁ j) + w₁ j) : SignType)
rw₂ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0) + 0) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - w₁ j) + w₁ j) : SignType)
rw₃ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0) + 0) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : SignType)
rw₄ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0) + 0) : SignType)
rw₅ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * (w₂ i - 0)) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : SignType)
rw₆ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * (w₂ j - 0)) : SignType)
rw₇ :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (r * w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (r * w₂ j) : SignType)
rw₈ :
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType) =
    (SignType.sign : (a : k) → SignType) (r * w₂ j)
rw₉ :
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType) =
    HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
rw₁₀ rw₁₁ :
  HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType) =
    HMul.hMul (α := SignType) (β := SignType) ((SignType.sign : (a : k) → SignType) r : SignType)
      ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)

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

Premises used: sub_zero, sign_mul, add_zero