∀ {R : Type u} {η : Type u₁'} {φ : η → Type u_1} [inst : Semiring R] [StrongRankCondition R]
  [inst_2 : (i : η) → AddCommMonoid (φ i)] [inst_3 : (i : η) → Module R (φ i)] [∀ (i : η), Module.Free R (φ i)]
  [Finite η], Module.rank R ((i : η) → φ i) = Cardinal.sum fun i => Module.rank R (φ i)