awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ QuaternionAlgebra.imI (a := -1) (↑x : ℍ[R]) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ QuaternionAlgebra.imJ (a := -1) (↑x : ℍ[R]) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ QuaternionAlgebra.imK (a := -1) (↑x : ℍ[R]) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ Eq (α := ℍ[R]) (im (↑x : ℍ[R])) 0

Tactic:
rfl

Premises used: Quaternion.im, QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := ℍ[R]) (im 0) 0

Tactic:
rfl

Premises used: Quaternion.im, QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := ℍ[R]) (↑0 : ℍ[R]) 0

Tactic:
rfl

Premises used: Quaternion.coe, QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 1) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 1) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 1) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := ℍ[R]) (im 1) 0

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ (a + b).imJ = a.imJ + b.imJ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ (a + b).imK = a.imK + b.imK

Tactic:
rfl

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

Tactic:
QuaternionAlgebra.im_add a b

Premises used: QuaternionAlgebra.im_add, Quaternion.im, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x y : R
⊢ (↑(x + y) : ℍ[R]) = HAdd.hAdd (α := ℍ[R]) (↑x : ℍ[R]) (↑y : ℍ[R])

Tactic:
QuaternionAlgebra.coe_add x y

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
QuaternionAlgebra.im_neg a

Premises used: Quaternion.im, QuaternionAlgebra.im_neg, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ Eq (α := ℍ[R]) (↑(-x) : ℍ[R]) (-(↑x : ℍ[R]))

Tactic:
QuaternionAlgebra.coe_neg x

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
QuaternionAlgebra.im_sub a b

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

Tactic:
QuaternionAlgebra.coe_sub x y

Premises used: QuaternionAlgebra.coe_sub, Quaternion.coe, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ + HMul.hMul (α := R) 0 (-1) * a.imJ * b.imK -
      HMul.hMul (α := R) (-1) (-1) * a.imK * b.imK =
    a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK

Tactic:
simp [one_mul, neg_mul, sub_eq_add_neg, neg_neg]

Premises used: sub_eq_add_neg, neg_neg, neg_mul, one_mul
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ a.re * b.imI + a.imI * b.re + 0 * a.imI * b.imI - -1 * a.imJ * b.imK + -1 * a.imK * b.imJ =
    a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ a.re * b.imJ + -1 * a.imI * b.imK + a.imJ * b.re + 0 * a.imJ * b.imI - -1 * a.imK * b.imI =
    a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ a.re * b.imK + a.imI * b.imJ + 0 * a.imI * b.imK - a.imJ * b.imI + a.imK * b.re =
    a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x y : R
⊢ (↑(x * y) : ℍ[R]) = HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (↑y : ℍ[R])

Tactic:
QuaternionAlgebra.coe_mul x y

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

Tactic:
QuaternionAlgebra.coe_pow x n

Premises used: Quaternion.coe, QuaternionAlgebra.coe_pow, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
⊢ Eq.{u_3 + 1} (α := R) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) (↑n : ℍ[R])) (↑n : R)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Quaternion.coe, QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := R) (β := ℍ[R]) coe

Tactic:
QuaternionAlgebra.coe_injective

Premises used: Quaternion.coe, Quaternion, QuaternionAlgebra.coe_injective
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x y : R
⊢ Eq (α := ℍ[R]) (↑x : ℍ[R]) (↑y : ℍ[R]) ↔ x = y

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, Quaternion.coe_injective
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
inst : CommRing R
a : ℍ[R]
inst_1 : SMul S R
s : S
⊢ (s • a).re = s • a.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
inst : CommRing R
a : ℍ[R]
inst_1 : SMul S R
s : S
⊢ (s • a).imI = s • a.imI

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
inst : CommRing R
a : ℍ[R]
inst_1 : SMul S R
s : S
⊢ (s • a).imJ = s • a.imJ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
inst : CommRing R
a : ℍ[R]
inst_1 : SMul S R
s : S
⊢ (s • a).imK = s • a.imK

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
inst : CommRing R
a : ℍ[R]
inst_1 : SMulZeroClass S R
s : S
⊢ (s • a).im = s • a.im

Tactic:
QuaternionAlgebra.im_smul a s

Premises used: Quaternion.im, QuaternionAlgebra.im_smul, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : SMulZeroClass S R
s : S
r : R
⊢ (↑(s • r) : ℍ[R]) = HSMul.hSMul (β := ℍ[R]) s (↑r : ℍ[R])

Tactic:
QuaternionAlgebra.coe_smul _ _

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

Tactic:
QuaternionAlgebra.coe_commutes r a

Premises used: QuaternionAlgebra.coe_commutes, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
r : R
a : ℍ[R]
⊢ Commute (↑r : ℍ[R]) a

