awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
h : ¬AffineIndependent k (P := V) (ι := ↥t) (Subtype.val (p := fun (x : V) ↦ x ∈ t))
⊢ ¬∀ (w : ↥t → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ (Subtype.val (p := fun (x : V) ↦ x ∈ t)) : (a : ↥t → k) → V) w : V)
            (0 : V) →
          ∀ (i : ↥t), w i = 0

Tactic:
rw [affineIndependent_iff_of_fintype] at h

Premises used: affineIndependent_iff_of_fintype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
h :
  ¬∀ (w : ↥t → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ (Subtype.val (p := fun (x : V) ↦ x ∈ t)) : (a : ↥t → k) → V) w : V)
            (0 : V) →
          ∀ (i : ↥t), w i = 0
⊢ ∃ (x : ↥t → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ↥t, x i) 0 ∧
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ (Subtype.val (p := fun (x : V) ↦ x ∈ t)) : (a : ↥t → k) → V) x : V)
          (0 : V) ∧
        ∃ (x_1 : ↥t), ¬x x_1 = 0

Tactic:
simp only [exists_prop, not_forall] at h

Premises used: exists_prop, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
h :
  ∃ (x : ↥t → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ↥t, x i) 0 ∧
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ (Subtype.val (p := fun (x : V) ↦ x ∈ t)) : (a : ↥t → k) → V) x : V)
          (0 : V) ∧
        ∃ (x_1 : ↥t), ¬x x_1 = 0
obtain :
  ∀ (w : ↥t → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0)
    (hwt :
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ (Subtype.val (p := fun (x : V) ↦ x ∈ t)) : (a : ↥t → k) → V) w : V)
        (0 : V))
    (i : ↥t) (hi : ¬w i = 0),
    ∃ (f : V → k), Eq (α := V) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := k) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
⊢ ∃ (f : V → k), Eq (α := V) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := k) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
obtain ⟨w, hw, hwt, i, hi⟩ := h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
hwt :
  Eq.{u_2 + 1} (α := V) ((weightedVSub univ (Subtype.val (p := fun (x : V) ↦ x ∈ t)) : (a : ↥t → k) → V) w : V) (0 : V)
i : ↥t
hi : ¬w i = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 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

Premises used: Finset.weightedVSubOfPoint_apply, sub_zero, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, OfNat.ofNat, Subtype.val, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
h : (↑i : V) ∈ t ∧ Ne.{u_1 + 1} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) (↑i : V)) 0
⊢ ∃ x ∈ t, Ne.{u_1 + 1} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) 0

Tactic:
use i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
⊢ (↑i : V) ∈ t ∧ Ne.{u_1 + 1} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) (↑i : V)) 0

Tactic:
simp [f, hi]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
refine_1 :
  Eq (α := V)
    (∑ e ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) e) e) 0
refine_2 : Eq.{u_1 + 1} (α := k) (∑ e ∈ t, (fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) e) 0
⊢ ∃ (f : V → k), Eq (α := V) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := k) (∑ 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]⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
this : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
⊢ Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0

Tactic:
this
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
this : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
h :
  ∀ x ∈ t,
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) x =
      if hx : x ∈ t then f x hx • x else 0
⊢ Eq (α := V)
    (∑ e ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) e) e) 0

Tactic:
convert! this
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
this : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
x : V
h : x ∈ t
pos :
  ∀ (hx : x ∈ t),
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) x =
      if hx : x ∈ t then f x hx • x else 0
neg :
  ∀ (hx : x ∉ t),
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) x =
      if hx : x ∈ t then f x hx • x else 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) x =
    if hx : x ∈ t then f x hx • x else 0

Tactic:
by_cases hx : x ∈ t
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
this : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
x : V
h hx : x ∈ t
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) x =
    if hx : x ∈ t then f x hx • x else 0

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
this : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
x : V
h : x ∈ t
hx : x ∉ t
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) x) x =
    if hx : x ∈ t then f x hx • x else 0

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
refine_1 : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
⊢ Eq (α := V)
    (∑ e ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) 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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
refine_1 : Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0
⊢ Eq (α := V)
    (∑ e ∈ t, HSMul.hSMul.{u_1, u_2, u_2} (α := k) ((fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) e) e) 0

Tactic:
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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
⊢ Eq (α := V) (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) 0

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

Premises used: Finset.mk_coe, Finset.sum_dite_of_true
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
t : Finset V
w : ↥t → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : ↥t, w i) 0
i : ↥t
hi : ¬w i = 0
hwt : Eq.{u_2 + 1} (α := V) (∑ x : ↥t, w x • (↑x : V)) 0
f : (x : V) → x ∈ t → k := fun (x : V) (hx : x ∈ t) ↦ w (Subtype.mk (p := fun (x : V) ↦ x ∈ t) x hx)
⊢ Eq.{u_1 + 1} (α := k) (∑ e ∈ t, (fun (x : V) ↦ (if hx : x ∈ t then f x hx else 0 : k)) e) 0

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

Premises used: Finset.mk_coe, Finset.sum_dite_of_true
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_5
p : ι → V
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ (Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V) → ∀ i ∈ s, w i = 0) ↔
    Eq.{u_2 + 1} (α := V) (∑ e ∈ s, w e • p e) 0 → ∀ e ∈ s, w e = 0

Tactic:
simp [s.weightedVSub_eq_linear_combination hw]

Premises used: Finset.weightedVSub_eq_linear_combination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → V
hp : AffineIndependent k p
hw₀ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • p i) 0
⊢ ∀ i ∈ s, w i = 0

Tactic:
affineIndependent_iff.1 hp _ _ hw₀ hw₁

