case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
⊢ ∃ I, (LinearIndependent R fun x => s ↑x) ∧ ∀ (i : ι), ¬i ∈ I → ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
⊢ ∃ I, (LinearIndependent R fun x => s ↑x) ∧ ∀ (i : ι), ¬i ∈ I → ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
rcases exists_maximal_independent' R s with ⟨I, hIlinind, hImaximal⟩
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
⊢ ∀ (i : ι), ¬i ∈ I → ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
⊢ ∃ I, (LinearIndependent R fun x => s ↑x) ∧ ∀ (i : ι), ¬i ∈ I → ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
use I, hIlinind
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
i : ι
hi : ¬i ∈ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
⊢ ∀ (i : ι), ¬i ∈ I → ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
intro i hi
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
hImaximal : (LinearIndependent R fun x => s ↑x) → I = I ∪ {i}
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
i : ι
hi : ¬i ∈ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
specialize hImaximal (I ∪ {i}) (by simp)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
hImaximal : (LinearIndependent R fun x => s ↑x) → I = I ∪ {i}
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
set J := I ∪ {i} with hJ
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
have hiJ : i ∈ J := by simp
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDependent_comp_subtype.mp h
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
have hfi : f i ≠ 0 := by
  contrapose hIlinind
  refine' linearDependent_comp_subtype.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)
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
⊢ ↑f i • s i ∈ span R (s '' I)
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
use f i, hfi
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
⊢ ↑f i • s i ∈ span R (s '' I)
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
⊢ ↑f i • s i ∈ span R (s '' I)
have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ↑f i • s i = -∑ x in Finset.erase f.support i, ↑f x • s x
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
⊢ ↑f i • s i ∈ span R (s '' I)
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
⊢ ↑f i • s i ∈ span R (s '' I)
rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.not_mem_erase _ _),
  add_eq_zero_iff_eq_neg] at sum_f
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ↑f i • s i = -∑ x in Finset.erase f.support i, ↑f x • s x
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
⊢ -∑ x in Finset.erase f.support i, ↑f x • s x ∈ span R (s '' I)
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ↑f i • s i = -∑ x in Finset.erase f.support i, ↑f x • s x
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
⊢ ↑f i • s i ∈ span R (s '' I)
rw [sum_f]
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ↑f i • s i = -∑ x in Finset.erase f.support i, ↑f x • s x
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
c : ι
hc : c ∈ Finset.erase f.support i
⊢ c ∈ I
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ↑f i • s i = -∑ x in Finset.erase f.support i, ↑f x • s x
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
⊢ -∑ x in Finset.erase f.support i, ↑f x • s x ∈ span R (s '' I)
refine' neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, _, rfl⟩))
no goals
case intro.intro.intro.intro.intro
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ↑f i • s i = -∑ x in Finset.erase f.support i, ↑f x • s x
f_ne : f ≠ 0
hfi : ↑f i ≠ 0
hfi' : i ∈ f.support
c : ι
hc : c ∈ Finset.erase f.support i
⊢ c ∈ I
exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)
no goals
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
hImaximal : ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun x => s ↑x) → I = J
i : ι
hi : ¬i ∈ I
⊢ I ⊆ I ∪ {i}
simp
no goals
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
⊢ ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
simp [hJ]
no goals
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
⊢ i ∈ J
simp
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬I = J
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ?m.518334
refine mt hImaximal ?_
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬I = J
intro h2
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
J : Set ι := I ∪ {i}
hi : ¬i ∈ J
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False
rw [h2] at hi
no goals
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
J : Set ι := I ∪ {i}
hi : ¬i ∈ J
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h2 : I = J
⊢ False
exact absurd hiJ hi
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
⊢ ¬LinearIndependent R fun x => s ↑x
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
hIlinind : LinearIndependent R fun x => s ↑x
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
⊢ ↑f i ≠ 0
contrapose hIlinind
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
⊢ f ∈ Finsupp.supported R R I
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
⊢ ¬LinearIndependent R fun x => s ↑x
refine' linearDependent_comp_subtype.mpr ⟨f, _, sum_f, f_ne⟩
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
⊢ ↑f.support ⊆ I
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
⊢ f ∈ Finsupp.supported R R I
simp only [Finsupp.mem_supported, hJ] at supp_f⊢
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
x : ι
hx : x ∈ ↑f.support
⊢ x ∈ I
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
⊢ ↑f.support ⊆ I
rintro x hx
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
x : ι
hx : x ∈ ↑f.support
⊢ ¬x = i
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
x : ι
hx : x ∈ ↑f.support
⊢ x ∈ I
refine' (memJ.mp (supp_f hx)).resolve_left _
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
x : ι
hx : x ∈ ↑f.support
hi : ¬x ∈ I
J : Set ι := I ∪ {x}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {x}
memJ : ∀ {x_1 : ι}, x_1 ∈ J ↔ x_1 = x ∨ x_1 ∈ I
hiJ : x ∈ J
h : ¬LinearIndependent R fun x => s ↑x
hIlinind : ¬↑f x ≠ 0
supp_f : ↑f.support ⊆ I ∪ {x}
⊢ False
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
i : ι
hi : ¬i ∈ I
J : Set ι := I ∪ {i}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndependent R fun x => s ↑x
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
hIlinind : ¬↑f i ≠ 0
supp_f : ↑f.support ⊆ I ∪ {i}
x : ι
hx : x ∈ ↑f.support
⊢ ¬x = i
rintro rfl
no goals
ι : Type u'
ι' : Type ?u.511300
R : Type u_1
K : Type ?u.511306
M : Type u_2
M' : Type ?u.511312
M'' : Type ?u.511315
V : Type u
V' : Type ?u.511320
v : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
hv : LinearIndependent R v
s : ι → M
I : Set ι
f : ι →₀ R
sum_f : ∑ i in f.support, ↑f i • s i = 0
f_ne : f ≠ 0
x : ι
hx : x ∈ ↑f.support
hi : ¬x ∈ I
J : Set ι := I ∪ {x}
hImaximal : (LinearIndependent R fun x => s ↑x) → I = J
hJ : J = I ∪ {x}
memJ : ∀ {x_1 : ι}, x_1 ∈ J ↔ x_1 = x ∨ x_1 ∈ I
hiJ : x ∈ J
h : ¬LinearIndependent R fun x => s ↑x
hIlinind : ¬↑f x ≠ 0
supp_f : ↑f.support ⊆ I ∪ {x}
⊢ False
exact hIlinind (Finsupp.mem_support_iff.mp hx)