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_1 y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).imK =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
        (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
              (a : S) → ℍ[R,c₁,c₂,c₃])
            s :
          ℍ[R,c₁,c₂,c₃])
        x).imK

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) r : ℍ[R,c₁,c₂,c₃])
    ({ re := r, imI := 0, imJ := 0, imK := 0 } : ℍ[R,c₁,c₂,c₃])

Tactic:
rfl

Premises used: QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
x x_1 : R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) x : ℍ[R,c₁,c₂,c₃])
      ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) x_1 : ℍ[R,c₁,c₂,c₃]) →
    x = x_1

Tactic:
simp [algebraMap_eq]

Premises used: QuaternionAlgebra.algebraMap_eq
-- 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
⊢ IsTorsionFree R ℍ[R,c₁,c₂,c₃]

Tactic:
(addEquivProd ..).injective.moduleIsTorsionFree _ fun _ _ ↦ rfl

Premises used: AddEquiv.injective, QuaternionAlgebra.addEquivProd, Function.Injective.moduleIsTorsionFree, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
⊢ Eq (α := (a : ℍ[R,c₁,c₂,c₃]) → Fin 4 → R) (⇑(linearEquivTuple c₁ c₂ c₃) : (a : ℍ[R,c₁,c₂,c₃]) → Fin 4 → R)
    (⇑(equivTuple c₁ c₂ c₃) : (a : ℍ[R,c₁,c₂,c₃]) → Fin 4 → R)

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
⊢ Eq (α := (a : Fin 4 → R) → ℍ[R,c₁,c₂,c₃])
    (⇑(LinearEquiv.symm (linearEquivTuple c₁ c₂ c₃)) : (a : Fin 4 → R) → ℍ[R,c₁,c₂,c₃])
    (⇑(equivTuple c₁ c₂ c₃).symm : (a : Fin 4 → R) → ℍ[R,c₁,c₂,c₃])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
q : ℍ[R,c₁,c₂,c₃]
⊢ (⇑((Basis.repr (basisOneIJK c₁ c₂ c₃) : (a : ℍ[R,c₁,c₂,c₃]) → Fin 4 →₀ R) q : Fin 4 →₀ R) : (a : Fin 4) → R) =
    ![q.re, q.imI, q.imJ, q.imK]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, 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
⊢ Module.Finite R ℍ[R,c₁,c₂,c₃]

Tactic:
.of_basis (basisOneIJK c₁ c₂ c₃)

Premises used: Module.Finite.of_basis, QuaternionAlgebra.basisOneIJK
-- 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
⊢ Free R ℍ[R,c₁,c₂,c₃]

Tactic:
.of_basis (basisOneIJK c₁ c₂ c₃)

Premises used: Module.Free.of_basis, QuaternionAlgebra.basisOneIJK
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
rw : Eq.{u_3 + 2} (α := Cardinal.{u_3}) (↑4 : Cardinal.{u_3}) 4
⊢ Module.rank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
rw [rank_eq_card_basis (basisOneIJK c₁ c₂ c₃), Fintype.card_fin]

Premises used: Fintype.card_fin, rank_eq_card_basis, QuaternionAlgebra.basisOneIJK
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
⊢ Eq.{u_3 + 2} (α := Cardinal.{u_3}) (↑4 : Cardinal.{u_3}) 4

Tactic:
norm_num
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
rw : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) (Module.rank R ℍ[R,c₁,c₂,c₃]) : ℕ) (4 : ℕ)
rw₁ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) 4 : ℕ) (4 : ℕ)
rw₂ rw₃ : Eq (α := ℕ) 4 4
⊢ finrank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]

Premises used: Cardinal.toNat_ofNat, QuaternionAlgebra.rank_eq_four, Module.finrank
-- 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₃]
⊢ (fun (t : ℍ[R,c₃,c₁]) ↦ ({ re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK } : ℍ[R,c₁,c₃]))
      ((fun (t : ℍ[R,c₁,c₃]) ↦ ({ re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK } : ℍ[R,c₃,c₁])) x_1) =
    x_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 : CommRing R
x_1 : ℍ[R,c₃,c₁]
⊢ (fun (t : ℍ[R,c₁,c₃]) ↦ ({ re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK } : ℍ[R,c₃,c₁]))
      ((fun (t : ℍ[R,c₃,c₁]) ↦ ({ re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK } : ℍ[R,c₁,c₃])) x_1) =
    x_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 : CommRing R
