[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ star (star x) = x
[PROOFSTEP]
unfold Star.star
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ { star := MulOpposite.unop ∘ ↑(↑(lift R) (MulOpposite.op ∘ ι R)) }.1
      ({ star := MulOpposite.unop ∘ ↑(↑(lift R) (MulOpposite.op ∘ ι R)) }.1 x) =
    x
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) x))) = x
[PROOFSTEP]
refine' FreeAlgebra.induction R X _ _ _ _ x
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (r : R),
    MulOpposite.unop
        (↑(↑(lift R) (MulOpposite.op ∘ ι R))
          (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (↑(algebraMap R (FreeAlgebra R X)) r)))) =
      ↑(algebraMap R (FreeAlgebra R X)) r
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
r✝ : R
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R))
        (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (↑(algebraMap R (FreeAlgebra R X)) r✝)))) =
    ↑(algebraMap R (FreeAlgebra R X)) r✝
[PROOFSTEP]
simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (x : X),
    MulOpposite.unop
        (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (ι R x)))) =
      ι R x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
x✝ : X
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (ι R x✝)))) =
    ι R x✝
[PROOFSTEP]
simp only [lift_ι_apply, Function.comp_apply, MulOpposite.unop_op]
[GOAL]
case refine'_3
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a))) =
        a →
      MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b))) =
          b →
        MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a * b)))) =
          a * b
[PROOFSTEP]
intros
[GOAL]
case refine'_3
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x a✝² b✝ : FreeAlgebra R X
a✝¹ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a✝²))) =
    a✝²
a✝ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b✝))) =
    b✝
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a✝² * b✝)))) =
    a✝² * b✝
[PROOFSTEP]
simp only [*, map_mul, MulOpposite.unop_mul]
[GOAL]
case refine'_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a))) =
        a →
      MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b))) =
          b →
        MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a + b)))) =
          a + b
[PROOFSTEP]
intros
[GOAL]
case refine'_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x a✝² b✝ : FreeAlgebra R X
a✝¹ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a✝²))) =
    a✝²
a✝ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b✝))) =
    b✝
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a✝² + b✝)))) =
    a✝² + b✝
[PROOFSTEP]
simp only [*, map_add, MulOpposite.unop_add]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ star (a * b) = star b * star a
[PROOFSTEP]
simp only [Function.comp_apply, map_mul, MulOpposite.unop_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ star (a + b) = star a + star b
[PROOFSTEP]
simp only [Function.comp_apply, map_add, MulOpposite.unop_add]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : X
⊢ star (ι R x) = ι R x
[PROOFSTEP]
simp [star, Star.star]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
r : R
⊢ star (↑(algebraMap R (FreeAlgebra R X)) r) = ↑(algebraMap R (FreeAlgebra R X)) r
[PROOFSTEP]
simp [star, Star.star]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
src✝ : FreeAlgebra R X ≃+* (FreeAlgebra R X)ᵐᵒᵖ := starRingEquiv
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (FreeAlgebra R X)) r) = ↑(algebraMap R (FreeAlgebra R X)ᵐᵒᵖ) r
[PROOFSTEP]
simp [star_algebraMap]


