awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (Nat.succ 3))

Tactic:
rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x) ⟨0, ⋯⟩ =
    x (⟨0, ⋯⟩ : Fin (Nat.succ 3))

Tactic:
rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (equivTuple c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → 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
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
⊢ { re := a.re, imI := a.imI, imJ := a.imJ, imK := 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 y : R
a b : ℍ[R,c₁,c₂,c₃]
inst : Subsingleton R
⊢ Subsingleton.{u_3 + 1} ℍ[R,c₁,c₂,c₃]

Tactic:
(equivTuple c₁ c₂ c₃).subsingleton

Premises used: QuaternionAlgebra.equivTuple, Equiv.subsingleton
-- 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 : Nontrivial R
⊢ Nontrivial.{u_3} ℍ[R,c₁,c₂,c₃]

Tactic:
(equivTuple c₁ c₂ c₃).surjective.nontrivial

Premises used: Function.Surjective.nontrivial, QuaternionAlgebra.equivTuple, Equiv.surjective
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : Zero R
⊢ a.im.re = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : Zero R
⊢ a.im.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 : Zero R
⊢ a.im.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 : Zero R
⊢ a.im.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 : Zero R
⊢ a.im.im = a.im

Tactic:
rfl

Premises used: QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : Zero R
⊢ re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃]) = x

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
fun _ _ h => congr_arg re h

