K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
⊢ lift (#I) ≤ lift (Module.rank R M)
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
⊢ lift (#{ i // V i ≠ ⊥ }) ≤ lift (Module.rank R M)
set I := { i : ι // V i ≠ ⊥ }
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v, v ∈ V ↑i ∧ v ≠ 0
⊢ lift (#I) ≤ lift (Module.rank R M)
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
⊢ lift (#I) ≤ lift (Module.rank R M)
have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
  intro i
  rw [← Submodule.ne_bot_iff]
  exact i.prop
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
⊢ lift (#I) ≤ lift (Module.rank R M)
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v, v ∈ V ↑i ∧ v ≠ 0
⊢ lift (#I) ≤ lift (Module.rank R M)
choose v hvV hv using hI
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
this : LinearIndependent R v
⊢ lift (#I) ≤ lift (Module.rank R M)
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
⊢ lift (#I) ≤ lift (Module.rank R M)
have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
no goals
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
v : I → M
hvV : ∀ (i : I), v i ∈ V ↑i
hv : ∀ (i : I), v i ≠ 0
this : LinearIndependent R v
⊢ lift (#I) ≤ lift (Module.rank R M)
exact cardinal_lift_le_rank_of_linearIndependent' this
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ ∃ v, v ∈ V ↑i ∧ v ≠ 0
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
⊢ ∀ (i : I), ∃ v, v ∈ V ↑i ∧ v ≠ 0
intro i
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ V ↑i ≠ ⊥
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ ∃ v, v ∈ V ↑i ∧ v ≠ 0
rw [← Submodule.ne_bot_iff]
no goals
K : Type u
V✝ V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.220324
R : Type u
inst✝⁸ : Ring R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type v'
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
M₁ : Type v
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
V : ι → Submodule R M
hV : Independent V
I : Type w := { i // V i ≠ ⊥ }
i : I
⊢ V ↑i ≠ ⊥
exact i.prop