Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_re
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK)

pp: case h2.e_imI
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ)

pp: case h2.e_imJ
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI)

pp: case h2.e_imK
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re)

Tactic:
<;>

Goal state after:
case h2.e_re
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK)

case h2.e_imI
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ)

case h2.e_imJ
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI)

case h2.e_imK
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re)