[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


[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle : x ≤ y
z : R
⊢ z + x ≤ z + y
[PROOFSTEP]
rw [StarOrderedRing.le_iff] at hle ⊢
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle✝ : x ≤ y
hle : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
z : R
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ z + y = z + x + p
[PROOFSTEP]
refine hle.imp fun s hs ↦ ?_
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle✝ : x ≤ y
hle : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ z + y = z + x + s
[PROOFSTEP]
rw [hs.2, add_assoc]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : R
hle✝ : x ≤ y
hle : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
z s : R
hs : s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + s
⊢ s ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ z + (x + s) = z + (x + s)
[PROOFSTEP]
exact ⟨hs.1, rfl⟩
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
obtain ⟨p, hp⟩ := (h_le_iff x y).mp h
[GOAL]
case refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩
[GOAL]
case refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y : R
⊢ (∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p) → x ≤ y
[PROOFSTEP]
rintro ⟨p, hp, hpxy⟩
[GOAL]
case refine'_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
x y p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hpxy : y = x + p
⊢ x ≤ y
[PROOFSTEP]
revert x y hpxy
[GOAL]
case refine'_2.intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x y : R), y = x + p → x ≤ y
[PROOFSTEP]
refine' AddSubmonoid.closure_induction hp _ (fun x y h => add_zero x ▸ h.ge) _
[GOAL]
case refine'_2.intro.intro.refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x : R), (x ∈ Set.range fun s => star s * s) → ∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ x y rfl
[GOAL]
case refine'_2.intro.intro.refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
s x : R
⊢ x ≤ x + (fun s => star s * s) s
[PROOFSTEP]
exact (h_le_iff _ _).mpr ⟨s, rfl⟩
[GOAL]
case refine'_2.intro.intro.refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x y : R),
    (∀ (x_1 y : R), y = x_1 + x → x_1 ≤ y) →
      (∀ (x y_1 : R), y_1 = x + y → x ≤ y_1) → ∀ (x_1 y_1 : R), y_1 = x_1 + (x + y) → x_1 ≤ y_1
[PROOFSTEP]
rintro a b ha hb x y rfl
[GOAL]
case refine'_2.intro.intro.refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a b : R
ha : ∀ (x y : R), y = x + a → x ≤ y
hb : ∀ (x y : R), y = x + b → x ≤ y
x : R
⊢ x ≤ x + (a + b)
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_2.intro.intro.refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
a b : R
ha : ∀ (x y : R), y = x + a → x ≤ y
hb : ∀ (x y : R), y = x + b → x ≤ y
x : R
⊢ x ≤ x + a + b
[PROOFSTEP]
exact (ha _ _ rfl).trans (hb _ _ rfl)
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
x y : R
⊢ x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
x y : R
this : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
[PROOFSTEP]
simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
[PROOFSTEP]
haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
[GOAL]
R : Type u
inst✝² : NonUnitalRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y
h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s
this : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
[PROOFSTEP]
simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x : R
⊢ 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
simp only [le_iff, zero_add, exists_eq_right']
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
r : R
⊢ 0 ≤ r * star r
[PROOFSTEP]
simpa only [star_star] using star_mul_self_nonneg (star r)
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ star c * a * c
[PROOFSTEP]
rw [StarOrderedRing.nonneg_iff] at ha
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c : R
⊢ 0 ≤ star c * a * c
[PROOFSTEP]
refine' AddSubmonoid.closure_induction ha (fun x hx => _) (by rw [mul_zero, zero_mul]) fun x y hx hy => _
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c : R
⊢ 0 ≤ star c * 0 * c
[PROOFSTEP]
rw [mul_zero, zero_mul]
[GOAL]
case refine'_1
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
hx : x ∈ Set.range fun s => star s * s
⊢ 0 ≤ star c * x * c
[PROOFSTEP]
obtain ⟨x, rfl⟩ := hx
[GOAL]
case refine'_1.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
⊢ 0 ≤ star c * (fun s => star s * s) x * c
[PROOFSTEP]
convert star_mul_self_nonneg (x * c) using 1
[GOAL]
case h.e'_4
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x : R
⊢ star c * (fun s => star s * s) x * c = star (x * c) * (x * c)
[PROOFSTEP]
rw [star_mul, ← mul_assoc, mul_assoc _ _ c]
[GOAL]
case refine'_2
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * (x + y) * c
[PROOFSTEP]
calc
  0 ≤ star c * x * c + 0 := by rw [add_zero]; exact hx
  _ ≤ star c * x * c + star c * y * c := (add_le_add_left hy _)
  _ ≤ _ := by rw [mul_add, add_mul]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c + 0
[PROOFSTEP]
rw [add_zero]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ 0 ≤ star c * x * c
[PROOFSTEP]
exact hx
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha✝ : 0 ≤ a
ha : a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
c x y : R
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + star c * y * c ≤ star c * (x + y) * c
[PROOFSTEP]
rw [mul_add, add_mul]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ c * a * star c
[PROOFSTEP]
simpa only [star_star] using conjugate_nonneg ha (star c)
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ star c * a * c ≤ star c * b * c
[PROOFSTEP]
rw [StarOrderedRing.le_iff] at hab ⊢
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab✝ : a ≤ b
hab : ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ b = a + p
c : R
⊢ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ star c * b * c = star c * a * c + p
[PROOFSTEP]
obtain ⟨p, hp, rfl⟩ := hab
[GOAL]
case intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hp : p ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
hab : a ≤ a + p
⊢ ∃ p_1, p_1 ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ star c * (a + p) * c = star c * a * c + p_1
[PROOFSTEP]
simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢
[GOAL]
case intro.intro
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hab : a ≤ a + p
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
[PROOFSTEP]
exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a c p : R
hab : a ≤ a + p
hp : 0 ≤ p
⊢ star c * (a + p) * c = star c * a * c + star c * p * c
[PROOFSTEP]
simp only [add_mul, mul_add]
[GOAL]
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c
[PROOFSTEP]
simpa only [star_star] using conjugate_le_conjugate hab (star c)


[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B ∈ {U | star U * U = 1 ∧ U * star U = 1}
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star (U * B) * (U * B) = 1
[PROOFSTEP]
calc
  star (U * B) * (U * B) = star B * star U * U * B := by simp only [mul_assoc, star_mul]
  _ = star B * (star U * U) * B := by rw [← mul_assoc]
  _ = 1 := by rw [hA₁, mul_one, hB₁]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star (U * B) * (U * B) = star B * star U * U * B
[PROOFSTEP]
simp only [mul_assoc, star_mul]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * star U * U * B = star B * (star U * U) * B
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * (star U * U) * B = 1
[PROOFSTEP]
rw [hA₁, mul_one, hB₁]
[GOAL]
case refine'_2
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = 1
[PROOFSTEP]
calc
  U * B * star (U * B) = U * B * (star B * star U) := by rw [star_mul]
  _ = U * (B * star B) * star U := by simp_rw [← mul_assoc]
  _ = 1 := by rw [hB₂, mul_one, hA₂]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = U * B * (star B * star U)
[PROOFSTEP]
rw [star_mul]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * (B * star B) * star U
[PROOFSTEP]
simp_rw [← mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * (B * star B) * star U = 1
[PROOFSTEP]
rw [hB₂, mul_one, hA₂]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ 1 ∈
    { carrier := {U | star U * U = 1 ∧ U * star U = 1},
        mul_mem' :=
          (_ :
            ∀ (U B : R),
              U ∈ {U | star U * U = 1 ∧ U * star U = 1} →
                B ∈ {U | star U * U = 1 ∧ U * star U = 1} → U * B ∈ {U | star U * U = 1 ∧ U * star U = 1}) }.carrier
[PROOFSTEP]
simp only [mul_one, and_self_iff, Set.mem_setOf_eq, star_one]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U : R
hU : U ∈ unitary R
⊢ star (star U) * star U = 1
[PROOFSTEP]
rw [star_star, mul_star_self_of_mem hU]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
U : R
hU : U ∈ unitary R
⊢ star U * star (star U) = 1
[PROOFSTEP]
rw [star_star, star_mul_self_of_mem hU]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ Function.Involutive star
[PROOFSTEP]
intro x
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x : { x // x ∈ unitary R }
⊢ star (star x) = x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x : { x // x ∈ unitary R }
⊢ ↑(star (star x)) = ↑x
[PROOFSTEP]
rw [coe_star, coe_star, star_star]
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
⊢ ∀ (r s : { x // x ∈ unitary R }), star (r * s) = star s * star r
[PROOFSTEP]
intro x y
[GOAL]
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x y : { x // x ∈ unitary R }
⊢ star (x * y) = star y * star x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarSemigroup R
x y : { x // x ∈ unitary R }
⊢ ↑(star (x * y)) = ↑(star y * star x)
[PROOFSTEP]
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]
[GOAL]
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U₁ U₂ : { x // x ∈ unitary R }
⊢ ↑(U₁ / U₂) = ↑U₁ / ↑U₂
[PROOFSTEP]
simp only [div_eq_mul_inv, coe_inv, Submonoid.coe_mul]
[GOAL]
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
z : ℤ
⊢ ↑(U ^ z) = ↑U ^ z
[PROOFSTEP]
induction z
[GOAL]
case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝
[PROOFSTEP]
simp [SubmonoidClass.coe_pow]
[GOAL]
case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝
[PROOFSTEP]
simp [coe_inv]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
U : { x // x ∈ unitary R }
⊢ -↑U ∈ unitary R
[PROOFSTEP]
simp [mem_iff, star_neg, neg_mul_neg]


[GOAL]
R : Type u
inst✝ : InvolutiveStar R
r s : R
h : r = star s
⊢ s = star r
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y : R
⊢ star (star x * y) = star y * x
[PROOFSTEP]
rw [star_mul, star_star]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y : R
⊢ star (x * star y) = y * star x
[PROOFSTEP]
rw [star_mul, star_star]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
[PROOFSTEP]
simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
x y : R
⊢ Commute (star x) y ↔ Commute x (star y)
[PROOFSTEP]
rw [← commute_star_star, star_star]
[GOAL]
R : Type u
inst✝¹ : Semigroup R
inst✝ : StarSemigroup R
src✝ : R ≃ Rᵐᵒᵖ := (Function.Involutive.toPerm star (_ : Function.Involutive star)).trans opEquiv
x y : R
⊢ Equiv.toFun
      { toFun := fun x => op (star x), invFun := src✝.invFun,
        left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (x * y) =
    Equiv.toFun
        { toFun := fun x => op (star x), invFun := src✝.invFun,
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x *
      Equiv.toFun
        { toFun := fun x => op (star x), invFun := src✝.invFun,
          left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y
[PROOFSTEP]
simp only [star_mul, op_mul]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ star x ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
simp only [ne_eq, star_eq_zero]
[GOAL]
R : Type u
S : Type u_1
inst✝² : NonAssocSemiring S
inst✝¹ : CommSemiring R
inst✝ : StarRing R
⊢ Function.Involutive star
[PROOFSTEP]
intro
[GOAL]
R : Type u
S : Type u_1
inst✝² : NonAssocSemiring S
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : S →+* R
⊢ star (star x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type u_1
inst✝² : NonAssocSemiring S
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝¹ : S →+* R
x✝ : S
⊢ ↑(star (star x✝¹)) x✝ = ↑x✝¹ x✝
[PROOFSTEP]
simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]
[GOAL]
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ star (x / y) = star x / star y
[PROOFSTEP]
apply op_injective
[GOAL]
case a
R : Type u
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
⊢ op (star (x / y)) = op (star x / star y)
[PROOFSTEP]
rw [division_def, op_div, mul_comm, star_mul, star_inv', op_mul, op_inv]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
r : R
⊢ star (bit0 r) = bit0 (star r)
[PROOFSTEP]
simp [bit0]
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R
⊢ star (bit1 r) = bit1 (star r)
[PROOFSTEP]
simp [bit1]
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
⊢ inverse (star a) = star (inverse a)
[PROOFSTEP]
by_cases ha : IsUnit a
[GOAL]
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : IsUnit a
⊢ inverse (star a) = star (inverse a)
[PROOFSTEP]
obtain ⟨u, rfl⟩ := ha
[GOAL]
case pos.intro
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ inverse (star ↑u) = star (inverse ↑u)
[PROOFSTEP]
rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ inverse (star a) = star (inverse a)
[PROOFSTEP]
rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
r : R
inst✝ : Invertible r
⊢ Star.star ⅟r * Star.star r = 1
[PROOFSTEP]
rw [← star_mul, mul_invOf_self, star_one]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarSemigroup R
r : R
inst✝ : Invertible r
⊢ Star.star r * Star.star ⅟r = 1
[PROOFSTEP]
rw [← star_mul, invOf_mul_self, star_one]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = ⅟(star r)
[PROOFSTEP]
have : star (⅟r) = star (⅟r) * ((star r) * ⅟(star r)) := by simp only [mul_invOf_self, mul_one]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = star ⅟r * (star r * ⅟(star r))
[PROOFSTEP]
simp only [mul_invOf_self, mul_one]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r = ⅟(star r)
[PROOFSTEP]
rw [this, ← mul_assoc]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)
[PROOFSTEP]
have : (star (⅟r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r = star 1
[PROOFSTEP]
rw [← star_mul, mul_invOf_self]
[GOAL]
R✝ : Type u
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarSemigroup R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this✝ : star ⅟r = star ⅟r * (star r * ⅟(star r))
this : star ⅟r * star r = star 1
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)
[PROOFSTEP]
rw [this, star_one, one_mul]