-- Mathlib/Algebra/QuaternionBasis.lean
theorem lift_mul (x y : ℍ[R,c₁,c₂,c₃]) : q.lift (x * y) = q.lift x * q.lift y

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (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) • (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) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((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 +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Tactic:
simp only [mul_re, sub_eq_add_neg, add_smul, neg_smul, mul_imI, ← add_assoc, mul_imJ, mul_imK]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x.re * y.re) • 1 + (c₁ * x.imI * y.imI) • 1 + (c₃ * x.imJ * y.imJ) • 1 + (c₂ * c₃ * x.imJ * y.imK) • 1 +
                                    -((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 =
    (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) • (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) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((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 +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (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) • (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) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((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 +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Tactic:
simp only [← mul_comm c₁ c₂, ← mul_assoc]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (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) • (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) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((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 +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (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) • (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) +
                (x.imJ * y.imJ * c₃) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Tactic:
simp only [mul_comm _ c₂, mul_right_comm _ _ c₃]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (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) • (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) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((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 +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re • 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) * (y.re • 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)

Tactic:
simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (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) • (q.i * q.i) + (x.imI * y.imJ) • (q.i * q.j) +
            (x.imI * y.imK) • (q.i * q.k)) +
        ((x.imJ * y.re) • q.j + (x.imJ * y.imI) • (q.j * q.i) + (x.imJ * y.imJ) • (q.j * q.j) +
          (x.imJ * y.imK) • (q.j * q.k)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • (q.k * q.i) + (x.imK * y.imJ) • (q.k * q.j) +
        (x.imK * y.imK) • (q.k * q.k))