-- 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 : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k (insert (p i₁) (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
rw :
  ∀
    (hs :
      Membership.mem (α := P) (γ := AffineSubspace k P)
        (affineSpan k
          (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
            (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
      ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
rw₁ rw₂ rw₃ :
  ∀
    (hs :
      Membership.mem (α := P) (γ := AffineSubspace k P)
        (affineSpan k
          (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
            (singleton (α := P)
              ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
      ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)
refine_1 :
  ∀
    (hs :
      Membership.mem (α := P) (γ := AffineSubspace k P)
        (affineSpan k
          (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
            (singleton (α := P)
              ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
refine_2 refine_2₁ :
  ∀
    (hs :
      Membership.mem (α := P) (γ := AffineSubspace k P)
        (affineSpan k
          (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
            (singleton (α := P)
              ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₂) : SignType)
      ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₃) : SignType)
refine_2₂ :
  ∀
    (hs :
      Membership.mem (α := P) (γ := AffineSubspace k P)
        (affineSpan k
          (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
            (singleton (α := P)
              ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
        ((affineCombination k s p : (a : ι → k) → P) w : P)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (1 - c) : SignType)
      ((SignType.sign : (a : k) → SignType) c : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)

Tactic:
classical
    rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
    refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
    · rw [Finset.sum_pi_single', if_pos h₁]
    rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
    simp_all only [sub_pos, sign_pos]

Premises used: sub_pos, sign_pos, if_pos, Finset.sum_pi_single'