[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ Module.rank R M < ℵ₀
[PROOFSTEP]
simp only [Module.rank_def]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι < ℵ₀
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber R
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι < ℵ₀
[PROOFSTEP]
obtain ⟨S, hS⟩ := Module.finite_def.mp ‹Module.Finite R M›
[GOAL]
case intro
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
S : Finset M
hS : Submodule.span R ↑S = ⊤
⊢ ⨆ (ι : { s // LinearIndependent R Subtype.val }), #↑↑ι < ℵ₀
[PROOFSTEP]
refine' (ciSup_le' fun i => _).trans_lt (nat_lt_aleph0 S.card)
[GOAL]
case intro
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
S : Finset M
hS : Submodule.span R ↑S = ⊤
i : { s // LinearIndependent R Subtype.val }
⊢ #↑↑i ≤ ↑(Finset.card S)
[PROOFSTEP]
exact linearIndependent_le_span_finset _ i.prop S hS
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁷ : Ring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ ↑(finrank R M) = Module.rank R M
[PROOFSTEP]
rw [finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R M = card (ChooseBasisIndex R M)
[PROOFSTEP]
simp [finrank, rank_eq_card_chooseBasisIndex]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module.Free R M
inst✝⁵ : Module.Finite R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι →₀ R) = card ι
[PROOFSTEP]
rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module.Free R M
inst✝⁵ : Module.Finite R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι → R) = card ι
[PROOFSTEP]
simp [finrank]
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring R
inst✝¹³ : StrongRankCondition R
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R M✝
inst✝¹⁰ : Module.Free R M✝
inst✝⁹ : Module.Finite R M✝
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module.Free R N
inst✝⁵ : Module.Finite R N
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i)
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber R
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring R
inst✝¹³ : StrongRankCondition R
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R M✝
inst✝¹⁰ : Module.Free R M✝
inst✝⁹ : Module.Finite R M✝
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module.Free R N
inst✝⁵ : Module.Finite R N
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i)
[PROOFSTEP]
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_directSum, ← mk_sigma, mk_toNat_eq_card,
  card_sigma]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
⊢ finrank R (M × N) = finrank R M + finrank R N
[PROOFSTEP]
simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R N]
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring R
inst✝¹³ : StrongRankCondition R
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R M✝
inst✝¹⁰ : Module.Free R M✝
inst✝⁹ : Module.Finite R M✝
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module.Free R N
inst✝⁵ : Module.Finite R N
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber R
[GOAL]
R : Type u
M✝ : Type v
N : Type w
inst✝¹⁴ : Ring R
inst✝¹³ : StrongRankCondition R
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : Module R M✝
inst✝¹⁰ : Module.Free R M✝
inst✝⁹ : Module.Finite R M✝
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : Module.Free R N
inst✝⁵ : Module.Finite R N
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Module.Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R ((i : ι) → M i) = ∑ i : ι, finrank R (M i)
[PROOFSTEP]
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma, mk_toNat_eq_card, card_sigma]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹¹ : Ring R
inst✝¹⁰ : StrongRankCondition R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : Module.Free R M
inst✝⁶ : Module.Finite R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ finrank R (Matrix m n R) = card m * card n
[PROOFSTEP]
simp [finrank]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
cond : finrank R M = finrank R N
⊢ Cardinal.lift (Module.rank R M) = Cardinal.lift (Module.rank R N)
[PROOFSTEP]
simp only [← finrank_eq_rank, cond, lift_natCast]
[GOAL]
R : Type u
M✝ : Type v
N✝ : Type w
inst✝¹⁵ : CommRing R
inst✝¹⁴ : StrongRankCondition R
inst✝¹³ : AddCommGroup M✝
inst✝¹² : Module R M✝
inst✝¹¹ : Module.Free R M✝
inst✝¹⁰ : Module.Finite R M✝
inst✝⁹ : AddCommGroup N✝
inst✝⁸ : Module R N✝
inst✝⁷ : Module.Free R N✝
inst✝⁶ : Module.Finite R N✝
M : Type v
N : Type w
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
⊢ finrank R (M ⊗[R] N) = finrank R M * finrank R N
[PROOFSTEP]
simp [finrank]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
s : Submodule R M
⊢ finrank R { x // x ∈ s } ≤ finrank R M
[PROOFSTEP]
simpa only [Cardinal.toNat_lift] using toNat_le_of_le_of_lt_aleph0 (rank_lt_aleph0 _ _) (rank_submodule_le s)
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
s : Submodule R M
⊢ finrank R (M ⧸ s) ≤ finrank R M
[PROOFSTEP]
simpa only [Cardinal.toNat_lift] using
  toNat_le_of_le_of_lt_aleph0 (rank_lt_aleph0 _ _) ((Submodule.mkQ s).rank_le_of_surjective (surjective_quot_mk _))
