{K : semiOutParam (Type u_1)} →
  {P : Sort u} →
    {toDenselyNormedField : DenselyNormedField K} →
      {toStarRing : StarRing K} →
        {toNormedAlgebra : NormedAlgebra ℝ K} →
          {toCompleteSpace : CompleteSpace K} →
            {re im : K →+ ℝ} →
              {I : K} →
                {I_re_ax : re I = 0} →
                  {I_mul_I_ax : I = 0 ∨ I * I = -1} →
                    {re_add_im_ax : ∀ (z : K), (algebraMap ℝ K) (re z) + (algebraMap ℝ K) (im z) * I = z} →
                      {ofReal_re_ax : ∀ (r : ℝ), re ((algebraMap ℝ K) r) = r} →
                        {ofReal_im_ax : ∀ (r : ℝ), im ((algebraMap ℝ K) r) = 0} →
                          {mul_re_ax : ∀ (z w : K), re (z * w) = re z * re w - im z * im w} →
                            {mul_im_ax : ∀ (z w : K), im (z * w) = re z * im w + im z * re w} →
                              {conj_re_ax : ∀ (z : K), re ((starRingEnd K) z) = re z} →
                                {conj_im_ax : ∀ (z : K), im ((starRingEnd K) z) = -im z} →
                                  {conj_I_ax : (starRingEnd K) I = -I} →
                                    {norm_sq_eq_def_ax : ∀ (z : K), ‖z‖ ^ 2 = re z * re z + im z * im z} →
                                      {mul_im_I_ax : ∀ (z : K), im z * im I = im z} →
                                        {toPartialOrder : PartialOrder K} →
                                          {le_iff_re_im : ∀ {z w : K}, z ≤ w ↔ re z ≤ re w ∧ im z = im w} →
                                            {toDecidableEq : DecidableEq K} →
                                              {toDenselyNormedField' : DenselyNormedField K} →
                                                {toStarRing' : StarRing K} →
                                                  {toNormedAlgebra' : NormedAlgebra ℝ K} →
                                                    {toCompleteSpace' : CompleteSpace K} →
                                                      {re' im' : K →+ ℝ} →
                                                        {I' : K} →
                                                          {I_re_ax' : re' I' = 0} →
                                                            {I_mul_I_ax' : I' = 0 ∨ I' * I' = -1} →
                                                              {re_add_im_ax' :
                                                                  ∀ (z : K),
                                                                    (algebraMap ℝ K) (re' z) +
                                                                        (algebraMap ℝ K) (im' z) * I' =
                                                                      z} →
                                                                {ofReal_re_ax' :
                                                                    ∀ (r : ℝ), re' ((algebraMap ℝ K) r) = r} →
                                                                  {ofReal_im_ax' :
                                                                      ∀ (r : ℝ), im' ((algebraMap ℝ K) r) = 0} →
                                                                    {mul_re_ax' :
                                                                        ∀ (z w : K),
                                                                          re' (z * w) = re' z * re' w - im' z * im' w} →
                                                                      {mul_im_ax' :
                                                                          ∀ (z w : K),
                                                                            im' (z * w) =
                                                                              re' z * im' w + im' z * re' w} →
                                                                        {conj_re_ax' :
                                                                            ∀ (z : K),
                                                                              re' ((starRingEnd K) z) = re' z} →
                                                                          {conj_im_ax' :
                                                                              ∀ (z : K),
                                                                                im' ((starRingEnd K) z) = -im' z} →
                                                                            {conj_I_ax' : (starRingEnd K) I' = -I'} →
                                                                              {norm_sq_eq_def_ax' :
                                                                                  ∀ (z : K),
                                                                                    ‖z‖ ^ 2 =
                                                                                      re' z * re' z + im' z * im' z} →
                                                                                {mul_im_I_ax' :
                                                                                    ∀ (z : K), im' z * im' I' = im' z} →
                                                                                  {toPartialOrder' : PartialOrder K} →
                                                                                    {le_iff_re_im' :
                                                                                        ∀ {z w : K},
                                                                                          z ≤ w ↔
                                                                                            re' z ≤ re' w ∧
                                                                                              im' z = im' w} →
                                                                                      {toDecidableEq' : DecidableEq K} →
                                                                                        {
                                                                                              toDenselyNormedField :=
                                                                                                toDenselyNormedField,
                                                                                              toStarRing := toStarRing,
                                                                                              toNormedAlgebra :=
                                                                                                toNormedAlgebra,
                                                                                              toCompleteSpace :=
                                                                                                toCompleteSpace,
                                                                                              re := re, im := im,
                                                                                              I := I,
                                                                                              I_re_ax := I_re_ax,
                                                                                              I_mul_I_ax := I_mul_I_ax,
                                                                                              re_add_im_ax :=
                                                                                                re_add_im_ax,
                                                                                              ofReal_re_ax :=
                                                                                                ofReal_re_ax,
                                                                                              ofReal_im_ax :=
                                                                                                ofReal_im_ax,
                                                                                              mul_re_ax := mul_re_ax,
                                                                                              mul_im_ax := mul_im_ax,
                                                                                              conj_re_ax := conj_re_ax,
                                                                                              conj_im_ax := conj_im_ax,
                                                                                              conj_I_ax := conj_I_ax,
                                                                                              norm_sq_eq_def_ax :=
                                                                                                norm_sq_eq_def_ax,
                                                                                              mul_im_I_ax :=
                                                                                                mul_im_I_ax,
                                                                                              toPartialOrder :=
                                                                                                toPartialOrder,
                                                                                              le_iff_re_im :=
                                                                                                le_iff_re_im,
                                                                                              toDecidableEq :=
                                                                                                toDecidableEq } =
                                                                                            {
                                                                                              toDenselyNormedField :=
                                                                                                toDenselyNormedField',
                                                                                              toStarRing := toStarRing',
                                                                                              toNormedAlgebra :=
                                                                                                toNormedAlgebra',
                                                                                              toCompleteSpace :=
                                                                                                toCompleteSpace',
                                                                                              re := re', im := im',
                                                                                              I := I',
                                                                                              I_re_ax := I_re_ax',
                                                                                              I_mul_I_ax := I_mul_I_ax',
                                                                                              re_add_im_ax :=
                                                                                                re_add_im_ax',
                                                                                              ofReal_re_ax :=
                                                                                                ofReal_re_ax',
                                                                                              ofReal_im_ax :=
                                                                                                ofReal_im_ax',
                                                                                              mul_re_ax := mul_re_ax',
                                                                                              mul_im_ax := mul_im_ax',
                                                                                              conj_re_ax := conj_re_ax',
                                                                                              conj_im_ax := conj_im_ax',
                                                                                              conj_I_ax := conj_I_ax',
                                                                                              norm_sq_eq_def_ax :=
                                                                                                norm_sq_eq_def_ax',
                                                                                              mul_im_I_ax :=
                                                                                                mul_im_I_ax',
                                                                                              toPartialOrder :=
                                                                                                toPartialOrder',
                                                                                              le_iff_re_im :=
                                                                                                le_iff_re_im',
                                                                                              toDecidableEq :=
                                                                                                toDecidableEq' } →
                                                                                          (toDenselyNormedField ≍
                                                                                                toDenselyNormedField' →
                                                                                              toStarRing ≍ toStarRing' →
                                                                                                toNormedAlgebra ≍
                                                                                                    toNormedAlgebra' →
                                                                                                  re ≍ re' →
                                                                                                    ⋯ →
                                                                                                      I ≍ I' →
                                                                                                        toPartialOrder ≍
                                                                                                            toPartialOrder' →
                                                                                                          toDecidableEq ≍
                                                                                                              toDecidableEq' →
                                                                                                            P) →
                                                                                            P