Premises used: QuaternionAlgebra.re, congr_arg, Function.Injective
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : Zero R
x y : R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃]) ↔ x = y

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, QuaternionAlgebra.coe_injective
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : Zero R
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (im 0) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : Zero R
inst_1 : One R
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (im 1) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : Add R
a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R
⊢ HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) { re := a₁, imI := a₂, imJ := a₃, imK := a₄ : ℍ[R,c₁,c₂,c₃] }
      { re := b₁, imI := b₂, imJ := b₃, imK := b₄ : ℍ[R,c₁,c₂,c₃] } =
    { re := a₁ + b₁, imI := a₂ + b₂, imJ := a₃ + b₃, imK := a₄ + b₄ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : Add R
c₁ c₂ c₃ : R
⊢ Eq (α := (a : ℍ[R,c₁,c₂,c₃]) → Fin 4 → R) (⇑(addEquivTuple 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: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : Add R
c₁ c₂ c₃ : R
⊢ Eq (α := (a : Fin 4 → R) → ℍ[R,c₁,c₂,c₃])
    (⇑(AddEquiv.symm (addEquivTuple 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: QuaternionAlgebra.equivTuple, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : Add R
c₁ c₂ c₃ : R
⊢ Eq (α := (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (⇑(addEquivProd c₁ c₂ c₃) : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R)
    (⇑(equivProd c₁ c₂ c₃) : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : Add R
c₁ c₂ c₃ : R
⊢ Eq (α := (a : R × R × R × R) → ℍ[R,c₁,c₂,c₃])
    (⇑(AddEquiv.symm (addEquivProd c₁ c₂ c₃)) : (a : R × R × R × R) → ℍ[R,c₁,c₂,c₃])
    (⇑(equivProd c₁ c₂ c₃).symm : (a : R × R × R × R) → ℍ[R,c₁,c₂,c₃])

Tactic:
rfl

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

Tactic:
QuaternionAlgebra.ext (zero_add _).symm rfl rfl rfl

Premises used: QuaternionAlgebra.ext, zero_add, Eq.symm, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : AddZeroClass R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re
imI :
  QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imI
imJ :
  QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imJ
imK :
  QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imK
⊢ (↑(x + y) : ℍ[R,c₁,c₂,c₃]) = HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : AddZeroClass R
⊢ re (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : AddZeroClass R
⊢ imI (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : AddZeroClass R
⊢ imJ (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : AddZeroClass R
⊢ imK (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imK

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : Neg R
a₁ a₂ a₃ a₄ : R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (-{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ })
    { re := -a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : AddGroup R
⊢ (-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₃ x : R
inst : AddGroup R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(-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₃) (↑(-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₃) (↑(-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₃) (↑(-x) : ℍ[R,c₁,c₂,c₃]) =
    QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) (-(↑x : ℍ[R,c₁,c₂,c₃]))
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(-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 : AddGroup R
⊢ re (a := c₁) (b := c₂) (c := c₃) (↑(-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 : AddGroup R
⊢ imI (a := c₁) (b := c₂) (c := c₃) (↑(-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 : AddGroup R
⊢ imJ (a := c₁) (b := c₂) (c := c₃) (↑(-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 : AddGroup R
⊢ imK (a := c₁) (b := c₂) (c := c₃) (↑(-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 b : ℍ[R,c₁,c₂,c₃]
inst : AddGroup R
⊢ (a - b).im = a.im - b.im

Tactic:
QuaternionAlgebra.ext (sub_zero _).symm rfl rfl rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : AddGroup R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (im (↑x : ℍ[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
a : ℍ[R,c₁,c₂,c₃]
inst : AddGroup R
⊢ (↑a.re : ℍ[R,c₁,c₂,c₃]) + a.im = a

Tactic:
QuaternionAlgebra.ext (add_zero _) (zero_add _) (zero_add _) (zero_add _)

Premises used: QuaternionAlgebra.ext, zero_add, add_zero
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : AddGroup R
⊢ a - a.im = (↑a.re : ℍ[R,c₁,c₂,c₃])

Tactic:
QuaternionAlgebra.ext (sub_zero _) (sub_self _) (sub_self _) (sub_self _)

Premises used: sub_self, sub_zero, QuaternionAlgebra.ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : AddGroup R
⊢ a - (↑a.re : ℍ[R,c₁,c₂,c₃]) = a.im

Tactic:
QuaternionAlgebra.ext (sub_self _) (sub_zero _) (sub_zero _) (sub_zero _)

Premises used: sub_self, sub_zero, QuaternionAlgebra.ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : Ring R
a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := a₁, imI := a₂, imJ := a₃, imK := a₄ : ℍ[R,c₁,c₂,c₃] }
      { re := b₁, imI := b₂, imJ := b₃, imK := b₄ : ℍ[R,c₁,c₂,c₃] } =
    { re := a₁ * b₁ + c₁ * a₂ * b₂ + c₃ * a₃ * b₃ + c₂ * c₃ * a₃ * b₄ - c₁ * c₃ * a₄ * b₄,
      imI := a₁ * b₂ + a₂ * b₁ + c₂ * a₂ * b₂ - c₃ * a₃ * b₄ + c₃ * a₄ * b₃,
      imJ := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ + c₂ * a₃ * b₂ - c₁ * a₄ * b₂,
      imK := a₁ * b₄ + a₂ * b₃ + c₂ * a₂ * b₄ - a₃ * b₂ + a₄ * b₁ }

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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : ((s • t) • x).re = (s • t • x).re
imI : ((s • t) • x).imI = (s • t • x).imI
imJ : ((s • t) • x).imJ = (s • t • x).imJ
imK : ((s • t) • x).imK = (s • t • x).imK
⊢ (s • t) • x = s • t • x

Tactic:
ext
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).re = (s • t • x).re

Tactic:
smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).re = (s • t • x).re

Tactic:
exact smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imI = (s • t • x).imI

Tactic:
smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imI = (s • t • x).imI

Tactic:
exact smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imJ = (s • t • x).imJ

Tactic:
smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imJ = (s • t • x).imJ

Tactic:
exact smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imK = (s • t • x).imK

Tactic:
smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imK = (s • t • x).imK

Tactic:
exact smul_assoc _ _ _

Premises used: smul_assoc
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : (s • t • x).re = (t • s • x).re
imI : (s • t • x).imI = (t • s • x).imI
imJ : (s • t • x).imJ = (t • s • x).imJ
imK : (s • t • x).imK = (t • s • x).imK
⊢ s • t • x = t • s • x

Tactic:
ext
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).re = (t • s • x).re

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).re = (t • s • x).re

Tactic:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imI = (t • s • x).imI

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imI = (t • s • x).imI

Tactic:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imJ = (t • s • x).imJ

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imJ = (t • s • x).imJ

Tactic:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imK = (t • s • x).imK

Tactic:
smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t • x).imK = (t • s • x).imK

Tactic:
exact smul_comm _ _ _

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
S : Type u_4
inst : CommRing R
inst_1 : SMulZeroClass S R
s : S
⊢ (s • a).im = s • a.im

Tactic:
QuaternionAlgebra.ext (smul_zero s).symm rfl rfl rfl

Premises used: smul_zero, QuaternionAlgebra.ext, Eq.symm, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
c₁ c₂ c₃ : R
inst : SMul S R
s : S
re im_i im_j im_k : R
⊢ HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) s { re := re, imI := im_i, imJ := im_j, imK := im_k : ℍ[R,c₁,c₂,c₃] } =
    { re := s • re, imI := s • im_i, imJ := s • im_j, imK := s • im_k }

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 : AddCommGroup R
zero :
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)
add :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x + y) =
      HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
neg :
  ∀ (x : ℍ[R,c₁,c₂,c₃]),
    Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (-x) : R × R × R × R)
      (-(equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
sub :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x - y) =
      HSub.hSub (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
nsmul :
  ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℕ),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x) =
      HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
zsmul :
  ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℤ),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x) =
      HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]

Tactic:
apply (equivProd c₁ c₂ c₃).injective.addCommGroup

Premises used: Function.Injective.addCommGroup, QuaternionAlgebra.equivProd, Equiv.injective
-- 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 : AddCommGroup R
⊢ Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)

Tactic:
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 : AddCommGroup R
x_1 y_1 : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x_1 + y_1) =
    HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x_1 : R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y_1 : R × R × R × R)

Tactic:
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 : AddCommGroup R
x_1 : ℍ[R,c₁,c₂,c₃]
⊢ Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (-x_1) : R × R × R × R)
    (-(equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x_1 : R × R × R × R)

Tactic:
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 : AddCommGroup R
x_1 y_1 : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x_1 - y_1) =
    HSub.hSub (α := R × R × R × R) (β := R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x_1 : R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y_1 : R × R × R × R)

Tactic:
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 : AddCommGroup R
x_1 : ℍ[R,c₁,c₂,c₃]
n : ℕ
⊢ (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x_1) =
    HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x_1 : R × R × R × R)

Tactic:
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 : AddCommGroup R
x_1 : ℍ[R,c₁,c₂,c₃]
n : ℤ
⊢ (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x_1) =
    HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x_1 : R × R × R × R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
S : Type u_1
R : Type u_3
c₁ c₂ c₃ : R
inst : Zero R
inst_1 : SMulZeroClass S R
s : S
r : R
⊢ (↑(s • r) : ℍ[R,c₁,c₂,c₃]) = HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) s (↑r : ℍ[R,c₁,c₂,c₃])

Tactic:
QuaternionAlgebra.ext rfl (smul_zero _).symm (smul_zero _).symm (smul_zero _).symm

Premises used: smul_zero, QuaternionAlgebra.ext, Eq.symm, rfl