Premises used: affineIndependent_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • p i) (∑ i ∈ s, w₂ i • p i)
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
fun i hi ↦ sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero (w := w₁ - w₂) ?_ ?_ _ hi)

Premises used: sub_eq_zero, Iff.mp, AffineIndependent.eq_zero_of_sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • p i) (∑ i ∈ s, w₂ i • p i)
refine_1 : ∀ (i : ι) (hi : i ∈ s), Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (w₁ - w₂) i) 0
refine_2 : ∀ (i : ι) (hi : i ∈ s), Eq.{u_2 + 1} (α := V) (∑ i ∈ s, (w₁ - w₂) i • p i) 0
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine fun i hi ↦ sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero (w := w₁ - w₂) ?_ ?_ _ hi)

Premises used: sub_eq_zero, Iff.mp, AffineIndependent.eq_zero_of_sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • p i) (∑ i ∈ s, w₂ i • p i)
i : ι
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (w₁ - w₂) i) 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, sub_mul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • p i) (∑ i ∈ s, w₂ i • p i)
i : ι
hi : i ∈ s
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, (w₁ - w₂) i • p i) 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, sub_mul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w : V → k
hw₀ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, w x) 0
hw₁ : Eq (α := V) (∑ x ∈ s, w x • x) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s.attach, w (↑x : V)) 0

Tactic:
rw [← sum_attach] at hw₀ hw₁

Premises used: Finset.sum_attach
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w : V → k
hw₀ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s, w x) 0
hw₁ : Eq (α := V) (∑ x ∈ s, w x • x) 0
hw₂ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s.attach, w (↑x : V)) 0
⊢ Eq (α := V) (∑ x ∈ s.attach, w (↑x : V) • (↑x : V)) 0

Tactic:
rw [← sum_attach] at hw₀ hw₁

Premises used: Finset.sum_attach
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w : V → k
hw₀ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s.attach, w (↑x : V)) 0
hw₁ : Eq (α := V) (∑ x ∈ s.attach, w (↑x : V) • (↑x : V)) 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
fun x hx ↦ hp.eq_zero_of_sum_eq_zero hw₀ hw₁ ⟨x, hx⟩ (mem_univ _)

Premises used: Finset.mem_univ, Subtype.mk, AffineIndependent.eq_zero_of_sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w : V → k
hw₀ : Eq.{u_1 + 1} (α := k) (∑ x ∈ s.attach, w (↑x : V)) 0
hw₁ : Eq (α := V) (∑ x ∈ s.attach, w (↑x : V) • (↑x : V)) 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
exact fun x hx ↦ hp.eq_zero_of_sum_eq_zero hw₀ hw₁ ⟨x, hx⟩ (mem_univ _)

Premises used: Finset.mem_univ, Subtype.mk, AffineIndependent.eq_zero_of_sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w₁ w₂ : V → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq (α := V) (∑ i ∈ s, w₁ i • i) (∑ i ∈ s, w₂ i • i)
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi)

Premises used: sub_eq_zero, Iff.mp, AffineIndependent.eq_zero_of_sum_eq_zero_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w₁ w₂ : V → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq (α := V) (∑ i ∈ s, w₁ i • i) (∑ i ∈ s, w₂ i • i)
refine_1 : ∀ (i : V) (hi : i ∈ s), Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (w₁ - w₂) x) 0
refine_2 : ∀ (i : V) (hi : i ∈ s), Eq (α := V) (∑ x ∈ s, (w₁ - w₂) x • x) 0
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi)

Premises used: sub_eq_zero, Iff.mp, AffineIndependent.eq_zero_of_sum_eq_zero_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w₁ w₂ : V → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq (α := V) (∑ i ∈ s, w₁ i • i) (∑ i ∈ s, w₂ i • i)
i : V
hi : i ∈ s
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s, (w₁ - w₂) x) 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, sub_mul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Finset V
hp : AffineIndependent k (P := V) (ι := ↥s) (Subtype.val (p := fun (x : V) ↦ x ∈ s))
w₁ w₂ : V → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) (∑ i ∈ s, w₂ i)
hwp : Eq (α := V) (∑ i ∈ s, w₁ i • i) (∑ i ∈ s, w₂ i • i)
i : V
hi : i ∈ s
⊢ Eq (α := V) (∑ x ∈ s, (w₁ - w₂) x • x) 0

Tactic:
simpa [sub_mul, sub_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, sub_mul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
rw :
  (∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ Membership.mem (α := V) (γ := Submodule k V)
      (vectorSpan k (P := P)
        (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          (singleton (α := P) ((affineCombination k s p : (a : ι → k) → P) w₂ : P))))
      ((s.weightedVSub p : (a : ι → k) → V) w : V) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
rw [mem_vectorSpan_pair]

Premises used: mem_vectorSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
⊢ (∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
refine_1 :
  ∀
    (h :
      ∃ (r : k),
        r •
            VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
              ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
          (s.weightedVSub p : (a : ι → k) → V) w),
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
refine_2 :
  ∀ (h : ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)),
    ∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w
⊢ (∃ (r : k),
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w) ↔
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
h_1 : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
h :
  ∃ (r : k),
    r •
        VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
          ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
      (s.weightedVSub p : (a : ι → k) → V) w
refine_1 :
  ∀ (r : k)
    (hr :
      r •
          VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
        (s.weightedVSub p : (a : ι → k) → V) w),
    ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
rcases h with ⟨r, hr⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : 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) 0
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
r : k
hr :
  r •
      VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) w
⊢ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
⟨r, fun i hi => ?_⟩

Premises used: Exists.intro