-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
a :
  HSMul.hSMul (β := A) (x.re * y.re) 1 + HSMul.hSMul (β := A) (c₁ * x.imI * y.imI) 1 +
                                            HSMul.hSMul (β := A) (c₃ * x.imJ * y.imJ) 1 +
                                          HSMul.hSMul (β := A) (c₂ * c₃ * x.imJ * y.imK) 1 +
                                        -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1 +
                                      (x.re * y.imI) • q.i +
                                    (x.imI * y.re) • q.i +
                                  (c₂ * x.imI * y.imI) • q.i +
                                -((c₃ * x.imJ * y.imK) • q.i) +
                              (c₃ * x.imK * y.imJ) • q.i +
                            (x.re * y.imJ) • q.j +
                          (c₁ * x.imI * y.imK) • q.j +
                        (x.imJ * y.re) • q.j +
                      (c₂ * x.imJ * y.imI) • q.j +
                    -((c₁ * x.imK * y.imI) • q.j) +
                  (x.re * y.imK) • q.k +
                (x.imI * y.imJ) • q.k +
              (c₂ * x.imI * y.imK) • q.k +
            -((x.imJ * y.imI) • q.k) +
          (x.imK * y.re) • q.k +
        0 -
      (HSMul.hSMul (β := A) (x.re * y.re) 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
                                (x.imI * y.re) • q.i +
                              (x.imI * y.imI) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) +
                            (x.imI * y.imJ) • q.k +
                          (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                        (x.imJ * y.re) • q.j +
                      (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                    HSMul.hSMul (β := A) (x.imJ * c₃ * y.imJ) 1 +
                  (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
                (x.imK * y.re) • q.k +
              -((c₁ * x.imK * y.imI) • q.j) +
            (x.imK * c₃ * y.imJ) • q.i +
          -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1 +
        0) =
    0
⊢ HSMul.hSMul (β := A) (x.re * y.re) 1 + HSMul.hSMul (β := A) (c₁ * x.imI * y.imI) 1 +
                                        HSMul.hSMul (β := A) (c₃ * x.imJ * y.imJ) 1 +
                                      HSMul.hSMul (β := A) (c₂ * c₃ * x.imJ * y.imK) 1 +
                                    -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1 +
                                  (x.re * y.imI) • q.i +
                                (x.imI * y.re) • q.i +
                              (c₂ * x.imI * y.imI) • q.i +
                            -((c₃ * x.imJ * y.imK) • q.i) +
                          (c₃ * x.imK * y.imJ) • q.i +
                        (x.re * y.imJ) • q.j +
                      (c₁ * x.imI * y.imK) • q.j +
                    (x.imJ * y.re) • q.j +
                  (c₂ * x.imJ * y.imI) • q.j +
                -((c₁ * x.imK * y.imI) • q.j) +
              (x.re * y.imK) • q.k +
            (x.imI * y.imJ) • q.k +
          (c₂ * x.imI * y.imK) • q.k +
        -((x.imJ * y.imI) • q.k) +
      (x.imK * y.re) • q.k =
    HSMul.hSMul (β := A) (x.re * y.re) 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k +
                            (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                HSMul.hSMul (β := A) (x.imJ * c₃ * y.imJ) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1

Tactic:
linear_combination (norm := module)