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
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.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
a b : ℍ[R,c₁,c₂,c₃]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))

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
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.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
a b : ℍ[R,c₁,c₂,c₃]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.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
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))