awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
⟨s \ t, Finset.sdiff_subset, f, ?_, i, Finset.mem_sdiff.2 ⟨hi, hi'⟩, hfi⟩

Premises used: Iff.mpr, Finset.mem_sdiff, SDiff.sdiff, And.intro, Exists.intro, Finset.sdiff_subset
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
neg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s \ t, f i • v i) (∑ i ∈ s \ (s \ t), f i • v i)
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨s \ t, Finset.sdiff_subset, f, ?_, i, Finset.mem_sdiff.2 ⟨hi, hi'⟩, hfi⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s \ t, f i • v i) (∑ i ∈ s \ (s \ t), f i • v i)

Tactic:
simpa [Finset.sdiff_sdiff_eq_self hst] using heq.symm

Premises used: Finset.sdiff_sdiff_eq_self, Eq.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : LinearIndependent R v
f g : ι →₀ R
h :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R (-v) : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R (-v) : (a : ι →₀ R) → M) g : M)
⊢ Eq.{u_4 + 1} (α := M) (f.sum fun (a : ι) (b : R) ↦ b • v a) (g.sum fun (a : ι) (b : R) ↦ b • v a)

Tactic:
simp only [Finsupp.linearCombination_apply, Pi.neg_apply, smul_neg, Finsupp.sum_neg, neg_inj] at h

Premises used: smul_neg, Finsupp.sum_neg, Finsupp.linearCombination_apply, neg_inj, Pi.neg_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : LinearIndependent R v
f g : ι →₀ R
h : Eq.{u_4 + 1} (α := M) (f.sum fun (a : ι) (b : R) ↦ b • v a) (g.sum fun (a : ι) (b : R) ↦ b • v a)
h₁ : ∀ (m : ι), Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) m : R) ((g : (a : ι) → R) m : R)
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : LinearIndependent R v
f g : ι →₀ R
h : Eq.{u_4 + 1} (α := M) (f.sum fun (a : ι) (b : R) ↦ b • v a) (g.sum fun (a : ι) (b : R) ↦ b • v a)
m : ι
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) m : R) ((g : (a : ι) → R) m : R)

Tactic:
DFunLike.congr_fun (hv h) m

Premises used: DFunLike.congr_fun
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : LinearIndependent R v
f g : ι →₀ R
h : Eq.{u_4 + 1} (α := M) (f.sum fun (a : ι) (b : R) ↦ b • v a) (g.sum fun (a : ι) (b : R) ↦ b • v a)
m : ι
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) m : R) ((g : (a : ι) → R) m : R)

Tactic:
exact DFunLike.congr_fun (hv h) m

Premises used: DFunLike.congr_fun
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndependent R (-v) ↔ LinearIndependent R v

Tactic:
⟨fun h ↦ ?_, LinearIndependent.neg⟩

Premises used: LinearIndependent.neg, Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
refine : ∀ (h : LinearIndependent R (-v)), LinearIndependent R v
⊢ LinearIndependent R (-v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, LinearIndependent.neg⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : LinearIndependent R (-v)
⊢ LinearIndependent R v

Tactic:
simpa using h.neg

Premises used: LinearIndependent.neg
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndependent R v ↔ Eq (α := Submodule R (ι →₀ R)) (LinearMap.ker (Finsupp.linearCombination R v)) ⊥

Tactic:
LinearMap.ker_eq_bot.symm

Premises used: LinearMap.ker_eq_bot, LinearIndependent, Iff.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndependent R v ↔
    ∀ (l : ι →₀ R), Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0

Tactic:
simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

Premises used: linearIndependent_iff_ker, LinearMap.ker_eq_bot'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0

Tactic:
rw [linearIndependent_iff'ₛ]

Premises used: linearIndependent_iff'ₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0

Tactic:
⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
refine_1 :
  ∀
    (h :
      ∀ (s : Finset ι) (f g : ι → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
    (s : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
refine_2 :
  ∀ (h : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) (s : Finset ι)
    (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
⊢ (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0

Tactic:
refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (0 i) (v i)) →
    ∀ i ∈ s, f i = 0 i

Tactic:
h s f 0

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
a :
  (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (0 i) (v i)) →
      ∀ i ∈ s, f i = 0 i
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0

Tactic:
convert! h s f 0

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
a :
  (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ x ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x)) →
      ∀ i ∈ s, f i = 0
a₁ :
  (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ x ∈ s, 0) → ∀ i ∈ s, f i = 0
⊢ (Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) (0 i) (v i)) →
      ∀ i ∈ s, f i = 0 i

Tactic:
simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]

Premises used: Pi.zero_apply, Finset.sum_const_zero, zero_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
refine_2 : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i

Tactic:
rw [← sub_eq_zero, ← Finset.sum_sub_distrib]

Premises used: sub_eq_zero, Finset.sum_sub_distrib
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, (f - g) i • v i) 0 → ∀ i ∈ s, (f - g) i = 0

Tactic:
h s (f - g)

Premises used: HSub.hSub
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
a :
  (Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, (f - g) i • v i) 0 → ∀ i ∈ s, (f - g) i = 0
⊢ Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i

Tactic:
convert! h s (f - g) using 3

Premises used: HSub.hSub
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ (Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (f x • v x - g x • v x)) 0 → ∀ i ∈ s, f i = g i) ↔
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, (f - g) i • v i) 0 → ∀ i ∈ s, (f - g) i = 0

