∀ {E : Type u_5} [inst : NormedAddCommGroup E],
  NormedAddCommGroup.toSeminormedAddCommGroup =
    { toNorm := inst.toNorm, toAddCommGroup := inst.toAddCommGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      dist_eq := ⋯ }