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) * x✝.re + c₁ * (x✝².imI + x✝¹.imI) * x✝.imI + c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imJ +
        c₂ * c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK -
      c₁ * c₃ * (x✝².imK + x✝¹.imK) * 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 +
      (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)

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) * x✝.imI + (x✝².imI + x✝¹.imI) * x✝.re + c₂ * (x✝².imI + x✝¹.imI) * x✝.imI -
        c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK +
      c₃ * (x✝².imK + x✝¹.imK) * 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✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

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) * x✝.imJ + c₁ * (x✝².imI + x✝¹.imI) * x✝.imK + (x✝².imJ + x✝¹.imJ) * x✝.re +
        c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imI -
      c₁ * (x✝².imK + x✝¹.imK) * 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 +
      (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 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) * x✝.imK + (x✝².imI + x✝¹.imI) * x✝.imJ + c₂ * (x✝².imI + x✝¹.imI) * x✝.imK -
        (x✝².imJ + x✝¹.imJ) * x✝.imI +
      (x✝².imK + x✝¹.imK) * x✝.re =
    x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re +
      (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)

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) * x✝.re + c₁ * (x✝².imI + x✝¹.imI) * x✝.imI + c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imJ +
        c₂ * c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK -
      c₁ * c₃ * (x✝².imK + x✝¹.imK) * 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 +
      (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)

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) * x✝.imI + (x✝².imI + x✝¹.imI) * x✝.re + c₂ * (x✝².imI + x✝¹.imI) * x✝.imI -
        c₃ * (x✝².imJ + x✝¹.imJ) * x✝.imK +
      c₃ * (x✝².imK + x✝¹.imK) * 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✝¹.re * x✝.imI + x✝¹.imI * x✝.re + c₂ * x✝¹.imI * x✝.imI - c₃ * x✝¹.imJ * x✝.imK + c₃ * x✝¹.imK * x✝.imJ)

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) * x✝.imJ + c₁ * (x✝².imI + x✝¹.imI) * x✝.imK + (x✝².imJ + x✝¹.imJ) * x✝.re +
        c₂ * (x✝².imJ + x✝¹.imJ) * x✝.imI -
      c₁ * (x✝².imK + x✝¹.imK) * 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 +
      (x✝¹.re * x✝.imJ + c₁ * x✝¹.imI * x✝.imK + x✝¹.imJ * x✝.re + c₂ * x✝¹.imJ * x✝.imI - c₁ * x✝¹.imK * x✝.imI)

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) * x✝.imK + (x✝².imI + x✝¹.imI) * x✝.imJ + c₂ * (x✝².imI + x✝¹.imI) * x✝.imK -
        (x✝².imJ + x✝¹.imJ) * x✝.imI +
      (x✝².imK + x✝¹.imK) * x✝.re =
    x✝².re * x✝.imK + x✝².imI * x✝.imJ + c₂ * x✝².imI * x✝.imK - x✝².imJ * x✝.imI + x✝².imK * x✝.re +
      (x✝¹.re * x✝.imK + x✝¹.imI * x✝.imJ + c₂ * x✝¹.imI * x✝.imK - x✝¹.imJ * x✝.imI + x✝¹.imK * x✝.re)