-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one {w : ι → k} {p : ι → P}
    (hw : s.weightedVSub p w = (0 : V)) {i : ι} [DecidablePred (· ≠ i)] (his : i ∈ s)
    (hwi : w i = -1) : {x ∈ s | x ≠ i}.affineCombination k p w = p i

Proof state:
case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = (affineCombination k {i} p) (-w)

Tactic:
refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm

Result:
case e_a.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (-w) i = 1

case e_a.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ i2 ∈ {i}, i2 ≠ i → (-w) i2 = 0

Proof state:
case e_a.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ i2 ∈ {i}, i2 ≠ i → (-w) i2 = 0

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k (filter (fun x => x ≠ i) s) p) w -ᵥ p i =
    (affineCombination k (filter (fun a => a ≠ i) s) p) w -ᵥ (affineCombination k {i} p) (-w)

Tactic:
congr

Result:
case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = (affineCombination k {i} p) (-w)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k (filter (fun x => x ≠ i) s) p) w = p i

Tactic:
rw [← @vsub_eq_zero_iff_eq V, ← hw,
  ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
  ← filter_ne']

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k (filter (fun x => x ≠ i) s) p) w -ᵥ p i =
    (affineCombination k (filter (fun a => a ≠ i) s) p) w -ᵥ (affineCombination k {i} p) (-w)

Proof state:
case e_a.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (-w) i = 1

Tactic:
simp [hwi]

Result:
no goals