[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (x y : ℍ[DualNumber R]),
    Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        (x * y) =
      Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          x *
        Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          y
[PROOFSTEP]
rintro ⟨⟨xr, xrε⟩, ⟨xi, xiε⟩, ⟨xj, xjε⟩, ⟨xk, xkε⟩⟩
[GOAL]
case mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε : R
⊢ ∀ (y : ℍ[DualNumber R]),
    Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } * y) =
      Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          { re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
        Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          y
[PROOFSTEP]
rintro ⟨⟨yr, yrε⟩, ⟨yi, yiε⟩, ⟨yj, yjε⟩, ⟨yk, ykε⟩⟩
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ Equiv.toFun
      {
        toFun := fun q =>
          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
              imK := TrivSqZeroExt.fst q.imK },
            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
              imK := TrivSqZeroExt.snd q.imK }),
        invFun := fun d =>
          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
        left_inv :=
          (_ :
            ∀ (x : ℍ[DualNumber R]),
              (fun d =>
                    { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                      imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                      imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                      imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                  ((fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DualNumber ℍ[R]),
              (fun q =>
                    ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                        imK := TrivSqZeroExt.fst q.imK },
                      { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                        imK := TrivSqZeroExt.snd q.imK }))
                  ((fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    x) =
                x) }
      ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
        { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }) =
    Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        { re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
      Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }
[PROOFSTEP]
ext : 1
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h1
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ TrivSqZeroExt.fst
      (Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) })) =
    TrivSqZeroExt.fst
      (Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          { re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
        Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) })
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ TrivSqZeroExt.snd
      (Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) })) =
    TrivSqZeroExt.snd
      (Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          { re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
        Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) })
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ {
      re :=
        TrivSqZeroExt.snd
          ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
              { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).re,
      imI :=
        TrivSqZeroExt.snd
          ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
              { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).imI,
      imJ :=
        TrivSqZeroExt.snd
          ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
              { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).imJ,
      imK :=
        TrivSqZeroExt.snd
          ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
              { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).imK } =
    { re := xr, imI := xi, imJ := xj, imK := xk } * { re := yrε, imI := yiε, imJ := yjε, imK := ykε } +
      { re := xrε, imI := xiε, imJ := xjε, imK := xkε } * { re := yr, imI := yi, imJ := yj, imK := yk }
[PROOFSTEP]
congr 1
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_re
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ TrivSqZeroExt.snd
      ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).re =
    ({ re := xr, imI := xi, imJ := xj, imK := xk } * { re := yrε, imI := yiε, imJ := yjε, imK := ykε }).re +
      ({ re := xrε, imI := xiε, imJ := xjε, imK := xkε } * { re := yr, imI := yi, imJ := yj, imK := yk }).re
[PROOFSTEP]
simp
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_imI
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ TrivSqZeroExt.snd
      ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).imI =
    ({ re := xr, imI := xi, imJ := xj, imK := xk } * { re := yrε, imI := yiε, imJ := yjε, imK := ykε }).imI +
      ({ re := xrε, imI := xiε, imJ := xjε, imK := xkε } * { re := yr, imI := yi, imJ := yj, imK := yk }).imI
[PROOFSTEP]
simp
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_imJ
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ TrivSqZeroExt.snd
      ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).imJ =
    ({ re := xr, imI := xi, imJ := xj, imK := xk } * { re := yrε, imI := yiε, imJ := yjε, imK := ykε }).imJ +
      ({ re := xrε, imI := xiε, imJ := xjε, imK := xkε } * { re := yr, imI := yi, imJ := yj, imK := yk }).imJ
[PROOFSTEP]
simp
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_imK
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ TrivSqZeroExt.snd
      ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } *
          { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }).imK =
    ({ re := xr, imI := xi, imJ := xj, imK := xk } * { re := yrε, imI := yiε, imJ := yjε, imK := ykε }).imK +
      ({ re := xrε, imI := xiε, imJ := xjε, imK := xkε } * { re := yr, imI := yi, imJ := yj, imK := yk }).imK
[PROOFSTEP]
simp
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_re
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ xr * yrε + xrε * yr - (xi * yiε + xiε * yi) - (xj * yjε + xjε * yj) - (xk * ykε + xkε * yk) =
    xr * yrε - xi * yiε - xj * yjε - xk * ykε + (xrε * yr - xiε * yi - xjε * yj - xkε * yk)
[PROOFSTEP]
ring
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_imI
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ xr * yiε + xrε * yi + (xi * yrε + xiε * yr) + (xj * ykε + xjε * yk) - (xk * yjε + xkε * yj) =
    xr * yiε + xi * yrε + xj * ykε - xk * yjε + (xrε * yi + xiε * yr + xjε * yk - xkε * yj)
