awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
rw : x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
⊢ x • x_1 = (↑x : ℍ[R]) * x_1

Tactic:
rw [← coe_nnratCast, coe_mul_eq_smul]

Premises used: Quaternion.coe_mul_eq_smul, Quaternion.coe_nnratCast
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
a₁ : (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re
a₂ : (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI
a₃ : (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ
a₄ : (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re

Tactic:
NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re

Tactic:
exact NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI

Tactic:
NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI

Tactic:
exact NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ

Tactic:
NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ

Tactic:
exact NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK

Tactic:
NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK

Tactic:
exact NNRat.smul_def ..

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₁ : (↑(HDiv.hDiv (α := R) (↑x.num : R) (↑x.den : R)) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₂ :
  HDiv.hDiv (α := ℍ[R]) (↑(↑x.num : R) : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) =
    HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₃ :
  HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₄ rw₅ : HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])

Tactic:
rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]

Premises used: Quaternion.coe_natCast, Quaternion.coe_ratCast, Quaternion.coe_div, Rat.cast_def, Quaternion.coe_intCast
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
rw : x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
⊢ x • x_1 = (↑x : ℍ[R]) * x_1

Tactic:
rw [← coe_ratCast, coe_mul_eq_smul]

Premises used: Quaternion.coe_ratCast, Quaternion.coe_mul_eq_smul
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
a₁ : (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re
a₂ : (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI
a₃ : (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ
a₄ : (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re

Tactic:
Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re

Tactic:
exact Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI

Tactic:
Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI

Tactic:
exact Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ

Tactic:
Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ

Tactic:
exact Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK

Tactic:
Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ
x_1 : ℍ[R]
⊢ (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK

Tactic:
exact Rat.smul_def ..

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ Eq (α := R) ((normSq : (a : ℍ[R]) → R) a⁻¹ : R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R)

Tactic:
map_inv₀ normSq _

Premises used: Quaternion.normSq, map_inv₀
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
⊢ (normSq : (a : ℍ[R]) → R) (a / b) =
    HDiv.hDiv (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R)

Tactic:
map_div₀ normSq a b

Premises used: Quaternion.normSq, map_div₀
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
z : ℤ
⊢ (normSq : (a : ℍ[R]) → R) (a ^ z) = HPow.hPow (α := R) ((normSq : (a : ℍ[R]) → R) a : R) z

Tactic:
map_zpow₀ normSq a z

Premises used: Quaternion.normSq, map_zpow₀
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
q : ℚ
rw : (↑((normSq : (a : ℍ[R]) → R) (↑(↑q : R) : ℍ[R])) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2
rw₁ : (↑(HPow.hPow (α := R) (β := ℕ) (↑q : R) 2) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2
rw₂ rw₃ : HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2 = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2
⊢ (↑((normSq : (a : ℍ[R]) → R) (↑q : ℍ[R])) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑q : ℍ[R]) 2

Tactic:
rw [← coe_ratCast, normSq_coe, coe_pow]

Premises used: Quaternion.coe_ratCast, Quaternion.coe_pow, Quaternion.normSq_coe
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Infinite R
⊢ LE.le (α := ℕ) 1 4

Tactic:
decide
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
rw : #(R × R × R × R) = HPow.hPow (β := ℕ) (#R) 4
⊢ #ℍ[R,c₁,c₂,c₃] = HPow.hPow (β := ℕ) (#R) 4

Tactic:
rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂ c₃)]

Premises used: QuaternionAlgebra.equivProd, Cardinal.mk_congr
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #R * (#R * (#R * #R)) = HPow.hPow (β := ℕ) (#R) 4

Tactic:
ring
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
inst : Infinite R
rw : HPow.hPow (β := ℕ) (#R) 4 = #R
rw₁ rw₂ : #R = #R
⊢ #ℍ[R,c₁,c₂,c₃] = #R

Tactic:
rw [mk_quaternionAlgebra, pow_four]

Premises used: _private.0.Cardinal.pow_four, Cardinal.mk_quaternionAlgebra
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
rw : #ℍ[R,c₁,c₂,c₃] = HPow.hPow (β := ℕ) (#R) 4
rw₁ rw₂ : HPow.hPow (β := ℕ) (#R) 4 = HPow.hPow (β := ℕ) (#R) 4
⊢ #(↑Set.univ : Type u_1) = HPow.hPow (β := ℕ) (#R) 4

Tactic:
rw [mk_univ, mk_quaternionAlgebra]

Premises used: Cardinal.mk_univ, Cardinal.mk_quaternionAlgebra
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
c₁ c₂ c₃ : R
inst : Infinite R
rw : HPow.hPow (β := ℕ) (#R) 4 = #R
rw₁ rw₂ : #R = #R
⊢ #(↑Set.univ : Type u_1) = #R

Tactic:
rw [mk_univ_quaternionAlgebra, pow_four]

Premises used: _private.0.Cardinal.pow_four, Cardinal.mk_univ_quaternionAlgebra
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
⊢ #ℍ[R] = HPow.hPow (β := ℕ) (#R) 4

Tactic:
mk_quaternionAlgebra _ _ _

Premises used: Quaternion, Cardinal.mk_quaternionAlgebra
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
inst_3 : Infinite R
⊢ #ℍ[R] = #R

Tactic:
mk_quaternionAlgebra_of_infinite _ _ _

Premises used: Cardinal.mk_quaternionAlgebra_of_infinite, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
⊢ #(↑Set.univ : Type u_1) = HPow.hPow (β := ℕ) (#R) 4

Tactic:
mk_univ_quaternionAlgebra _ _ _

Premises used: Cardinal.mk_univ_quaternionAlgebra, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
inst_2 : Neg R
inst_3 : Infinite R
⊢ #(↑Set.univ : Type u_1) = #R

Tactic:
mk_univ_quaternionAlgebra_of_infinite _ _ _

Premises used: Cardinal.mk_univ_quaternionAlgebra_of_infinite, Quaternion
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q₁ q₂ : Basis A c₁ c₂ c₃
hi : q₁.i = q₂.i
hj : q₁.j = q₂.j
mk :
  ∀ (i j k : A) (i_mul_i : i * i = HSMul.hSMul (β := A) c₁ 1 + c₂ • i) (j_mul_j : j * j = HSMul.hSMul (β := A) c₃ 1)
    (i_mul_j : i * j = k) (j_mul_i : j * i = c₂ • j - k)
    (hi :
      { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
            Basis A c₁ c₂ c₃ }.i =
        q₂.i)
    (hj :
      { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
            Basis A c₁ c₂ c₃ }.j =
        q₂.j),
    { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
        Basis A c₁ c₂ c₃ } =
      q₂
⊢ q₁ = q₂

Tactic:
cases q₁
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
q₂ : Basis A c₁ c₂ c₃
i j k : A
i_mul_i : i * i = HSMul.hSMul (β := A) c₁ 1 + c₂ • i
j_mul_j : j * j = HSMul.hSMul (β := A) c₃ 1
i_mul_j : i * j = k
j_mul_i : j * i = c₂ • j - k
hi :
  { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
        Basis A c₁ c₂ c₃ }.i =
    q₂.i
hj :
  { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
        Basis A c₁ c₂ c₃ }.j =
    q₂.j
mk :
  ∀ (i_1 j_1 k_1 : A) (i_mul_i_1 : i_1 * i_1 = HSMul.hSMul (β := A) c₁ 1 + c₂ • i_1)
    (j_mul_j_1 : j_1 * j_1 = HSMul.hSMul (β := A) c₃ 1) (i_mul_j_1 : i_1 * j_1 = k_1)
    (j_mul_i_1 : j_1 * i_1 = c₂ • j_1 - k_1)
    (hi :
      { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
            Basis A c₁ c₂ c₃ }.i =
        { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
            j_mul_i := j_mul_i_1 : Basis A c₁ c₂ c₃ }.i)
    (hj :
      { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
            Basis A c₁ c₂ c₃ }.j =
        { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
            j_mul_i := j_mul_i_1 : Basis A c₁ c₂ c₃ }.j),
    { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
        Basis A c₁ c₂ c₃ } =
      { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
        j_mul_i := j_mul_i_1 }
⊢ { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
      Basis A c₁ c₂ c₃ } =
    q₂

Tactic:
cases q₂
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
i j k : A
i_mul_i : i * i = HSMul.hSMul (β := A) c₁ 1 + c₂ • i
j_mul_j : j * j = HSMul.hSMul (β := A) c₃ 1
i_mul_j : i * j = k
j_mul_i : j * i = c₂ • j - k
i_1 j_1 k_1 : A
i_mul_i_1 : i_1 * i_1 = HSMul.hSMul (β := A) c₁ 1 + c₂ • i_1
j_mul_j_1 : j_1 * j_1 = HSMul.hSMul (β := A) c₃ 1
i_mul_j_1 : i_1 * j_1 = k_1
j_mul_i_1 : j_1 * i_1 = c₂ • j_1 - k_1
hi :
  { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
        Basis A c₁ c₂ c₃ }.i =
    { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
        j_mul_i := j_mul_i_1 : Basis A c₁ c₂ c₃ }.i
hj :
  { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
        Basis A c₁ c₂ c₃ }.j =
    { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
        j_mul_i := j_mul_i_1 : Basis A c₁ c₂ c₃ }.j
⊢ { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i :
      Basis A c₁ c₂ c₃ } =
    { i := i_1, j := j_1, k := k_1, i_mul_i := i_mul_i_1, j_mul_j := j_mul_j_1, i_mul_j := i_mul_j_1,
      j_mul_i := j_mul_i_1 }

Tactic:
grind
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ
imK :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
      HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }

Tactic:
ext
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₁ 1 +
        HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₂ { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).re
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).imI
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).imJ
imK :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).imK
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1

Tactic:
ext
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).re

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).imI

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).imJ

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    (HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1).imK

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
re :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
imI :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imI =
    QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
imJ :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imJ =
    QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
imK :
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).imK =
    QuaternionAlgebra.imK (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
⊢ HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
      { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
ext
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
⊢ (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] }
        { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] }).re =
    re (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
simp