-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem exists_maximal_linearIndepOn (v : ι → M) :
    ∃ s : Set ι, (LinearIndepOn R v s) ∧ ∀ i ∉ s, ∃ a : R, a ≠ 0 ∧ a • v i ∈ span R (v '' s)

Proof state:
case right.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

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 hIlinind (Finsupp.mem_support_iff.mp hx)

Result:
case right.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hfi : f i ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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
⊢ ¬I = J

Tactic:
intro h2

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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
⊢ False

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
i : ι
hi : i ∉ I
⊢ I ⊆ I ∪ {i}

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hIlinind : ¬f i ≠ 0
⊢ f ∈ Finsupp.supported R R I

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

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hIlinind : ¬f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
⊢ ↑f.support ⊆ I

Proof state:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
set J := I ∪ {i} with hJ

Result:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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}
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Proof state:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : f ∈ Finsupp.supported R R J
sum_f : f i • v i = -∑ x ∈ f.support.erase i, f x • v x
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
c : ι
hc : c ∈ f.support.erase i
⊢ c ∈ I

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

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
⊢ f i ≠ 0

Tactic:
contrapose hIlinind

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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 : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hIlinind : ¬f i ≠ 0
⊢ ¬LinearIndepOn R v I

Proof state:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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}
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]

Result:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
f : ι →₀ R
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
x : ι
hx : x ∈ ↑f.support
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 : ¬f x ≠ 0
supp_f : ↑f.support ⊆ I ∪ {x}
⊢ False

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

Result:
no goals

Proof state:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
have hiJ : i ∈ J := by simp [J]

Result:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : 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
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)