x_1 x_2 : ℍ[R,c₁,c₃]
re :
  QuaternionAlgebra.re (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).re
imI :
  QuaternionAlgebra.imI (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imI
imJ :
  QuaternionAlgebra.imJ (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imJ
imK :
  QuaternionAlgebra.imK (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imK
⊢ { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK } =
    HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
      { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }

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 : ℍ[R,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.imK * x_2.imK =
    x_1.re * x_2.re + c₃ * x_1.imJ * x_2.imJ + c₁ * x_1.imI * x_2.imI - c₃ * c₁ * x_1.imK * x_2.imK
⊢ QuaternionAlgebra.re (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).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 : ℍ[R,c₁,c₃]
imI :
  x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re - c₁ * x_1.imK * x_2.imI =
    x_1.re * x_2.imJ + x_1.imJ * x_2.re + c₁ * x_1.imI * x_2.imK + -(c₁ * x_1.imK * x_2.imI)
⊢ QuaternionAlgebra.imI (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).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 : ℍ[R,c₁,c₃]
imJ :
  x_1.re * x_2.imI + x_1.imI * x_2.re - c₃ * x_1.imJ * x_2.imK =
    x_1.re * x_2.imI + -(c₃ * x_1.imJ * x_2.imK) + x_1.imI * x_2.re
⊢ QuaternionAlgebra.imJ (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).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 : ℍ[R,c₁,c₃]
imK :
  -(x_1.imK * x_2.re) + (x_1.imJ * x_2.imI - (x_1.re * x_2.imK + x_1.imI * x_2.imJ)) =
    -(x_1.re * x_2.imK) + x_1.imJ * x_2.imI - x_1.imI * x_2.imJ + -(x_1.imK * x_2.re)
⊢ QuaternionAlgebra.imK (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK : ℍ[R,c₃,c₁] } =
    (HMul.hMul (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).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 : ℍ[R,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.imK * x_2.imK =
    x_1.re * x_2.re + c₃ * x_1.imJ * x_2.imJ + c₁ * x_1.imI * x_2.imI - c₃ * c₁ * x_1.imK * x_2.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 x_2 : ℍ[R,c₁,c₃]
⊢ x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re - c₁ * x_1.imK * x_2.imI =
    x_1.re * x_2.imJ + x_1.imJ * x_2.re + c₁ * x_1.imI * x_2.imK + -(c₁ * x_1.imK * x_2.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 : ℍ[R,c₁,c₃]
⊢ x_1.re * x_2.imI + x_1.imI * x_2.re - c₃ * x_1.imJ * x_2.imK =
    x_1.re * x_2.imI + -(c₃ * x_1.imJ * x_2.imK) + x_1.imI * x_2.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 : ℍ[R,c₁,c₃]
⊢ -(x_1.imK * x_2.re) + (x_1.imJ * x_2.imI - (x_1.re * x_2.imK + x_1.imI * x_2.imJ)) =
    -(x_1.re * x_2.imK) + x_1.imJ * x_2.imI - x_1.imI * x_2.imJ + -(x_1.imK * x_2.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 : ℍ[R,c₁,c₃]
re :
  QuaternionAlgebra.re (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).re
imI :
  QuaternionAlgebra.imI (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imI
imJ :
  QuaternionAlgebra.imJ (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imJ
imK :
  QuaternionAlgebra.imK (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imK
⊢ { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK } =
    HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
      { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }

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 : ℍ[R,c₁,c₃]
⊢ re (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).re

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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 : ℍ[R,c₁,c₃]
⊢ imI (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imI

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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 : ℍ[R,c₁,c₃]
⊢ imJ (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imJ

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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 : ℍ[R,c₁,c₃]
⊢ imK (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imK

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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
⊢ Eq (α := ℍ[R,c₃,c₁])
    ({ re := re (a := c₁) (b := 0) ((algebraMap R ℍ[R,c₁,c₃] : (a : R) → ℍ[R,c₁,c₃]) x_1),
        imI := imJ (a := c₁) (b := 0) ((algebraMap R ℍ[R,c₁,c₃] : (a : R) → ℍ[R,c₁,c₃]) x_1),
        imJ := imI (a := c₁) (b := 0) ((algebraMap R ℍ[R,c₁,c₃] : (a : R) → ℍ[R,c₁,c₃]) x_1),
        imK := -imK (a := c₁) (b := 0) ((algebraMap R ℍ[R,c₁,c₃] : (a : R) → ℍ[R,c₁,c₃]) x_1) } :
      ℍ[R,c₃,c₁])
    ((algebraMap R ℍ[R,c₃,c₁] : (a : R) → ℍ[R,c₃,c₁]) x_1 : ℍ[R,c₃,c₁])

Tactic:
simp [algebraMap_eq]

Premises used: QuaternionAlgebra.algebraMap_eq
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
⊢ (↑(x - y) : ℍ[R,c₁,c₂,c₃]) = HSub.hSub (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])

Tactic:
(algebraMap R ℍ[R,c₁,c₂,c₃]).map_sub x y

Premises used: Algebra.algebraMap, QuaternionAlgebra, RingHom.map_sub, QuaternionAlgebra.coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
n : ℕ
⊢ (↑(x ^ n) : ℍ[R,c₁,c₂,c₃]) = HPow.hPow (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) n

Tactic:
(algebraMap R ℍ[R,c₁,c₂,c₃]).map_pow x n

Premises used: Algebra.algebraMap, QuaternionAlgebra, QuaternionAlgebra.coe, RingHom.map_pow
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * a = a * (↑r : ℍ[R,c₁,c₂,c₃])

Tactic:
Algebra.commutes r a

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ Commute (↑r : ℍ[R,c₁,c₂,c₃]) a

Tactic:
coe_commutes r a

Premises used: SemiconjBy, Commute, QuaternionAlgebra.coe_commutes
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * a = r • a

Tactic:
(Algebra.smul_def r a).symm

Premises used: Algebra.smul_def, Eq.symm
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw : (↑r : ℍ[R,c₁,c₂,c₃]) * a = r • a
rw₁ rw₂ : r • a = r • a
⊢ a * (↑r : ℍ[R,c₁,c₂,c₃]) = r • a

Tactic:
rw [← coe_commutes, coe_mul_eq_smul]

Premises used: QuaternionAlgebra.coe_mul_eq_smul, QuaternionAlgebra.coe_commutes
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
⊢ Eq (α := (a : R) → ℍ[R,c₁,c₂,c₃]) (⇑(algebraMap R ℍ[R,c₁,c₂,c₃]) : (a : R) → ℍ[R,c₁,c₂,c₃]) coe

Tactic:
rfl

Premises used: QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
rw :
  HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃]) =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])
rw₁ rw₂ :
  HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃]) = HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃])
⊢ HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃]) = (↑(x * y) : ℍ[R,c₁,c₂,c₃])

Tactic:
rw [coe_mul, coe_mul_eq_smul]

Premises used: QuaternionAlgebra.coe_mul_eq_smul, QuaternionAlgebra.coe_mul
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a).re = a.re + c₂ * a.imI

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a).imI = -a.imI

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a).imJ = -a.imJ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a).imK = -a.imK

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a).im = -a.im

Tactic:
QuaternionAlgebra.ext neg_zero.symm rfl rfl rfl

Premises used: QuaternionAlgebra.ext, Eq.symm, neg_zero, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
a₁ a₂ a₃ a₄ : R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (star { re := a₁, imI := a₂, imJ := a₃, imK := a₄ })
    { re := a₁ + c₂ * a₂, imI := -a₂, imJ := -a₃, imK := -a₄ }

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_1 y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x : ℍ[R,c₁,c₂,c₃]
⊢ star (star x) = x

Tactic:
simp [Star.star]

Premises used: Star.star
-- 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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a * b)).re = (star b * star a).re
imI : (star (a * b)).imI = (star b * star a).imI
imJ : (star (a * b)).imJ = (star b * star a).imJ
imK : (star (a * b)).imK = (star b * star a).imK
⊢ star (a * b) = star b * star a

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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re :
  a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.imK
⊢ (star (a * b)).re = (star b * star a).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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
imI :
  -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.imJ
⊢ (star (a * b)).imI = (star b * star a).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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
imJ :
  c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.imI
⊢ (star (a * b)).imJ = (star b * star a).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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
imK :
  -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))
⊢ (star (a * b)).imK = (star b * star a).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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.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_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))

Tactic:
ring