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

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

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (a + star a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
imI : (a + star a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
imJ : (a + star a).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
imK : (a + star a).imK = QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
⊢ a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI
⊢ (a + star a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])

Tactic:
simp [two_mul]

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

Tactic:
simp [two_mul]

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

Tactic:
simp [two_mul]

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

Tactic:
simp [two_mul]

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

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ a + star a =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])

Tactic:
simp [self_add_star']

Premises used: QuaternionAlgebra.self_add_star'
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw : a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
rw₁ rw₂ : Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
⊢ star a + a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])

Tactic:
rw [add_comm, self_add_star']

Premises used: add_comm, QuaternionAlgebra.self_add_star'
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw :
  a + star a =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
rw₁ rw₂ :
  HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃]) =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
⊢ star a + a =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])

Tactic:
rw [add_comm, self_add_star]

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

Tactic:
eq_sub_iff_add_eq.2 a.star_add_self'

Premises used: Iff.mpr, eq_sub_iff_add_eq, QuaternionAlgebra.star_add_self'
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
re : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).re = (x * (↑r : ℍ[R,c₁,c₂,c₃])).re
imI : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imI = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imI
imJ : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imJ = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imJ
imK : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imK = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imK
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * x = x * (↑r : ℍ[R,c₁,c₂,c₃])

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ((↑r : ℍ[R,c₁,c₂,c₃]) * x).re = (x * (↑r : ℍ[R,c₁,c₂,c₃])).re

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imI = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imI

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imJ = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imJ

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imK = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imK

Tactic:
simp [mul_comm]

Premises used: mul_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
rw : ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)
⊢ Commute (star a) a

Tactic:
rw [commute_iff_eq, a.star_eq_two_re_sub]

