-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {t : Finset V}
    (h : ¬AffineIndependent k ((↑) : t → V)) :
    ∃ f : V → k, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
refine ⟨fun x => if hx : x ∈ t then f x hx else (0 : k), ?_, ?_, by use i; simp [f, hi]⟩

Result:
case intro.intro.intro.intro.refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x => if hx : x ∈ t then f x hx else 0) e • e = 0

case intro.intro.intro.intro.refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x => if hx : x ∈ t then f x hx else 0) e = 0

Proof state:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
hwt : (univ.weightedVSub Subtype.val) w = 0
i : { x // x ∈ t }
hi : ¬w i = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
simp only [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w ((↑) : t → V) hw 0,
  vsub_eq_sub, Finset.weightedVSubOfPoint_apply, sub_zero] at hwt

Result:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
case intro.intro.intro.intro.refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0

case intro.intro.intro.intro.refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x => if hx : x ∈ t then f x hx else 0) e = 0

Tactic:
all_goals
  simp only [f, Finset.sum_dite_of_true fun _ h => h, Finset.mk_coe, hwt, hw]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h : ∃ x, ∑ i : { x // x ∈ t }, x i = 0 ∧ (univ.weightedVSub Subtype.val) x = 0 ∧ ∃ x_1, ¬x x_1 = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
obtain ⟨w, hw, hwt, i, hi⟩ := h

Result:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
hwt : (univ.weightedVSub Subtype.val) w = 0
i : { x // x ∈ t }
hi : ¬w i = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h : ¬AffineIndependent k Subtype.val
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
classical
  rw [affineIndependent_iff_of_fintype] at h
  simp only [exists_prop, not_forall] at h
  obtain ⟨w, hw, hwt, i, hi⟩ := h
  simp only [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w ((↑) : t → V) hw 0,
    vsub_eq_sub, Finset.weightedVSubOfPoint_apply, sub_zero] at hwt
  let f : ∀ x : V, x ∈ t → k := fun x hx => w ⟨x, hx⟩
  refine ⟨fun x => if hx : x ∈ t then f x hx else (0 : k), ?_, ?_, by use i; simp [f, hi]⟩
  on_goal 1 =>
    suffices (∑ e ∈ t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by
      convert this
      rename V => x
      by_cases hx : x ∈ t <;> simp [hx]
  all_goals
    simp only [f, Finset.sum_dite_of_true fun _ h => h, Finset.mk_coe, hwt, hw]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h :
  ¬∀ (w : { x // x ∈ t } → k),
      ∑ i : { x // x ∈ t }, w i = 0 → (univ.weightedVSub Subtype.val) w = 0 → ∀ (i : { x // x ∈ t }), w i = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
simp only [exists_prop, not_forall] at h

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h : ∃ x, ∑ i : { x // x ∈ t }, x i = 0 ∧ (univ.weightedVSub Subtype.val) x = 0 ∧ ∃ x_1, ¬x x_1 = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h : ¬AffineIndependent k Subtype.val
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
rw [affineIndependent_iff_of_fintype] at h

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h :
  ¬∀ (w : { x // x ∈ t } → k),
      ∑ i : { x // x ∈ t }, w i = 0 → (univ.weightedVSub Subtype.val) w = 0 → ∀ (i : { x // x ∈ t }), w i = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Proof state:
case intro.intro.intro.intro.refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x => if hx : x ∈ t then f x hx else 0) e • e = 0

Tactic:
suffices (∑ e ∈ t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by
  convert this
  rename V => x
  by_cases hx : x ∈ t <;> simp [hx]

Result:
case intro.intro.intro.intro.refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ∃ x ∈ t, (fun x => if hx : x ∈ t then f x hx else 0) x ≠ 0

Tactic:
use i

Result:
case h
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : { x // x ∈ t } → k
hw : ∑ i : { x // x ∈ t }, w i = 0
i : { x // x ∈ t }
hi : ¬w i = 0
hwt : ∑ x : { x // x ∈ t }, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx => w ⟨x, hx⟩
⊢ ↑i ∈ t ∧ (fun x => if hx : x ∈ t then f x hx else 0) ↑i ≠ 0