∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] (f : M →* P)
  (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  Function.Injective ⇑(f.noncommCoprod g comm) ↔
    Function.Injective ⇑f ∧ Function.Injective ⇑g ∧ Disjoint f.range g.range