Theorem: FiniteDimensional.finrank_le_of_span_eq_top (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι
Tactic:
classical
rw [← finrank_top, ← hv]
exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])
State after:
no goals

State before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι
Tactic:
rw [← finrank_top, ← hv]
State after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R ↥(Submodule.span R (Set.range v)) ≤ Fintype.card ι

State before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ finrank R ↥(Submodule.span R (Set.range v)) ≤ Fintype.card ι
Tactic:
exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])
State after:
no goals

State before:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card ≤ Fintype.card ι
Tactic:
convert Fintype.card_range_le v
State after:
case h.e'_3
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card = Fintype.card ↑(Set.range v)

State before:
case h.e'_3
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card = Fintype.card ↑(Set.range v)
Tactic:
rw [Set.toFinset_card]
State after:
no goals