lean: Add missing arguments to rank

[eric-wieser]

Module.rank and finrank expect their first argument to be the ring that our module is over.

The invocations here are complete nonsense, and are talking about equalities between functions on possible (highly non-canonical) ring structures on the provided module.

A proof that this is nonsense can be found in https://github.com/leanprover-community/mathlib4/blob/1a36b1f1a21015cb61e376416b2247e627c1b4ed/Mathlib/tmp.lean#L27-L28, which states:

theorem module_rank_eq_natCast_iff {R : Type u} (n : Nat) :
    Module.rank.{u,max u v} R = n ↔ IsEmpty R ∨ (Subsingleton R ∧ n = 1)

i.e. "if you claim the mispelled-rank is any natural number, you are claiming that the ring is trivial". (Strictly speaking the max u v makes this theorem not apply here, but you would have to truly be desperate to come to that for help)

[ocfnash]

Yikes, this is terrifying. Nice catch.

[GeorgeTsoukalas]

Yikes! Thanks for spotting this.