ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
⊢ (∀ (l : ι →₀ R), ↑l default = 0 ∨ v default = 0 → l = 0) ↔ v default ≠ 0
ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
⊢ LinearIndependent R v ↔ v default ≠ 0
simp only [linearIndependent_iff, Finsupp.total_unique, smul_eq_zero]
ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), ↑l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
⊢ False
ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
⊢ (∀ (l : ι →₀ R), ↑l default = 0 ∨ v default = 0 → l = 0) ↔ v default ≠ 0
refine' ⟨fun h hv => _, fun hv l hl => Finsupp.unique_ext <| hl.resolve_right hv⟩
ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), ↑l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
this : Finsupp.single default 1 = 0
⊢ False
ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), ↑l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
⊢ False
have := h (Finsupp.single default 1) (Or.inr hv)
no goals
ι : Type u'
ι' : Type ?u.1178902
R : Type u_1
K : Type ?u.1178908
M : Type u_2
M' : Type ?u.1178914
M'' : Type ?u.1178917
V : Type u
V' : Type ?u.1178922
inst✝⁷ : Ring R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module R M'
v✝ : ι → M
s t : Set M
x y z : M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), ↑l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
this : Finsupp.single default 1 = 0
⊢ False
exact one_ne_zero (Finsupp.single_eq_zero.1 this)