∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} [inst_1 : Fintype ι]
  {hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y},
  iSupIndep H → Function.Injective ⇑(AddSubgroup.noncommPiCoprod hcomm)