awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬LinearIndepOn R v J

Tactic:
mt hImaximal ?_

Premises used: mt
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
refine : ¬I = J
⊢ ¬LinearIndepOn R v J

Tactic:
refine mt hImaximal ?_

Premises used: mt
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ i ∉ J

Tactic:
rw [h2] at hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
hi₁ : i ∉ J
⊢ LinearIndepOn R v J → I = J

Tactic:
rw [h2] at hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
hi₁ : i ∉ J
hImaximal₁ : LinearIndepOn R v J → I = J
⊢ J = I ∪ {i}

Tactic:
rw [h2] at hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
hi₁ : i ∉ J
hImaximal₁ : LinearIndepOn R v J → I = J
hJ₁ : J = I ∪ {i}
⊢ ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I

Tactic:
rw [h2] at hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
hi₁ : i ∉ J
hImaximal₁ : LinearIndepOn R v J → I = J
hJ₁ : J = I ∪ {i}
memJ₁ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
⊢ i ∈ J

Tactic:
rw [h2] at hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
hi₁ : i ∉ J
hImaximal₁ : LinearIndepOn R v J → I = J
hJ₁ : J = I ∪ {i}
memJ₁ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ₁ : i ∈ J
⊢ I = J

Tactic:
rw [h2] at hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
J : Set ι := I ∪ {i}
hi : i ∉ J
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False

Tactic:
absurd hiJ hi

Premises used: absurd
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
J : Set ι := I ∪ {i}
hi : i ∉ J
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False

Tactic:
exact absurd hiJ hi

Premises used: absurd
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬LinearIndepOn R v J

Tactic:
have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
right :
  ∀ (f : ι →₀ R) (supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f)
    (sum_f :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0)
    (f_ne : f ≠ 0), ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)

Tactic:
obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h

Premises used: linearDepOn_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
contrapose : ∀ (hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)), ¬LinearIndepOn R v I
⊢ Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)

Tactic:
contrapose hIlinind
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ ¬LinearIndepOn R v I

Tactic:
linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩

Premises used: Iff.mpr, linearDepOn_iff, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
refine : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R I) f
⊢ ¬LinearIndepOn R v I

Tactic:
refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩

Premises used: Iff.mpr, linearDepOn_iff, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ (↑f.support : Set ι) ⊆ I ∪ {i}

Tactic:
simp only [Finsupp.mem_supported, hJ] at supp_f ⊢

Premises used: Finsupp.mem_supported
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
supp_f : (↑f.support : Set ι) ⊆ I ∪ {i}
x : ι
hx : x ∈ (↑f.support : Set ι)
⊢ x ∈ I

Tactic:
(memJ.mp (supp_f hx)).resolve_left ?_

Premises used: Or.resolve_left, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
supp_f : (↑f.support : Set ι) ⊆ I ∪ {i}
x : ι
hx : x ∈ (↑f.support : Set ι)
refine : ¬x = i
⊢ x ∈ I

Tactic:
refine (memJ.mp (supp_f hx)).resolve_left ?_

Premises used: Or.resolve_left, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
f : ι →₀ R
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
x : ι
hx : x ∈ (↑f.support : Set ι)
hi : x ∉ I
J : Set ι := I ∪ {x}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {x}
memJ : ∀ {x_1 : ι}, x_1 ∈ J ↔ x_1 = x ∨ x_1 ∈ I
hiJ : x ∈ J
h : ¬LinearIndepOn R v J
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R)
supp_f : (↑f.support : Set ι) ⊆ I ∪ {x}
⊢ False

Tactic:
(Finsupp.mem_support_iff.mp hx) hIlinind

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
f : ι →₀ R
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
x : ι
hx : x ∈ (↑f.support : Set ι)
hi : x ∉ I
J : Set ι := I ∪ {x}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {x}
memJ : ∀ {x_1 : ι}, x_1 ∈ J ↔ x_1 = x ∨ x_1 ∈ I
hiJ : x ∈ J
h : ¬LinearIndepOn R v J
hIlinind : Eq.{u_2 + 1} (α := R) ((f : (a : ι) → R) x : R) (0 : R)
supp_f : (↑f.support : Set ι) ⊆ I ∪ {x}
⊢ False

Tactic:
exact (Finsupp.mem_support_iff.mp hx) hIlinind

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
⊢ Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)

Tactic:
have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
right :
  Membership.mem (γ := Submodule R M) (span R (v '' I))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
⊢ ∃ (a : R), a ≠ 0 ∧ Membership.mem (γ := Submodule R M) (span R (v '' I)) (a • v i)

Tactic:
use f i, hfi

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ i ∈ f.support

Tactic:
have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)

Tactic:
rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f

Premises used: add_eq_zero_iff_eq_neg, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
sum_f₁ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
⊢ f ≠ 0

Tactic:
rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f

Premises used: add_eq_zero_iff_eq_neg, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
sum_f₁ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne₁ : f ≠ 0
⊢ Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)

Tactic:
rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f

Premises used: add_eq_zero_iff_eq_neg, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f : Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i)) 0
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
sum_f₁ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne₁ : f ≠ 0
hfi₁ : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
⊢ i ∈ f.support

Tactic:
rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f

Premises used: add_eq_zero_iff_eq_neg, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
right :
  Membership.mem (γ := Submodule R M) (span R (v '' I))
    (-∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))

Tactic:
rw [sum_f]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (-∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x))

Tactic:
neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))

Premises used: And.intro, Exists.intro, Submodule.span, Set.image, Submodule.subset_span, DFunLike.coe, sum_mem, rfl, Submodule.smul_mem, NegMemClass.neg_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
right : ∀ (c : ι) (hc : c ∈ f.support.erase i), c ∈ I
⊢ Membership.mem (γ := Submodule R M) (span R (v '' I))
    (-∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x))

Tactic:
refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
c : ι
hc : c ∈ f.support.erase i
⊢ c ∈ I

Tactic:
(memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)

Premises used: Finset.ne_of_mem_erase, Or.resolve_left, Iff.mp, Finset.erase_subset