Tactic:
QuaternionAlgebra.coe_commute r a

Premises used: Quaternion.coe, QuaternionAlgebra.coe_commute, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
r : R
a : ℍ[R]
⊢ (↑r : ℍ[R]) * a = r • a

Tactic:
QuaternionAlgebra.coe_mul_eq_smul r a

Premises used: QuaternionAlgebra.coe_mul_eq_smul, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
r : R
a : ℍ[R]
⊢ a * (↑r : ℍ[R]) = r • a

Tactic:
QuaternionAlgebra.mul_coe_eq_smul r a

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

Tactic:
rfl

Premises used: Quaternion.coe, QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Function.Injective (α := R) (β := ℍ[R]) (⇑(algebraMap R ℍ[R]) : (a : R) → ℍ[R])

Tactic:
QuaternionAlgebra.algebraMap_injective

Premises used: QuaternionAlgebra.algebraMap_injective, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x y : R
⊢ HSMul.hSMul (β := ℍ[R]) x (↑y : ℍ[R]) = (↑(x * y) : ℍ[R])

Tactic:
QuaternionAlgebra.smul_coe x y

Premises used: Quaternion.coe, QuaternionAlgebra.smul_coe, Quaternion
-- 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]
⊢ Module.Finite R ℍ[R]

Tactic:
inferInstanceAs <| Module.Finite R ℍ[R,-1,0,-1]

Premises used: _private.0.Quaternion.instFinite._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]
⊢ Free R ℍ[R]

Tactic:
inferInstanceAs <| Module.Free R ℍ[R,-1,0,-1]

Premises used: _private.0.Quaternion.instFree._proof_1
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
⊢ Module.rank R ℍ[R] = 4

Tactic:
QuaternionAlgebra.rank_eq_four _ _ _

Premises used: QuaternionAlgebra.rank_eq_four, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
inst_1 : StrongRankCondition R
⊢ finrank R ℍ[R] = 4

Tactic:
QuaternionAlgebra.finrank_eq_four _ _ _

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

Tactic:
rw [QuaternionAlgebra.re_star, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, QuaternionAlgebra.re_star, add_zero
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (star a).imI = -a.imI

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
QuaternionAlgebra.im_star a

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

Tactic:
simpa using QuaternionAlgebra.self_add_star' a

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

Tactic:
simpa using QuaternionAlgebra.self_add_star a

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

Tactic:
simpa using QuaternionAlgebra.star_add_self' a

Premises used: QuaternionAlgebra.star_add_self'
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ star a + a = HMul.hMul (α := ℍ[R]) 2 (↑a.re : ℍ[R])

Tactic:
simpa using QuaternionAlgebra.star_add_self a

Premises used: QuaternionAlgebra.star_add_self
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ star a = (↑(2 * a.re) : ℍ[R]) - a

Tactic:
simpa using QuaternionAlgebra.star_eq_two_re_sub a

Premises used: QuaternionAlgebra.star_eq_two_re_sub
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ Eq (α := ℍ[R]) (star (↑x : ℍ[R])) (↑x : ℍ[R])

Tactic:
QuaternionAlgebra.star_coe x

Premises used: Quaternion.coe, QuaternionAlgebra.star_coe, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
a₁ : (star a.im).re = (-a.im).re
a₂ : (star a.im).imI = (-a.im).imI
a₃ : (star a.im).imJ = (-a.im).imJ
a₄ : (star a.im).imK = (-a.im).imK
⊢ star a.im = -a.im

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (star a.im).re = (-a.im).re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (star a.im).imI = (-a.im).imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (star a.im).imJ = (-a.im).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (star a.im).imK = (-a.im).imK

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

Tactic:
QuaternionAlgebra.star_smul' s a

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

Tactic:
QuaternionAlgebra.eq_re_of_eq_coe h

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

Tactic:
QuaternionAlgebra.eq_re_iff_mem_range_coe

Premises used: Quaternion.coe, Set.Mem, QuaternionAlgebra.eq_re_iff_mem_range_coe, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
a : ℍ[R]
⊢ star a = a ↔ a = (↑a.re : ℍ[R])

Tactic:
QuaternionAlgebra.star_eq_self

Premises used: Quaternion.coe, QuaternionAlgebra.star_eq_self, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
a : ℍ[R]
⊢ star a = -a ↔ a.re = 0

Tactic:
QuaternionAlgebra.star_eq_neg

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

Tactic:
QuaternionAlgebra.star_mul_eq_coe a

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

Tactic:
QuaternionAlgebra.mul_star_eq_coe a

Premises used: Quaternion.coe, QuaternionAlgebra.mul_star_eq_coe, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := (a : ℍ[R]) → ℍ[R]ᵐᵒᵖ) (⇑starAe : (a : ℍ[R]) → ℍ[R]ᵐᵒᵖ) (op ∘ star)

