Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h1
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst
      ({ re := TrivSqZeroExt.fst (x✝ * y✝).re, imI := TrivSqZeroExt.fst (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.fst (x✝ * y✝).imJ, imK := TrivSqZeroExt.fst (x✝ * y✝).imK },
        { re := TrivSqZeroExt.snd (x✝ * y✝).re, imI := TrivSqZeroExt.snd (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.snd (x✝ * y✝).imJ, imK := TrivSqZeroExt.snd (x✝ * y✝).imK }) =
    TrivSqZeroExt.fst
      (({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.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 },
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }))

pp: case h2
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd
      ({ re := TrivSqZeroExt.fst (x✝ * y✝).re, imI := TrivSqZeroExt.fst (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.fst (x✝ * y✝).imJ, imK := TrivSqZeroExt.fst (x✝ * y✝).imK },
        { re := TrivSqZeroExt.snd (x✝ * y✝).re, imI := TrivSqZeroExt.snd (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.snd (x✝ * y✝).imJ, imK := TrivSqZeroExt.snd (x✝ * y✝).imK }) =
    TrivSqZeroExt.snd
      (({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.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 },
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }))

Tactic:
· rfl

Goal state after:
case h2
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd
      ({ re := TrivSqZeroExt.fst (x✝ * y✝).re, imI := TrivSqZeroExt.fst (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.fst (x✝ * y✝).imJ, imK := TrivSqZeroExt.fst (x✝ * y✝).imK },
        { re := TrivSqZeroExt.snd (x✝ * y✝).re, imI := TrivSqZeroExt.snd (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.snd (x✝ * y✝).imJ, imK := TrivSqZeroExt.snd (x✝ * y✝).imK }) =
    TrivSqZeroExt.snd
      (({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.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 },
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }))