∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [Nontrivial R] [inst_3 : Module R M]
  {ι : Type w} (b : Module.Basis ι R M) [Infinite ι] {κ : Type w'} (v : κ → M) (i : LinearIndependent R v),
  i.Maximal → Cardinal.lift.{w', w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, w'} (Cardinal.mk κ)