∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : Group E] [inst_2 : NormedGroup F]
  [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f),
  NormedGroup.induced E F f h =
    { toNorm := (SeminormedGroup.induced E F f).toNorm, toGroup := (SeminormedGroup.induced E F f).toGroup,
      toPseudoMetricSpace := (SeminormedGroup.induced E F f).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }