awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    imI (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    imJ (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    imK (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).re
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imI
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imJ
imK :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imK
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
      { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
ext
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imI

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } -
        { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] }).imK

Tactic:
simp
-- 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₃
rw : q.i * (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
rw₁ : q.i * q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₂ : (HSMul.hSMul (β := A) c₁ 1 + c₂ • q.i) * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₃ : HSMul.hSMul (β := A) c₁ 1 * q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₄ : c₁ • (1 * q.j) + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₅ : c₁ • q.j + c₂ • q.i * q.j = c₁ • q.j + c₂ • (q.i * q.j)
rw₆ rw₇ : c₁ • q.j + c₂ • (q.i * q.j) = c₁ • q.j + c₂ • (q.i * q.j)
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k

Tactic:
rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]

Premises used: add_mul, QuaternionAlgebra.Basis.i_mul_i, QuaternionAlgebra.Basis.i_mul_j, mul_assoc, smul_mul_assoc, one_mul
-- 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₃
rw : c₂ • q.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)
⊢ q.k * q.i = -c₁ • q.j

Tactic:
rw [← i_mul_j, mul_assoc, j_mul_i, mul_sub, i_mul_k, neg_smul, mul_smul_comm, i_mul_j]

Premises used: neg_smul, mul_sub, QuaternionAlgebra.Basis.i_mul_j, mul_assoc, QuaternionAlgebra.Basis.j_mul_i, mul_smul_comm, QuaternionAlgebra.Basis.i_mul_k
-- 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₃
⊢ c₂ • q.k - (c₁ • q.j + c₂ • q.k) + 0 - (-(c₁ • q.j) + 0) = 0

Tactic:
module
-- 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₃
a : c₂ • q.k - (c₁ • q.j + c₂ • q.k) + 0 - (-(c₁ • q.j) + 0) = 0
⊢ c₂ • q.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)

Tactic:
linear_combination (norm := module)
-- 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₃
rw : q.i * q.j * q.j = c₃ • q.i
rw₁ : q.i * (q.j * q.j) = c₃ • q.i
rw₂ : q.i * HSMul.hSMul (β := A) c₃ 1 = c₃ • q.i
rw₃ : c₃ • (q.i * 1) = c₃ • q.i
rw₄ rw₅ : c₃ • q.i = c₃ • q.i
⊢ q.k * q.j = c₃ • q.i

Tactic:
rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]

Premises used: QuaternionAlgebra.Basis.j_mul_j, QuaternionAlgebra.Basis.i_mul_j, mul_assoc, mul_smul_comm, mul_one
-- 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₃
rw : HSMul.hSMul (β := A) (c₂ • c₃) 1 - c₃ • q.i = HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i
⊢ q.j * q.k = HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i

Tactic:
rw [← i_mul_j, ← mul_assoc, j_mul_i, sub_mul, smul_mul_assoc, j_mul_j, ← smul_assoc, k_mul_j]

Premises used: smul_assoc, QuaternionAlgebra.Basis.j_mul_j, QuaternionAlgebra.Basis.i_mul_j, mul_assoc, smul_mul_assoc, sub_mul, QuaternionAlgebra.Basis.j_mul_i, QuaternionAlgebra.Basis.k_mul_j
-- 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₃
⊢ HSMul.hSMul (β := A) (c₂ • c₃) 1 - c₃ • q.i = HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i

Tactic:
rfl
-- 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₃
rw :
  c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) =
    -HSMul.hSMul (β := A) (c₁ * c₃) 1
⊢ q.k * q.k = -HSMul.hSMul (β := A) (c₁ * c₃) 1

Tactic:
rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_sub, ←
    mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, sub_mul, smul_mul_assoc, mul_smul_comm,
    smul_mul_assoc, mul_assoc, j_mul_j, add_mul, smul_mul_assoc, j_mul_j, smul_smul,
    smul_mul_assoc, mul_assoc, j_mul_j]

Premises used: add_mul, QuaternionAlgebra.Basis.i_mul_i, mul_sub, QuaternionAlgebra.Basis.j_mul_j, QuaternionAlgebra.Basis.i_mul_j, mul_assoc, smul_smul, smul_mul_assoc, sub_mul, QuaternionAlgebra.Basis.j_mul_i, mul_smul_comm, QuaternionAlgebra.Basis.j, one_mul
-- 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₃
⊢ c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) +
        0 -
      (-HSMul.hSMul (β := A) (c₁ * c₃) 1 + 0) =
    0

Tactic:
module
-- 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₃
a :
  c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) +
        0 -
      (-HSMul.hSMul (β := A) (c₁ * c₃) 1 + 0) =
    0
⊢ c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1) - (HSMul.hSMul (β := A) (c₁ * c₃) 1 + c₂ • (q.i * HSMul.hSMul (β := A) c₃ 1)) =
    -HSMul.hSMul (β := A) (c₁ * c₃) 1

Tactic:
linear_combination (norm := module)
-- 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₃
⊢ q.lift 0 = 0

Tactic:
simp [lift]

Premises used: QuaternionAlgebra.Basis.lift
-- 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₃
⊢ q.lift 1 = 1

Tactic:
simp [lift]

Premises used: QuaternionAlgebra.Basis.lift
-- 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₃]
simp :
  HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) x.re : A) ((algebraMap R A : (a : R) → A) y.re : A) +
          (x.imI • q.i + y.imI • q.i) +
        (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A) (x.imI • q.i) + x.imJ • q.j + x.imK • q.k +
      (HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) y.re : A) (y.imI • q.i) + y.imJ • q.j + y.imK • q.k)
⊢ q.lift (x + y) = q.lift x + q.lift y

Tactic:
simp only [lift, re_add, map_add, imI_add, add_smul, imJ_add, imK_add]

Premises used: QuaternionAlgebra.re_add, QuaternionAlgebra.imK_add, QuaternionAlgebra.imI_add, map_add, add_smul, QuaternionAlgebra.Basis.lift, QuaternionAlgebra.imJ_add
-- 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₃]
⊢ HAdd.hAdd (α := A) (β := A) ((algebraMap R A : (a : R) → A) x.re : A) ((algebraMap R A : (a : R) → A) y.re : A) +
          (x.imI • q.i + y.imI • q.i) +
        (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A) (x.imI • q.i) + x.imJ • q.j + x.imK • q.k +
      (HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) y.re : A) (y.imI • q.i) + y.imJ • q.j + y.imK • q.k)

Tactic:
abel
-- 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₃]
simp :
  HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (HSMul.hSMul (β := A) x.re 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) *
      (HSMul.hSMul (β := A) y.re 1 + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
⊢ q.lift (x * y) = q.lift x * q.lift y

Tactic:
simp only [lift, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, QuaternionAlgebra.Basis.lift
-- 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₃]
simp_rw :
  HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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) • (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))
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (HSMul.hSMul (β := A) x.re 1 + x.imI • q.i + x.imJ • q.j + x.imK • q.k) *
      (HSMul.hSMul (β := A) 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]

Premises used: add_mul, smul_smul, smul_mul_assoc, mul_smul_comm, mul_add, mul_one, one_mul
-- 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₃]
simp :
  HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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) + (x.imJ * y.imJ) • HSMul.hSMul (β := A) c₃ 1 +
          (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₃ • q.i +
        (x.imK * y.imK) • -HSMul.hSMul (β := A) (c₁ * c₃) 1)
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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) • (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))

Tactic:
simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]

Premises used: QuaternionAlgebra.Basis.i_mul_i, QuaternionAlgebra.Basis.k_mul_i, QuaternionAlgebra.Basis.j_mul_j, QuaternionAlgebra.Basis.i_mul_j, QuaternionAlgebra.Basis.j_mul_k, QuaternionAlgebra.Basis.k_mul_k, QuaternionAlgebra.Basis.j_mul_i, QuaternionAlgebra.Basis.k_mul_j, QuaternionAlgebra.Basis.i_mul_k
-- 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₃]
simp :
  HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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 * y.imJ * c₃) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (x.imK * y.imK * (c₁ * c₃)) 1
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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) + (x.imJ * y.imJ) • HSMul.hSMul (β := A) c₃ 1 +
          (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 - c₃ • q.i)) +
      ((x.imK * y.re) • q.k + (x.imK * y.imI) • -c₁ • q.j + (x.imK * y.imJ) • c₃ • q.i +
        (x.imK * y.imK) • -HSMul.hSMul (β := A) (c₁ * c₃) 1)

Tactic:
simp only [smul_smul, smul_neg, sub_eq_add_neg, ← add_assoc, neg_smul]

Premises used: neg_smul, add_assoc, sub_eq_add_neg, smul_smul, smul_neg
-- 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₃]
simp :
  HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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 * y.imJ * c₃) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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 * y.imJ * c₃) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (x.imK * y.imK * (c₁ * c₃)) 1

Tactic:
simp only [mul_right_comm _ _ (c₁ * c₃), mul_comm _ (c₁ * c₃)]

Premises used: HMul.hMul, mul_right_comm, mul_comm
-- 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₃]
simp :
  HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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 * y.imJ * c₃) 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 * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1
⊢ HSMul.hSMul (β := A) (x * y).re 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • 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 * y.imJ * c₃) 1 +
              (x.imJ * y.imK) • (HSMul.hSMul (β := A) (c₂ * c₃) 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((x.imK * y.imI * c₁) • q.j) +
        (x.imK * y.imJ * c₃) • q.i +
      -HSMul.hSMul (β := A) (c₁ * c₃ * x.imK * y.imK) 1

Tactic:
simp only [mul_comm _ c₁]

Premises used: mul_comm