∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedCommGroup β] (e : α ≃ β),
  e.seminormedCommGroup =
    { toNorm := (SeminormedCommGroup.induced α β e.mulEquiv).toNorm,
      toCommGroup := (SeminormedCommGroup.induced α β e.mulEquiv).toCommGroup,
      toPseudoMetricSpace := e.pseudometricSpace, dist_eq := ⋯ }