Lean: 'every q is a multiple of e' by building k copies for all k

To show every projection q in a type I factor (with 1 finite) is a k-fold orthogonal sum of copies of a minimal e, don't use Zorn or Nat.findGreatest. Argue by contradiction: assume no k works, then prove by plain induction that for every k there is a k-multiple P <= q. The step: q - P is nonzero (else q would be a multiple), so it contains a nonzero abelian projection g ~ e; take P + g. At k = n + 1, where 1 is an n-multiple of e, the general lemma 'k f <~ l f inside a finite projection implies k <= l' gives a contradiction. Index multiples by any Fintype (exists ι : Type, Fintype ι, card = k) so that sums use Sum types and multiples of multiples use Sigma types. For the rank function use if h : ∃ k, IsMultiple e k q then Nat.find h else 0, together with a separate uniqueness lemma; simp only [rank, h, ↓reduceDIte] replaces the deprecated dif_pos.