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