[PROOFSTEP]
ring
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_imJ
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ xr * yjε + xrε * yj - (xi * ykε + xiε * yk) + (xj * yrε + xjε * yr) + (xk * yiε + xkε * yi) =
    xr * yjε - xi * ykε + xj * yrε + xk * yiε + (xrε * yj - xiε * yk + xjε * yr + xkε * yi)
[PROOFSTEP]
ring
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk.h2.e_imK
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ xr * ykε + xrε * yk + (xi * yjε + xiε * yj) - (xj * yiε + xjε * yi) + (xk * yrε + xkε * yr) =
    xr * ykε + xi * yjε - xj * yiε + xk * yrε + (xrε * yk + xiε * yj - xjε * yi + xkε * yr)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (x y : ℍ[DualNumber R]),
    Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        (x + y) =
      Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          x +
        Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          y
[PROOFSTEP]
rintro ⟨⟨xr, xrε⟩, ⟨xi, xiε⟩, ⟨xj, xjε⟩, ⟨xk, xkε⟩⟩
[GOAL]
case mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε : R
⊢ ∀ (y : ℍ[DualNumber R]),
    Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } + y) =
      Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          { re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } +
        Equiv.toFun
          {
            toFun := fun q =>
              ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                  imK := TrivSqZeroExt.fst q.imK },
                { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                  imK := TrivSqZeroExt.snd q.imK }),
            invFun := fun d =>
              { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
            left_inv :=
              (_ :
                ∀ (x : ℍ[DualNumber R]),
                  (fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      ((fun q =>
                          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI,
                              imJ := TrivSqZeroExt.fst q.imJ, imK := TrivSqZeroExt.fst q.imK },
                            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                              imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DualNumber ℍ[R]),
                  (fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      ((fun d =>
                          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                        x) =
                    x) }
          y
[PROOFSTEP]
rintro ⟨⟨yr, yrε⟩, ⟨yi, yiε⟩, ⟨yj, yjε⟩, ⟨yk, ykε⟩⟩
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommRing R
xr xrε xi xiε xj xjε xk xkε yr yrε yi yiε yj yjε yk ykε : R
⊢ Equiv.toFun
      {
        toFun := fun q =>
          ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
              imK := TrivSqZeroExt.fst q.imK },
            { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
              imK := TrivSqZeroExt.snd q.imK }),
        invFun := fun d =>
          { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
            imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
            imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
            imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
        left_inv :=
          (_ :
            ∀ (x : ℍ[DualNumber R]),
              (fun d =>
                    { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                      imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                      imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                      imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                  ((fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DualNumber ℍ[R]),
              (fun q =>
                    ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                        imK := TrivSqZeroExt.fst q.imK },
                      { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                        imK := TrivSqZeroExt.snd q.imK }))
                  ((fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    x) =
                x) }
      ({ re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } +
        { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }) =
    Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        { re := (xr, xrε), imI := (xi, xiε), imJ := (xj, xjε), imK := (xk, xkε) } +
      Equiv.toFun
        {
          toFun := fun q =>
            ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                imK := TrivSqZeroExt.fst q.imK },
              { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                imK := TrivSqZeroExt.snd q.imK }),
          invFun := fun d =>
            { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
              imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
              imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
              imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) },
          left_inv :=
            (_ :
              ∀ (x : ℍ[DualNumber R]),
                (fun d =>
                      { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                        imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                        imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                        imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                    ((fun q =>
                        ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                            imK := TrivSqZeroExt.fst q.imK },
                          { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI,
                            imJ := TrivSqZeroExt.snd q.imJ, imK := TrivSqZeroExt.snd q.imK }))
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DualNumber ℍ[R]),
                (fun q =>
                      ({ re := TrivSqZeroExt.fst q.re, imI := TrivSqZeroExt.fst q.imI, imJ := TrivSqZeroExt.fst q.imJ,
                          imK := TrivSqZeroExt.fst q.imK },
                        { re := TrivSqZeroExt.snd q.re, imI := TrivSqZeroExt.snd q.imI, imJ := TrivSqZeroExt.snd q.imJ,
                          imK := TrivSqZeroExt.snd q.imK }))
                    ((fun d =>
                        { re := ((TrivSqZeroExt.fst d).re, (TrivSqZeroExt.snd d).re),
                          imI := ((TrivSqZeroExt.fst d).imI, (TrivSqZeroExt.snd d).imI),
                          imJ := ((TrivSqZeroExt.fst d).imJ, (TrivSqZeroExt.snd d).imJ),
                          imK := ((TrivSqZeroExt.fst d).imK, (TrivSqZeroExt.snd d).imK) })
                      x) =
                  x) }
        { re := (yr, yrε), imI := (yi, yiε), imJ := (yj, yjε), imK := (yk, ykε) }
[PROOFSTEP]
rfl
