K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this : Nontrivial R
⊢ (#ι) ≤ ↑(Fintype.card ↑w)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ (#ι) ≤ ↑(Fintype.card ↑w)
haveI := nontrivial_of_invariantBasisNumber R
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Fintype ι
⊢ (#ι) ≤ ↑(Fintype.card ↑w)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this : Nontrivial R
⊢ (#ι) ≤ ↑(Fintype.card ↑w)
haveI := basisFintypeOfFiniteSpans w s b
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Fintype ι
⊢ ↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Fintype ι
⊢ (#ι) ≤ ↑(Fintype.card ↑w)
rw [Cardinal.mk_fintype ι]
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Fintype ι
⊢ Fintype.card ι ≤ Fintype.card ↑w
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Fintype ι
⊢ ↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)
simp only [Cardinal.natCast_le]
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.307604
R : Type u
inst✝⁴ : Ring R
inst✝³ : RankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Fintype ι
⊢ Fintype.card ι ≤ Fintype.card ↑w
exact Basis.le_span'' b s