Premises used: QuaternionAlgebra.star_eq_two_re_sub, commute_iff_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
re :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).re
imI :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imI =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imI
imJ :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imJ =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imJ
imK :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imK =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imK
⊢ ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - 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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.re)
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - 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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
imI :
  (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imI =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - 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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
imJ :
  (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imJ =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - 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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
imK :
  (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imK =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - 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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
imI :
  QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
imJ :
  QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
imK :
  QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (star (↑x : ℍ[R,c₁,c₂,c₃])) (↑x : ℍ[R,c₁,c₂,c₃])

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
⊢ re (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
⊢ imI (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = imI (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
⊢ imJ (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = imJ (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
⊢ imK (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = imK (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (star a.im).re = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).re
imI : (star a.im).imI = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imI
imJ : (star a.im).imJ = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imJ
imK : (star a.im).imK = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imK
⊢ star a.im = -a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a.im).re = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a.im).imI = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a.im).imJ = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a.im).imK = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imK

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : SMulCommClass S R R
s : S
a : ℍ[R,c₁,c₂,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
simp [mul_smul_comm]

Premises used: mul_smul_comm
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
c₁ c₃ : R
inst : CommRing R
inst_1 : Monoid S
inst_2 : DistribMulAction S R
s : S
a : ℍ[R,c₁,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
a : ℍ[R,c₁,c₂,c₃]
x : R
h : a = (↑x : ℍ[R,c₁,c₂,c₃])
rw :
  Eq (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃])
    (↑(re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])) : ℍ[R,c₁,c₂,c₃])
rw₁ rw₂ : Eq (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃])
⊢ a = (↑a.re : ℍ[R,c₁,c₂,c₃])

Tactic:
rw [h, re_coe]

Premises used: QuaternionAlgebra.re_coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
a : ℍ[R,c₁,c₂,c₃]
⊢ a = (↑a.re : ℍ[R,c₁,c₂,c₃]) ↔ Membership.mem (γ := Set ℍ[R,c₁,c₂,c₃]) (Set.range coe) a

Tactic:
⟨fun h => ⟨a.re, h.symm⟩, fun ⟨_, h⟩ => eq_re_of_eq_coe h.symm⟩

Premises used: QuaternionAlgebra.re, _private.0.QuaternionAlgebra.eq_re_iff_mem_range_coe.match_1, QuaternionAlgebra.coe, Iff.intro, Exists.intro, QuaternionAlgebra.eq_re_of_eq_coe, Eq.symm, Eq
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₃ : R
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
c₁ c₂ : R
a : ℍ[R,c₁,c₂,c₃]
⊢ star a = a ↔ a = (↑a.re : ℍ[R,c₁,c₂,c₃])

Tactic:
simp_all [QuaternionAlgebra.ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]

Premises used: neg_eq_iff_add_eq_zero, add_self_eq_zero, QuaternionAlgebra.ext_iff
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₃ : R
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
c₁ : R
a : ℍ[R,c₁,c₃]
⊢ star a = -a ↔ a.re = 0

Tactic:
simp [QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero]

Premises used: QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (star a * a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
imI : (star a * a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
imJ : (star a * a).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
imK : (star a * a).imK = QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
⊢ star a * a = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (star a * a).re = re (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
imI :
  (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0
⊢ (star a * a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
imJ :
  (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0
⊢ (star a * a).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
imK : (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0
⊢ (star a * a).imK = QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw : star a * a = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
⊢ a * star a = (↑(a * star a).re : ℍ[R,c₁,c₂,c₃])

Tactic:
rw [← star_comm_self']

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

Tactic:
a.star_mul_eq_coe

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

Tactic:
exact a.star_mul_eq_coe

Premises used: QuaternionAlgebra.star_mul_eq_coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x_1 y_1 : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x y : ℍ[R,c₁,c₂,c₃]
⊢ (op ∘ star) (x * y) = (op ∘ star) x * (op ∘ star) y

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r_1 x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
r : R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ) ((op ∘ star) ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) r) : ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ)
    ((algebraMap R ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ : (a : R) → ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ) r : ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ)

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := (a : ℍ[R,c₁,c₂,c₃]) → ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ) (⇑starAe : (a : ℍ[R,c₁,c₂,c₃]) → ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ)
    (op ∘ star)

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
x : ℍ[R]
⊢ (equivTuple R : (a : ℍ[R]) → Fin 4 → R) x = ![x.re, x.imI, x.imJ, x.imK]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
inst_3 : Subsingleton R
⊢ Subsingleton.{u_1 + 1} ℍ[R]

Tactic:
inferInstanceAs <| Subsingleton <| ℍ[R,-1,0,-1]

Premises used: _private.0.instSubsingletonQuaternion._proof_1
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
inst_3 : Nontrivial R
⊢ Nontrivial.{u_1} ℍ[R]

Tactic:
inferInstanceAs <| Nontrivial <| ℍ[R,-1,0,-1]

Premises used: _private.0.instNontrivialQuaternion._proof_1
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
inst : CommRing R
r x y : R
a b : ℍ[R]
inst_1 : SMul S T
inst_2 : SMul S R
inst_3 : SMul T R
inst_4 : IsScalarTower S T R
⊢ IsScalarTower.{u_1, u_2, u_3} S T ℍ[R]

Tactic:
inferInstanceAs <| IsScalarTower S T ℍ[R,-1,0,-1]

Premises used: _private.0.Quaternion.instIsScalarTower._proof_1
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
inst : CommRing R
r x y : R
a b : ℍ[R]
inst_1 : SMul S R
inst_2 : SMul T R
inst_3 : SMulCommClass S T R
⊢ SMulCommClass.{u_1, u_2, u_3} S T ℍ[R]

Tactic:
inferInstanceAs <| SMulCommClass S T ℍ[R,-1,0,-1]

Premises used: _private.0.Quaternion.instSMulCommClass._proof_1
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
inst : CommRing R
r x y : R
a b : ℍ[R]
⊢ IsStarNormal a

Tactic:
inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,0,-1]) a

Premises used: _private.0.Quaternion.instIsStarNormal._proof_1
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b

Tactic:
QuaternionAlgebra.ext

Premises used: QuaternionAlgebra.ext, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a.im.re = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a.im.imI = a.imI

Tactic:
rfl

Premises used: rfl, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a.im.imJ = a.imJ

Tactic:
rfl

Premises used: rfl, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a.im.imK = a.imK

Tactic:
rfl

Premises used: rfl, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a.im.im = a.im

Tactic:
rfl

Premises used: Quaternion.im, QuaternionAlgebra.im, rfl, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (↑a.re : ℍ[R]) + a.im = a

Tactic:
QuaternionAlgebra.re_add_im a

Premises used: QuaternionAlgebra.re_add_im, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a - a.im = (↑a.re : ℍ[R])

Tactic:
QuaternionAlgebra.sub_im_self a

Premises used: Quaternion.coe, QuaternionAlgebra.sub_im_self, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a - (↑a.re : ℍ[R]) = a.im

Tactic:
QuaternionAlgebra.sub_re_self a

Premises used: QuaternionAlgebra.sub_re_self, Quaternion.im, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ QuaternionAlgebra.re (a := -1) (↑x : ℍ[R]) = x

Tactic:
rfl

Premises used: rfl