∀ {E : Type u_5} [inst : Norm E] [inst_1 : Group E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y),
  NormedGroup.ofMulDist' h₁ h₂ =
    { toNorm := (SeminormedGroup.ofMulDist' h₁ h₂).toNorm, toGroup := (SeminormedGroup.ofMulDist' h₁ h₂).toGroup,
      toPseudoMetricSpace := (SeminormedGroup.ofMulDist' h₁ h₂).toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯,
      dist_eq := ⋯ }