{α : Type u_5} →
  {P : Sort u} →
    {toNorm : Norm α} →
      {toRing : Ring α} →
        {toMetricSpace : MetricSpace α} →
          {dist_eq : ∀ (x y : α), dist x y = ‖x - y‖} →
            {norm_mul_le : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖} →
              {toNorm' : Norm α} →
                {toRing' : Ring α} →
                  {toMetricSpace' : MetricSpace α} →
                    {dist_eq' : ∀ (x y : α), dist x y = ‖x - y‖} →
                      {norm_mul_le' : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖} →
                        { toNorm := toNorm, toRing := toRing, toMetricSpace := toMetricSpace, dist_eq := dist_eq,
                              norm_mul_le := norm_mul_le } =
                            { toNorm := toNorm', toRing := toRing', toMetricSpace := toMetricSpace',
                              dist_eq := dist_eq', norm_mul_le := norm_mul_le' } →
                          (toNorm ≍ toNorm' → toRing ≍ toRing' → toMetricSpace ≍ toMetricSpace' → P) → P