awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : AddCommGroupWithOne R
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑0 : R) : ℍ[R,c₁,c₂,c₃]) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : AddCommGroupWithOne R
⊢ ∀ (n : ℕ), (↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]) = HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑(↑n : R) : ℍ[R,c₁,c₂,c₃]) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : AddCommGroupWithOne R
n : ℕ
change :
  Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(n + 1) : ℍ[R,c₁,c₂,c₃]))

Tactic:
change coe _ = -coe _

Premises used: QuaternionAlgebra.coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : AddCommGroupWithOne R
n : ℕ
rw : Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(-(↑(n + 1) : R)) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
rw₁ rw₂ : Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃])) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))

Tactic:
rw [Int.cast_negSucc, coe_neg]

Premises used: Int.cast_negSucc, QuaternionAlgebra.coe_neg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := R) (re (a := c₁) (b := c₂) (c := c₃) (↑n : ℍ[R,c₁,c₂,c₃])) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := R) (imI (a := c₁) (b := c₂) (c := c₃) (↑n : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := R) (imJ (a := c₁) (b := c₂) (c := c₃) (↑n : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := R) (imK (a := c₁) (b := c₂) (c := c₃) (↑n : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (im (↑n : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑n : R) : ℍ[R,c₁,c₂,c₃]) (↑n : ℍ[R,c₁,c₂,c₃])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
z : ℤ
⊢ Eq.{u_3 + 1} (α := R) (re (a := c₁) (b := c₂) (c := c₃) (↑z : ℍ[R,c₁,c₂,c₃])) (↑z : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := R) (re (a := c₁) (b := c₂) (c := c₃) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := R) (imI (a := c₁) (b := c₂) (c := c₃) (OfNat.ofNat n)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := R) (imJ (a := c₁) (b := c₂) (c := c₃) (OfNat.ofNat n)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := R) (imK (a := c₁) (b := c₂) (c := c₃) (OfNat.ofNat n)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (im (OfNat.ofNat n)) 0

Tactic:
rfl

Premises used: QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
z : ℤ
⊢ Eq.{u_3 + 1} (α := R) (imI (a := c₁) (b := c₂) (c := c₃) (↑z : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
z : ℤ
⊢ Eq.{u_3 + 1} (α := R) (imJ (a := c₁) (b := c₂) (c := c₃) (↑z : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
z : ℤ
⊢ Eq.{u_3 + 1} (α := R) (imK (a := c₁) (b := c₂) (c := c₃) (↑z : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
z : ℤ
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (im (↑z : ℍ[R,c₁,c₂,c₃])) 0

Tactic:
rfl

Premises used: QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : AddCommGroupWithOne R
z : ℤ
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑z : R) : ℍ[R,c₁,c₂,c₃]) (↑z : ℍ[R,c₁,c₂,c₃])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re
imI : (x_1 * x_2 * x_3).imI = (x_1 * (x_2 * x_3)).imI
imJ : (x_1 * x_2 * x_3).imJ = (x_1 * (x_2 * x_3)).imJ
imK : (x_1 * x_2 * x_3).imK = (x_1 * (x_2 * x_3)).imK
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
re :
  (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.re +
            c₁ *
                (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                  c₃ * x_1.imK * x_2.imJ) *
              x_3.imI +
          c₃ *
              (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
                c₁ * x_1.imK * x_2.imI) *
            x_3.imJ +
        c₂ * c₃ *
            (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
          x_3.imK -
      c₁ * c₃ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
        x_3.imK =
    x_1.re *
              (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
                c₁ * c₃ * x_2.imK * x_3.imK) +
            c₁ * x_1.imI *
              (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
                c₃ * x_2.imK * x_3.imJ) +
          c₃ * x_1.imJ *
            (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
              c₁ * x_2.imK * x_3.imI) +
        c₂ * c₃ * x_1.imJ *
          (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) -
      c₁ * c₃ * x_1.imK *
        (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re)
⊢ (x_1 * x_2 * x_3).re = (x_1 * (x_2 * x_3)).re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
imI :
  (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.imI +
            (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
              x_3.re +
          c₂ *
              (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
            x_3.imI -
        c₃ *
            (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
          x_3.imK +
      c₃ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
        x_3.imJ =
    x_1.re *
              (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
                c₃ * x_2.imK * x_3.imJ) +
            x_1.imI *
              (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
                c₁ * c₃ * x_2.imK * x_3.imK) +
          c₂ * x_1.imI *
            (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
              c₃ * x_2.imK * x_3.imJ) -
        c₃ * x_1.imJ *
          (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
      c₃ * x_1.imK *
        (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI - c₁ * x_2.imK * x_3.imI)
⊢ (x_1 * x_2 * x_3).imI = (x_1 * (x_2 * x_3)).imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
imJ :
  (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.imJ +
            c₁ *
                (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                  c₃ * x_1.imK * x_2.imJ) *
              x_3.imK +
          (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
            x_3.re +
        c₂ *
            (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
          x_3.imI -
      c₁ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
        x_3.imI =
    x_1.re *
              (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
                c₁ * x_2.imK * x_3.imI) +
            c₁ * x_1.imI *
              (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
          x_1.imJ *
            (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
              c₁ * c₃ * x_2.imK * x_3.imK) +
        c₂ * x_1.imJ *
          (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
            c₃ * x_2.imK * x_3.imJ) -
      c₁ * x_1.imK *
        (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK + c₃ * x_2.imK * x_3.imJ)
⊢ (x_1 * x_2 * x_3).imJ = (x_1 * (x_2 * x_3)).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
imK :
  (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.imK +
            (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
              x_3.imJ +
          c₂ *
              (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
            x_3.imK -
        (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
            c₁ * x_1.imK * x_2.imI) *
          x_3.imI +
      (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) * x_3.re =
    x_1.re * (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
            x_1.imI *
              (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
                c₁ * x_2.imK * x_3.imI) +
          c₂ * x_1.imI *
            (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) -
        x_1.imJ *
          (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
            c₃ * x_2.imK * x_3.imJ) +
      x_1.imK *
        (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
          c₁ * c₃ * x_2.imK * x_3.imK)
⊢ (x_1 * x_2 * x_3).imK = (x_1 * (x_2 * x_3)).imK

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.re +
            c₁ *
                (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                  c₃ * x_1.imK * x_2.imJ) *
              x_3.imI +
          c₃ *
              (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
                c₁ * x_1.imK * x_2.imI) *
            x_3.imJ +
        c₂ * c₃ *
            (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
          x_3.imK -
      c₁ * c₃ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
        x_3.imK =
    x_1.re *
              (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
                c₁ * c₃ * x_2.imK * x_3.imK) +
            c₁ * x_1.imI *
              (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
                c₃ * x_2.imK * x_3.imJ) +
          c₃ * x_1.imJ *
            (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
              c₁ * x_2.imK * x_3.imI) +
        c₂ * c₃ * x_1.imJ *
          (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) -
      c₁ * c₃ * x_1.imK *
        (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re)

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.imI +
            (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
              x_3.re +
          c₂ *
              (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
            x_3.imI -
        c₃ *
            (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
          x_3.imK +
      c₃ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
        x_3.imJ =
    x_1.re *
              (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
                c₃ * x_2.imK * x_3.imJ) +
            x_1.imI *
              (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
                c₁ * c₃ * x_2.imK * x_3.imK) +
          c₂ * x_1.imI *
            (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
              c₃ * x_2.imK * x_3.imJ) -
        c₃ * x_1.imJ *
          (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
      c₃ * x_1.imK *
        (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI - c₁ * x_2.imK * x_3.imI)

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.imJ +
            c₁ *
                (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                  c₃ * x_1.imK * x_2.imJ) *
              x_3.imK +
          (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
            x_3.re +
        c₂ *
            (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
              c₁ * x_1.imK * x_2.imI) *
          x_3.imI -
      c₁ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
        x_3.imI =
    x_1.re *
              (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
                c₁ * x_2.imK * x_3.imI) +
            c₁ * x_1.imI *
              (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
          x_1.imJ *
            (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
              c₁ * c₃ * x_2.imK * x_3.imK) +
        c₂ * x_1.imJ *
          (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
            c₃ * x_2.imK * x_3.imJ) -
      c₁ * x_1.imK *
        (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK + c₃ * x_2.imK * x_3.imJ)

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
                c₁ * c₃ * x_1.imK * x_2.imK) *
              x_3.imK +
            (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
              x_3.imJ +
          c₂ *
              (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
            x_3.imK -
        (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
            c₁ * x_1.imK * x_2.imI) *
          x_3.imI +
      (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) * x_3.re =
    x_1.re * (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
            x_1.imI *
              (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
                c₁ * x_2.imK * x_3.imI) +
          c₂ * x_1.imI *
            (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) -
        x_1.imJ *
          (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
            c₃ * x_2.imK * x_3.imJ) +
      x_1.imK *
        (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
          c₁ * c₃ * x_2.imK * x_3.imK)

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
re : (1 * x_1).re = x_1.re
imI : (1 * x_1).imI = x_1.imI
imJ : (1 * x_1).imJ = x_1.imJ
imK : (1 * x_1).imK = x_1.imK
⊢ 1 * x_1 = x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x_1).re = x_1.re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x_1).imI = x_1.imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x_1).imJ = x_1.imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (1 * x_1).imK = x_1.imK

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 1).re = x_1.re
imI : (x_1 * 1).imI = x_1.imI
imJ : (x_1 * 1).imJ = x_1.imJ
imK : (x_1 * 1).imK = x_1.imK
⊢ x_1 * 1 = x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * 1).re = x_1.re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * 1).imI = x_1.imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * 1).imJ = x_1.imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * 1).imK = x_1.imK

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
re : (0 * x_1).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
imI : (0 * x_1).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) 0
imJ : (0 * x_1).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) 0
imK : (0 * x_1).imK = QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) 0
⊢ 0 * x_1 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x_1).re = re (a := c₁) (b := c₂) (c := c₃) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x_1).imI = imI (a := c₁) (b := c₂) (c := c₃) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x_1).imJ = imJ (a := c₁) (b := c₂) (c := c₃) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ (0 * x_1).imK = imK (a := c₁) (b := c₂) (c := c₃) 0

Tactic:
simp