∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group F] [inst_1 : Group G] [inst_2 : Group H]
  [inst_3 : Fintype F] [inst_4 : Fintype H] (f : F →* G) (g : G →* H) (h : g.ker ≤ f.range),
  Group.fintypeOfKerLeRange f g h = Fintype.ofEquiv ((G ⧸ g.ker) × ↥g.ker) Subgroup.groupEquivQuotientProdSubgroup.symm