{α : Type u_5} →
  (norm : α → ℝ) →
    (add : α → α → α) →
      (∀ (a b c : α), a + b + c = a + (b + c)) →
        (zero : α) →
          (∀ (a : α), 0 + a = a) →
            (∀ (a : α), a + 0 = a) →
              (nsmul : ℕ → α → α) →
                autoParam (∀ (x : α), nsmul 0 x = 0) AddMonoid.nsmul_zero._autoParam →
                  autoParam (∀ (n : ℕ) (x : α), nsmul (n + 1) x = nsmul n x + x) AddMonoid.nsmul_succ._autoParam →
                    (∀ (a b : α), a + b = b + a) →
                      (mul : α → α → α) →
                        (∀ (a b c : α), a * (b + c) = a * b + a * c) →
                          (∀ (a b c : α), (a + b) * c = a * c + b * c) →
                            (∀ (a : α), 0 * a = 0) →
                              (∀ (a : α), a * 0 = 0) →
                                (∀ (a b c : α), a * b * c = a * (b * c)) →
                                  (one : α) →
                                    (∀ (a : α), 1 * a = a) →
                                      (∀ (a : α), a * 1 = a) →
                                        (natCast : ℕ → α) →
                                          autoParam (natCast 0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
                                            autoParam (∀ (n : ℕ), natCast (n + 1) = natCast n + 1)
                                                AddMonoidWithOne.natCast_succ._autoParam →
                                              (npow : ℕ → α → α) →
                                                autoParam (∀ (x : α), npow 0 x = 1) Monoid.npow_zero._autoParam →
                                                  autoParam (∀ (n : ℕ) (x : α), npow (n + 1) x = npow n x * x)
                                                      Monoid.npow_succ._autoParam →
                                                    (neg : α → α) →
                                                      (sub : α → α → α) →
                                                        autoParam (∀ (a b : α), a - b = a + neg b)
                                                            SubNegMonoid.sub_eq_add_neg._autoParam →
                                                          (zsmul : ℤ → α → α) →
                                                            autoParam (∀ (a : α), zsmul 0 a = 0)
                                                                SubNegMonoid.zsmul_zero'._autoParam →
                                                              autoParam
                                                                  (∀ (n : ℕ) (a : α),
                                                                    zsmul (↑n.succ) a = zsmul (↑n) a + a)
                                                                  SubNegMonoid.zsmul_succ'._autoParam →
                                                                autoParam
                                                                    (∀ (n : ℕ) (a : α),
                                                                      zsmul (Int.negSucc n) a = neg (zsmul (↑n.succ) a))
                                                                    SubNegMonoid.zsmul_neg'._autoParam →
                                                                  (∀ (a : α), neg a + a = 0) →
                                                                    (intCast : ℤ → α) →
                                                                      autoParam (∀ (n : ℕ), intCast ↑n = ↑n)
                                                                          AddGroupWithOne.intCast_ofNat._autoParam →
                                                                        autoParam
                                                                            (∀ (n : ℕ),
                                                                              intCast (Int.negSucc n) = neg ↑(n + 1))
                                                                            AddGroupWithOne.intCast_negSucc._autoParam →
                                                                          (dist : α → α → ℝ) →
                                                                            (∀ (x : α), dist x x = 0) →
                                                                              (∀ (x y : α), dist x y = dist y x) →
                                                                                (∀ (x y z : α),
                                                                                    dist x z ≤ dist x y + dist y z) →
                                                                                  (edist : α → α → ENNReal) →
                                                                                    autoParam
                                                                                        (∀ (x y : α),
                                                                                          edist x y =
                                                                                            ENNReal.ofReal (dist x y))
                                                                                        PseudoMetricSpace.edist_dist._autoParam →
                                                                                      (toUniformSpace :
                                                                                          UniformSpace α) →
                                                                                        autoParam
                                                                                            (uniformity α =
                                                                                              ⨅ ε,
                                                                                                ⨅ (_ : ε > 0),
                                                                                                  Filter.principal
                                                                                                    {p |
                                                                                                      dist p.1 p.2 < ε})
                                                                                            PseudoMetricSpace.uniformity_dist._autoParam →
                                                                                          (toBornology : Bornology α) →
                                                                                            autoParam
                                                                                                ((Bornology.cobounded
                                                                                                      α).sets =
                                                                                                  {s | ⋯})
                                                                                                PseudoMetricSpace.cobounded_sets._autoParam →
                                                                                              (∀ {x y : α},
                                                                                                  dist x y = 0 →
                                                                                                    x = y) →
                                                                                                (∀ (x y : α),
                                                                                                    dist x y =
                                                                                                      norm
                                                                                                        (neg x + y)) →
                                                                                                  (∀ (a b : α),
                                                                                                      norm (a * b) ≤
                                                                                                        norm a *
                                                                                                          norm b) →
                                                                                                    NormedRing α