awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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 : ℍ[R,c₁,c₃]
re :
  QuaternionAlgebra.re (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).re
imI :
  QuaternionAlgebra.imI (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imI
imJ :
  QuaternionAlgebra.imJ (a := c₃) (b := 0) (c := c₁)
      { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
    (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
        { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imJ
⊢ { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK } =
    HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
      { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }
have imK : imK (a := c₃) (b := 0) (c := c₁)
    { re := (x_1 + x_2).re, imI := (x_1 + x_2).imJ, imJ := (x_1 + x_2).imI, imK := -(x_1 + x_2).imK : ℍ[R,c₃,c₁] } =
  (HAdd.hAdd (α := ℍ[R,c₃,c₁]) { re := x_1.re, imI := x_1.imJ, imJ := x_1.imI, imK := -x_1.imK : ℍ[R,c₃,c₁] }
      { re := x_2.re, imI := x_2.imJ, imJ := x_2.imI, imK := -x_2.imK : ℍ[R,c₃,c₁] }).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ a * (↑r : ℍ[R,c₁,c₂,c₃]) = r • a
have rw : (↑r : ℍ[R,c₁,c₂,c₃]) * a = r • a
Tactic: rw [← coe_commutes, coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw : (↑r : ℍ[R,c₁,c₂,c₃]) * a = r • a
⊢ a * (↑r : ℍ[R,c₁,c₂,c₃]) = r • a
have rw₁ : r • a = r • a
Tactic: rw [← coe_commutes, coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
⊢ HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃]) = (↑(x * y) : ℍ[R,c₁,c₂,c₃])
have rw : HSMul.hSMul (β := ℍ[R,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₃])
Tactic: rw [coe_mul, coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
rw :
  HSMul.hSMul (β := ℍ[R,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₃])
⊢ HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃]) = (↑(x * y) : ℍ[R,c₁,c₂,c₃])
have rw₁ : HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃]) = HSMul.hSMul (β := ℍ[R,c₁,c₂,c₃]) x (↑y : ℍ[R,c₁,c₂,c₃])
Tactic: rw [coe_mul, coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a * b) = star b * star a
have re : (star (a * b)).re = (star b * star a).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a * b)).re = (star b * star a).re
⊢ star (a * b) = star b * star a
have imI : (star (a * b)).imI = (star b * star a).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a * b)).re = (star b * star a).re
imI : (star (a * b)).imI = (star b * star a).imI
⊢ star (a * b) = star b * star a
have imJ : (star (a * b)).imJ = (star b * star a).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a * b)).re = (star b * star a).re
imI : (star (a * b)).imI = (star b * star a).imI
imJ : (star (a * b)).imJ = (star b * star a).imJ
⊢ star (a * b) = star b * star a
have imK : (star (a * b)).imK = (star b * star a).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).re = (star b * star a).re
have re : a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
    c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
  (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
    c₁ * c₃ * b.imK * a.imK
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imI = (star b * star a).imI
have imI : -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
  -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
    c₃ * b.imK * a.imJ
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imJ = (star b * star a).imJ
have imJ : c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
  -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
    c₁ * b.imK * a.imI
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a * b)).imK = (star b * star a).imK
have imK : -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
  -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a + b) = star a + star b