Tactic:
rfl

Premises used: rfl, Quaternion, MulOpposite.op
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (normSq : (a : ℍ[R]) → R) a = (a * star a).re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (normSq : (a : ℍ[R]) → R) a =
    HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2

Tactic:
simp only [normSq_def, sq, mul_neg, sub_neg_eq_add, re_mul, re_star, imI_star, imJ_star,
    imK_star]

Premises used: Quaternion.re_star, sq, Quaternion.imI_star, Quaternion.imK_star, Quaternion.normSq_def, Quaternion.imJ_star, Quaternion.re_mul, sub_neg_eq_add, mul_neg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
x : R
rw : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (star (↑x : ℍ[R]))).re = HPow.hPow (β := ℕ) x 2
rw₁ : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (↑x : ℍ[R])).re = HPow.hPow (β := ℕ) x 2
rw₂ : QuaternionAlgebra.re (a := -1) (↑(x * x) : ℍ[R]) = HPow.hPow (β := ℕ) x 2
rw₃ : x * x = HPow.hPow (β := ℕ) x 2
rw₄ rw₅ : x * x = x * x
⊢ (normSq : (a : ℍ[R]) → R) (↑x : ℍ[R]) = HPow.hPow (β := ℕ) x 2

Tactic:
rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]

Premises used: sq, Quaternion.re_coe, Quaternion.coe_mul, Quaternion.normSq_def, Quaternion.star_coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ Eq (α := R) ((normSq : (a : ℍ[R]) → R) (star a) : R) ((normSq : (a : ℍ[R]) → R) a : R)

Tactic:
simp [normSq_def']

Premises used: Quaternion.normSq_def'
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
rw : (normSq : (a : ℍ[R]) → R) (↑(↑n : R) : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
rw₁ rw₂ : HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
⊢ (normSq : (a : ℍ[R]) → R) (↑n : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2

Tactic:
rw [← coe_natCast, normSq_coe]

Premises used: Quaternion.coe_natCast, Quaternion.normSq_coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
z : ℤ
rw : (normSq : (a : ℍ[R]) → R) (↑(↑z : R) : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
rw₁ rw₂ : HPow.hPow (α := R) (β := ℕ) (↑z : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
⊢ (normSq : (a : ℍ[R]) → R) (↑z : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2

Tactic:
rw [← coe_intCast, normSq_coe]

Premises used: Quaternion.coe_intCast, Quaternion.normSq_coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ Eq (α := R) ((normSq : (a : ℍ[R]) → R) (-a) : R) ((normSq : (a : ℍ[R]) → R) a : R)

Tactic:
simp only [normSq_def, star_neg, neg_mul_neg]

Premises used: star_neg, Quaternion.normSq_def, neg_mul_neg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
rw : Eq (α := ℍ[R]) (↑(a * star a).re : ℍ[R]) (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
rw₁ rw₂ : Eq (α := ℍ[R]) (↑(a * star a).re : ℍ[R]) (↑(a * star a).re : ℍ[R])
⊢ a * star a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])

Tactic:
rw [mul_star_eq_coe, normSq_def]

Premises used: Quaternion.mul_star_eq_coe, Quaternion.normSq_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
rw : a * star a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
rw₁ rw₂ :
  Eq (α := ℍ[R]) ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R])
⊢ star a * a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])

Tactic:
rw [star_comm_self, self_mul_star]

Premises used: IsStarNormal.star_comm_self, Quaternion.self_mul_star
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
simp_rw : a.im * a.im = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
simp_rw₁ : a.im * a.im = -(star a.im * a.im)
simp_rw₂ : a.im * a.im = -(-a.im * a.im)
simp_rw₃ : a.im * a.im = - -(a.im * a.im)
⊢ HPow.hPow (β := ℕ) a.im 2 = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])

Tactic:
simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]

Premises used: Quaternion.star_mul_self, neg_neg, sq, Quaternion.star_im, neg_mul
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ (↑((normSq : (a : ℍ[R]) → R) (a + b)) : ℍ[R]) =
    HAdd.hAdd (β := ℍ[R])
      (HAdd.hAdd (α := ℍ[R]) ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) (a * star b) + b * star a)
      ((↑((normSq : (a : ℍ[R]) → R) b) : ℍ[R]) : ℍ[R])

Tactic:
simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]

Premises used: add_mul, add_left_comm, StarAddMonoid.star_add, add_assoc, Quaternion.self_mul_star, mul_add