∀ {F : Type u_1} {G : Type u_2} [inst : AddGroup F] [inst_1 : AddGroup G] [inst_2 : Fintype F] (f : F →+ G)
  [inst_3 : f.range.Normal] [inst_4 : Fintype (G ⧸ f.range)],
  AddGroup.fintypeOfDomOfCoker f = AddGroup.fintypeOfKerLeRange f (QuotientAddGroup.mk' f.range) ⋯