-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
h1 :
  TrivSqZeroExt.fst (M := ℍ[R])
      ({ 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
      (HMul.hMul (α := DualNumber ℍ[R])
        ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
        ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }))
⊢ ({ 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 }) =
    HMul.hMul (α := DualNumber ℍ[R])
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
      ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] })
have h2 : TrivSqZeroExt.snd (R := ℍ[R])
    ({ 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
    (HMul.hMul (α := DualNumber ℍ[R])
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
      ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }))
Tactic: ext : 1