awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₃ : (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₄ : (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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 : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₁ : (↑(HDiv.hDiv (α := R) (↑x.num : R) (↑x.den : R)) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₂ : HDiv.hDiv (α := ℍ[R]) (↑(↑x.num : R) : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) =
  HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₃ : HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₄ : HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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 = (↑x : ℍ[R]) * x_1
have rw : x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
Tactic: rw [← coe_ratCast, coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₁ : (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₂ : (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₃ : (x • x_1).imJ = (HSMul.hSMul (α := R) (↑x : R) x_1).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₄ : (x • x_1).imK = (HSMul.hSMul (α := R) (↑x : R) x_1).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
q : ℚ
⊢ (↑((normSq : (a : ℍ[R]) → R) (↑q : ℍ[R])) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑q : ℍ[R]) 2
have rw : (↑((normSq : (a : ℍ[R]) → R) (↑(↑q : R) : ℍ[R])) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2
Tactic: rw [← coe_ratCast, normSq_coe, coe_pow]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ (↑((normSq : (a : ℍ[R]) → R) (↑q : ℍ[R])) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑q : ℍ[R]) 2
have rw₁ : (↑(HPow.hPow (α := R) (β := ℕ) (↑q : R) 2) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2
Tactic: rw [← coe_ratCast, normSq_coe, coe_pow]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ (↑((normSq : (a : ℍ[R]) → R) (↑q : ℍ[R])) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑q : ℍ[R]) 2
have rw₂ : HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2 = HPow.hPow (α := ℍ[R]) (β := ℕ) (↑(↑q : R) : ℍ[R]) 2
Tactic: rw [← coe_ratCast, normSq_coe, coe_pow]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #ℍ[R,c₁,c₂,c₃] = HPow.hPow (β := ℕ) (#R) 4
have rw : #(R × R × R × R) = HPow.hPow (β := ℕ) (#R) 4
Tactic: rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂ c₃)]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
inst : Infinite R
⊢ #ℍ[R,c₁,c₂,c₃] = #R
have rw : HPow.hPow (β := ℕ) (#R) 4 = #R
Tactic: rw [mk_quaternionAlgebra, pow_four]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
inst : Infinite R
rw : HPow.hPow (β := ℕ) (#R) 4 = #R
⊢ #ℍ[R,c₁,c₂,c₃] = #R
have rw₁ : #R = #R
Tactic: rw [mk_quaternionAlgebra, pow_four]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #(↑Set.univ : Type u_1) = HPow.hPow (β := ℕ) (#R) 4
have rw : #ℍ[R,c₁,c₂,c₃] = HPow.hPow (β := ℕ) (#R) 4
Tactic: rw [mk_univ, mk_quaternionAlgebra]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
rw : #ℍ[R,c₁,c₂,c₃] = HPow.hPow (β := ℕ) (#R) 4
⊢ #(↑Set.univ : Type u_1) = HPow.hPow (β := ℕ) (#R) 4
have rw₁ : HPow.hPow (β := ℕ) (#R) 4 = HPow.hPow (β := ℕ) (#R) 4
Tactic: rw [mk_univ, mk_quaternionAlgebra]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
inst : Infinite R
⊢ #(↑Set.univ : Type u_1) = #R
have rw : HPow.hPow (β := ℕ) (#R) 4 = #R
Tactic: rw [mk_univ_quaternionAlgebra, pow_four]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
inst : Infinite R
rw : HPow.hPow (β := ℕ) (#R) 4 = #R
⊢ #(↑Set.univ : Type u_1) = #R
have rw₁ : #R = #R
Tactic: rw [mk_univ_quaternionAlgebra, pow_four]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ q₁ = q₂
have 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₂
Tactic: cases q₁
Cleared hypotheses: q₁, hi, hj
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ { 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₂
have 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 }
Tactic: cases q₂
Cleared hypotheses: q₂, hi, hj
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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₃] } =
    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₃] }
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ 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₃] }
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ 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₃] }
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ 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₃] }
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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₃] } =
    HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) c₃ 1
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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 := 0, imI := 0, imJ := 0, imK := 1 }
have 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 =
  re (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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 }
⊢ 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 }
have 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 =
  imI (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
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 }
⊢ 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 }
have 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 =
  imJ (a := c₁) (b := c₂) (c := c₃) { re := 0, imI := 0, imJ := 0, imK := 1 }
Tactic: ext