Tactic:
simp only [Pi.sub_apply, sub_smul, sub_eq_zero]

Premises used: sub_eq_zero, sub_smul, Pi.sub_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
simp_rw simp_rw₁ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (if x ∈ s then g x else 0) • v x) 0
simp_rw₂ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then g x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x)) 0
simp_rw₃ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then g x • v x else 0) 0
simp_rw₄ : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then g j else 0) i) (v i)) 0

Tactic:
simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]

Premises used: zero_smul, Finset.sum_extend_by_zero, ite_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
h : g i = if i ∈ s then g i else 0
⊢ g i = 0

Tactic:
convert!
        H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i

Premises used: Membership.mem, OfNat.ofNat, if_neg, ite
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0

Tactic:
(if_pos hi).symm

Premises used: if_pos, Eq.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0

Tactic:
exact (if_pos hi).symm

Premises used: if_pos, Eq.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0

Tactic:
exact linearIndependent_iff'.trans
    ⟨fun H s g hg hv i => if his : i ∈ s then H s g hv i his else hg i his, fun H s g hg i hi => by
      convert!
        H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i
      exact (if_pos hi).symm⟩

Premises used: linearIndependent_iff', Iff.intro, Iff.trans
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ (i : ι), g i = 0

Tactic:
classical
  exact linearIndependent_iff'.trans
    ⟨fun H s g hg hv i => if his : i ∈ s then H s g hv i his else hg i his, fun H s g hg i hi => by
      convert!
        H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i
      exact (if_pos hi).symm⟩

Premises used: linearIndependent_iff', Iff.intro, Iff.trans
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
c : ι → R
i : ι
h₀ : c i = 0
⊢ LinearIndependent R (v + fun (x : ι) ↦ c x • v i) ↔ LinearIndependent R v

Tactic:
simp [linearIndependent_iff_injective_finsuppLinearCombination,
    ← Finsupp.linearCombination_comp_addSingleEquiv i c h₀]

Premises used: linearIndependent_iff_injective_finsuppLinearCombination, Finsupp.linearCombination_comp_addSingleEquiv
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ ¬LinearIndependent R v ↔
    ∃ (l : ι →₀ R), Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) ∧ l ≠ 0

Tactic:
simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

Premises used: linearIndependent_iff_ker, LinearMap.ker_eq_bot'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ ¬LinearIndependent R v ↔ ∃ (f : ι →₀ R), Eq.{u_4 + 1} (α := M) (f.sum fun (x : ι) (r : R) ↦ r • v x) 0 ∧ f ≠ 0

Tactic:
simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot', Finsupp.linearCombination]

Premises used: linearIndependent_iff_ker, LinearMap.ker_eq_bot', Finsupp.linearCombination
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (¬∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 ∧ ∃ i ∈ s, g i ≠ 0
⊢ ¬LinearIndependent R v ↔ ∃ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
rw [linearIndependent_iff']

Premises used: linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ (¬∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
simp only [exists_prop, not_forall]

Premises used: exists_prop, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
H : LinearIndependent R v
g : ι → R
⊢ Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0

Tactic:
simpa using linearIndependent_iff'.1 H Finset.univ g

Premises used: Finset.univ, linearIndependent_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
H :
  ∀ (H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0) (s : Finset ι) (g : ι → R)
    (hg : ∀ i ∉ s, g i = 0) (hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι),
    Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0
⊢ LinearIndependent R v ↔ ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0

Tactic:
refine
    ⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
      linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
rw : Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) (∑ i ∈ s, g i • v i)
⊢ Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0

Tactic:
rw [← hs]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
⊢ Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) (∑ i ∈ s, g i • v i)

Tactic:
(Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm

Premises used: Finset.sum_subset, Eq.symm, Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
refine : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ∀ (hi : i ∉ s), g i • v i = 0
⊢ Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) (∑ i ∈ s, g i • v i)

Tactic:
refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm

Premises used: Finset.sum_subset, Eq.symm, Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
H : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i_1 i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ s
rw : HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v i) = 0
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ g i • v i = 0

Tactic:
rw [hg i hi, zero_smul]

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
inst_3 : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 ∧ ∃ (i : ι), g i ≠ 0

Tactic:
simpa using not_iff_not.2 Fintype.linearIndependent_iff

Premises used: not_iff_not, Iff.mpr, Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
simp_rw :
  (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) ↔
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
⊢ LinearIndepOn R v (↑s : Set ι) ↔ ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0

Tactic:
simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]

Premises used: Fintype.linearIndependent_iff, LinearIndepOn