have re : (star (a + b)).re = (star a + star b).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a + b)).re = (star a + star b).re
⊢ star (a + b) = star a + star b
have imI : (star (a + b)).imI = (star a + star b).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a + b)).re = (star a + star b).re
imI : (star (a + b)).imI = (star a + star b).imI
⊢ star (a + b) = star a + star b
have imJ : (star (a + b)).imJ = (star a + star b).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
re : (star (a + b)).re = (star a + star b).re
imI : (star (a + b)).imI = (star a + star b).imI
imJ : (star (a + b)).imJ = (star a + star b).imJ
⊢ star (a + b) = star a + star b
have imK : (star (a + b)).imK = (star a + star b).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a_1 b_1 : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ (star (a + b)).re = (star a + star b).re
have re : a.re + b.re + c₂ * (a.imI + b.imI) = a.re + c₂ * a.imI + (b.re + c₂ * b.imI)
Tactic: simp [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have re : (a + star a).re = re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (a + star a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
⊢ a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have imI : (a + star a).imI = imI (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (a + star a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
imI : (a + star a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
⊢ a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have imJ : (a + star a).imJ = imJ (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (a + star a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
imI : (a + star a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
imJ : (a + star a).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
⊢ a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have imK : (a + star a).imK = imK (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ (a + star a).re = re (a := c₁) (b := c₂) (c := c₃) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have re : a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI
Tactic: simp [two_mul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ star a + a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have rw : a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
Tactic: rw [add_comm, self_add_star']
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw : a + star a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
⊢ star a + a = (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
have rw₁ : Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) (↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃])
Tactic: rw [add_comm, self_add_star']
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ star a + a =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
have rw : a + star a =
  HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
Tactic: rw [add_comm, self_add_star]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
rw :
  a + star a =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
⊢ star a + a =
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
      HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
have rw₁ : HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃]) =
  HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) 2 (↑a.re : ℍ[R,c₁,c₂,c₃]) +
    HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
Tactic: rw [add_comm, self_add_star]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * x = x * (↑r : ℍ[R,c₁,c₂,c₃])
have re : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).re = (x * (↑r : ℍ[R,c₁,c₂,c₃])).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
re : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).re = (x * (↑r : ℍ[R,c₁,c₂,c₃])).re
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * x = x * (↑r : ℍ[R,c₁,c₂,c₃])
have imI : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imI = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
re : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).re = (x * (↑r : ℍ[R,c₁,c₂,c₃])).re
imI : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imI = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imI
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * x = x * (↑r : ℍ[R,c₁,c₂,c₃])
have imJ : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imJ = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
re : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).re = (x * (↑r : ℍ[R,c₁,c₂,c₃])).re
imI : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imI = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imI
imJ : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imJ = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imJ
⊢ (↑r : ℍ[R,c₁,c₂,c₃]) * x = x * (↑r : ℍ[R,c₁,c₂,c₃])
have imK : ((↑r : ℍ[R,c₁,c₂,c₃]) * x).imK = (x * (↑r : ℍ[R,c₁,c₂,c₃])).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ Commute (star a) a
have rw : ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)
Tactic: rw [commute_iff_eq, a.star_eq_two_re_sub]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)
have re : (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
re :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).re
⊢ ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)
have imI : (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imI = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
re :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).re
imI :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imI =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imI
⊢ ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)
have imJ : (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imJ = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
re :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).re
imI :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imI =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imI
imJ :
  (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imJ =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imJ
⊢ ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a = a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)
have imK : (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imK = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).re = (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).re
have re : (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imI =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imI
have imI : (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imJ =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imJ
have imJ : (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
  -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
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
⊢ (((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a) * a).imK =
    (a * ((↑(2 * a.re + c₂ * a.imI) : ℍ[R,c₁,c₂,c₃]) - a)).imK
have imK : (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
  -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (star (↑x : ℍ[R,c₁,c₂,c₃])) (↑x : ℍ[R,c₁,c₂,c₃])
have re : re (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (star (↑x : ℍ[R,c₁,c₂,c₃])) (↑x : ℍ[R,c₁,c₂,c₃])
have imI : imI (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = imI (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (star (↑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₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (star (↑x : ℍ[R,c₁,c₂,c₃])) (↑x : ℍ[R,c₁,c₂,c₃])
have imJ : imJ (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = imJ (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (star (↑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₃) (star (↑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₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) =
    QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (star (↑x : ℍ[R,c₁,c₂,c₃])) (↑x : ℍ[R,c₁,c₂,c₃])
have imK : imK (a := c₁) (b := c₂) (c := c₃) (star (↑x : ℍ[R,c₁,c₂,c₃])) = imK (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
⊢ star a.im = -a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
have re : (star a.im).re = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (star a.im).re = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).re
⊢ star a.im = -a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
have imI : (star a.im).imI = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (star a.im).re = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).re
imI : (star a.im).imI = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imI
⊢ star a.im = -a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
have imJ : (star a.im).imJ = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
re : (star a.im).re = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).re
imI : (star a.im).imI = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imI
imJ : (star a.im).imJ = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imJ
⊢ star a.im = -a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])
have imK : (star a.im).imK = (-a.im + HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑c₂ : ℍ[R,c₁,c₂,c₃]) (↑a.imI : ℍ[R,c₁,c₂,c₃])).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
a : ℍ[R,c₁,c₂,c₃]
x : R
h : a = (↑x : ℍ[R,c₁,c₂,c₃])
⊢ a = (↑a.re : ℍ[R,c₁,c₂,c₃])
have rw : Eq (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑(re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])) : ℍ[R,c₁,c₂,c₃])
Tactic: rw [h, re_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
a : ℍ[R,c₁,c₂,c₃]
x : R
h : a = (↑x : ℍ[R,c₁,c₂,c₃])
rw :
  Eq (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃])
    (↑(re (a := c₁) (b := c₂) (c := c₃) (↑x : ℍ[R,c₁,c₂,c₃])) : ℍ[R,c₁,c₂,c₃])
⊢ a = (↑a.re : ℍ[R,c₁,c₂,c₃])
have rw₁ : Eq (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃])
Tactic: rw [h, re_coe]