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