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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := 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₃])).re
imI :
  QuaternionAlgebra.imI (a := c₁) (b := 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₃])).imI
imJ :
  QuaternionAlgebra.imJ (a := c₁) (b := 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₃])).imJ
imK :
  QuaternionAlgebra.imK (a := c₁) (b := 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₃])).imK
⊢ (↑(x * y) : ℍ[R,c₁,c₂,c₃]) = HMul.hMul (α := ℍ[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 : CommRing R
⊢ re (a := c₁) (b := 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₃])).re

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
⊢ imI (a := c₁) (b := 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₃])).imI

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
⊢ imJ (a := c₁) (b := 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₃])).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
⊢ imK (a := c₁) (b := 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₃])).imK

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(OfNat.ofNat n) : ℍ[R,c₁,c₂,c₃]) (OfNat.ofNat n)

Tactic:
rfl

Premises used: QuaternionAlgebra.coe, 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
inst_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) ((↑((algebraMap S R : (a : S) → R) 1) : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃])
    (1 : ℍ[R,c₁,c₂,c₃])

Tactic:
simp only [map_one, coe_one]

Premises used: map_one, QuaternionAlgebra.coe_one
-- 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
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ (↑((algebraMap S R : (a : S) → R) (x * y)) : ℍ[R,c₁,c₂,c₃]) =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (β := ℍ[R,c₁,c₂,c₃])
      ((↑((algebraMap S R : (a : S) → R) x) : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃])
      ((↑((algebraMap S R : (a : S) → R) y) : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃])

Tactic:
simp only [map_mul, coe_mul]

Premises used: map_mul, QuaternionAlgebra.coe_mul
-- 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
inst_1 : CommSemiring S
inst_2 : Algebra S R
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) ((↑((algebraMap S R : (a : S) → R) 0) : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃])
    (0 : ℍ[R,c₁,c₂,c₃])

Tactic:
simp only [map_zero, coe_zero]

Premises used: map_zero, QuaternionAlgebra.coe_zero
-- 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
inst_1 : CommSemiring S
inst_2 : Algebra S R
x y : S
⊢ (↑((algebraMap S R : (a : S) → R) (x + y)) : ℍ[R,c₁,c₂,c₃]) =
    HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (β := ℍ[R,c₁,c₂,c₃])
      ((↑((algebraMap S R : (a : S) → R) x) : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃])
      ((↑((algebraMap S R : (a : S) → R) y) : ℍ[R,c₁,c₂,c₃]) : ℍ[R,c₁,c₂,c₃])

Tactic:
simp only [map_add, coe_add]

Premises used: QuaternionAlgebra.coe_add, map_add
-- 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₃]
⊢ (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).re =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ 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₃])).re

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- 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₃]
⊢ (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).imI =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ 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₃])).imI

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- 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₃]
⊢ (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).imJ =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ 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₃])).imJ

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- 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₃]
⊢ (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 =
    (HMul.hMul (β := ℍ[R,c₁,c₂,c₃]) x
        (({ 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₃])).imK

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- 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₃]
re :
  (s • x).re =
    (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).re
imI :
  (s • x).imI =
    (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).imI
imJ :
  (s • x).imJ =
    (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).imJ
imK :
  (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
⊢ s • x =
    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' := ⋯ } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      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 : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • x).re =
    (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).re

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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).imI =
    (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).imI

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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).imJ =
    (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).imJ

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def