Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.re +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imI +
          c₃ *
              (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
                c₁ * x✝².imK * x✝¹.imI) *
            x✝.imJ +
        c₂ * c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK -
      c₁ * c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imK =
    x✝².re *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
          c₃ * x✝².imJ *
            (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
              c₁ * x✝¹.imK * x✝.imI) +
        c₂ * c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
      c₁ * c₃ * x✝².imK *
        (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)

pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imI +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.re +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imI -
        c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK +
      c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imJ =
    x✝².re *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
            x✝².imI *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
              c₃ * x✝¹.imK * x✝.imJ) -
        c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
      c₃ * x✝².imK *
        (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)

pp: case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imJ +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imK +
          (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
            x✝.re +
        c₂ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI -
      c₁ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imI =
    x✝².re *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
          x✝².imJ *
            (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
              c₁ * c₃ * x✝¹.imK * x✝.imK) +
        c₂ * x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) -
      c₁ * x✝².imK *
        (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

pp: case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imK +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imJ +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imK -
        (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
            c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI +
      (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.re =
    x✝².re * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
            x✝².imI *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
        x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) +
      x✝².imK *
        (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
          c₁ * c₃ * x✝¹.imK * x✝.imK)

Tactic:
<;>

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.re +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imI +
          c₃ *
              (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
                c₁ * x✝².imK * x✝¹.imI) *
            x✝.imJ +
        c₂ * c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK -
      c₁ * c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imK =
    x✝².re *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
          c₃ * x✝².imJ *
            (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
              c₁ * x✝¹.imK * x✝.imI) +
        c₂ * c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
      c₁ * c₃ * x✝².imK *
        (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)

case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imI +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.re +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imI -
        c₃ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imK +
      c₃ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imJ =
    x✝².re *
              (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
                c₃ * x✝¹.imK * x✝.imJ) +
            x✝².imI *
              (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
                c₁ * c₃ * x✝¹.imK * x✝.imK) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK +
              c₃ * x✝¹.imK * x✝.imJ) -
        c₃ * x✝².imJ *
          (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
      c₃ * x✝².imK *
        (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)

case imJ
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imJ +
            c₁ *
                (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                  c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imK +
          (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
            x✝.re +
        c₂ *
            (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
              c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI -
      c₁ * (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) *
        x✝.imI =
    x✝².re *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
            c₁ * x✝².imI *
              (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
          x✝².imJ *
            (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
              c₁ * c₃ * x✝¹.imK * x✝.imK) +
        c₂ * x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) -
      c₁ * x✝².imK *
        (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

case imK
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝² x✝¹ x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (x✝².re * x✝¹.re + c₁ * x✝².imI * x✝¹.imI + c₃ * x✝².imJ * x✝¹.imJ + c₂ * c₃ * x✝².imJ * x✝¹.imK -
                c₁ * c₃ * x✝².imK * x✝¹.imK) *
              x✝.imK +
            (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
              x✝.imJ +
          c₂ *
              (x✝².re * x✝¹.imI + x✝².imI * x✝¹.re + c₂ * x✝².imI * x✝¹.imI - c₃ * x✝².imJ * x✝¹.imK +
                c₃ * x✝².imK * x✝¹.imJ) *
            x✝.imK -
        (x✝².re * x✝¹.imJ + c₁ * x✝².imI * x✝¹.imK + x✝².imJ * x✝¹.re + c₂ * x✝².imJ * x✝¹.imI -
            c₁ * x✝².imK * x✝¹.imI) *
          x✝.imI +
      (x✝².re * x✝¹.imK + x✝².imI * x✝¹.imJ + c₂ * x✝².imI * x✝¹.imK - x✝².imJ * x✝¹.imI + x✝².imK * x✝¹.re) * x✝.re =
    x✝².re * (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) +
            x✝².imI *
              (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI -
                c₁ * x✝¹.imK * x✝.imI) +
          c₂ * x✝².imI *
            (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re) -
        x✝².imJ *
          (x✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ) +
      x✝².imK *
        (x✝¹.re * x✝.re + c₁ * x✝¹.imI * x✝.imI + c₃ * x✝¹.imJ * x✝.imJ + c₂ * c₃ * x✝¹.imJ * x✝.imK -
          c₁ * c₃ * x✝¹.imK * x✝.imK)