Module: Mathlib.Algebra.DualQuaternion

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

Tactic:
congr 1 <;> simp

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)