-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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₃]
⊢ 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
have 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
Tactic: linear_combination (norm := module)