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.413475
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
⊢ Nonempty (Fintype ι)
rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
  Cardinal.lt_aleph0_iff_fintype] at h