Theorem: Fintype.not_linearIndependent_restrict_iff' (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ ¬LinearIndependent (ι := ↑s) R (s.restrict f) ↔ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, c i ≠ 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
obtain ⟨s,rfl⟩ := s.toFinite.exists_finset_coe
State after:
case intro
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → M
s : Finset ι
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ ↑s, c i ≠ 0) ∧ ∀ i ∉ ↑s, c i = 0

State before:
case intro
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → M
s : Finset ι
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ ↑s, c i ≠ 0) ∧ ∀ i ∉ ↑s, c i = 0
Tactic:
exact Fintype.not_linearIndependent_restrict_iff
State after:
no goals