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_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 :
  (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
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 =
    (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
⊢ 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 =
    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' := ⋯ } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
have imJ : (HMul.hMul (α := ℍ[R,c₁,c₂,c₃])
      (({ toFun := fun (s : S) ↦ (↑((algebraMap S R : (a : S) → R) s) : ℍ[R,c₁,c₂,c₃]), map_one' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : 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' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])).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_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 =
    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
have 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' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      x).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_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
⊢ 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
have 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' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      x).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_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
⊢ 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
have 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' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      x).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_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
⊢ 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
have 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' := sorry, map_mul' := sorry,
              map_zero' := sorry, map_add' := sorry : RingHom.{u_1, u_3} S ℍ[R,c₁,c₂,c₃] } :
            (a : S) → ℍ[R,c₁,c₂,c₃])
          s :
        ℍ[R,c₁,c₂,c₃])
      x).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
⊢ Module.rank R ℍ[R,c₁,c₂,c₃] = 4
have rw : Eq.{u_3 + 2} (α := Cardinal.{u_3}) (↑4 : Cardinal.{u_3}) 4
Tactic: rw [rank_eq_card_basis (basisOneIJK c₁ c₂ c₃), Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
⊢ finrank R ℍ[R,c₁,c₂,c₃] = 4
have rw : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) (Module.rank R ℍ[R,c₁,c₂,c₃]) : ℕ) (4 : ℕ)
Tactic: rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
rw : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) (Module.rank R ℍ[R,c₁,c₂,c₃]) : ℕ) (4 : ℕ)
⊢ finrank R ℍ[R,c₁,c₂,c₃] = 4
have rw₁ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) 4 : ℕ) (4 : ℕ)
Tactic: rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ : R
inst : CommRing R
inst_1 : StrongRankCondition R
rw : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) (Module.rank R ℍ[R,c₁,c₂,c₃]) : ℕ) (4 : ℕ)
rw₁ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{u_3}) → ℕ) 4 : ℕ) (4 : ℕ)
⊢ finrank R ℍ[R,c₁,c₂,c₃] = 4
have rw₂ : Eq (α := ℕ) 4 4
Tactic: rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]
-- 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 := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK } =
    HMul.hMul (α := ℍ[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 re : 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₁] } =
  (HMul.hMul (α := ℍ[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
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
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₁] } =
    (HMul.hMul (α := ℍ[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
⊢ { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK } =
    HMul.hMul (α := ℍ[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 imI : 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₁] } =
  (HMul.hMul (α := ℍ[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
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
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₁] } =
    (HMul.hMul (α := ℍ[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₁] } =
    (HMul.hMul (α := ℍ[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
⊢ { re := (x_1 * x_2).re, imI := (x_1 * x_2).imJ, imJ := (x_1 * x_2).imI, imK := -(x_1 * x_2).imK } =
    HMul.hMul (α := ℍ[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 imJ : 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₁] } =
  (HMul.hMul (α := ℍ[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
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
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₁] } =
    (HMul.hMul (α := ℍ[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₁] } =
    (HMul.hMul (α := ℍ[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₁] } =
    (HMul.hMul (α := ℍ[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 } =
    HMul.hMul (α := ℍ[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₁] } =
  (HMul.hMul (α := ℍ[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:
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 (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₁] } =
    (HMul.hMul (α := ℍ[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
have re : x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ - c₁ * c₃ * x_1.imK * x_2.imK =
  x_1.re * x_2.re + c₃ * x_1.imJ * x_2.imJ + c₁ * x_1.imI * x_2.imI - c₃ * c₁ * x_1.imK * x_2.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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 : ℍ[R,c₁,c₃]
⊢ 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₁] } =
    (HMul.hMul (α := ℍ[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
have imI : x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re - c₁ * x_1.imK * x_2.imI =
  x_1.re * x_2.imJ + x_1.imJ * x_2.re + c₁ * x_1.imI * x_2.imK + -(c₁ * x_1.imK * x_2.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 b : ℍ[R,c₁,c₂,c₃]
inst : CommRing R
x_1 x_2 : ℍ[R,c₁,c₃]
⊢ 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₁] } =
    (HMul.hMul (α := ℍ[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
have imJ : x_1.re * x_2.imI + x_1.imI * x_2.re - c₃ * x_1.imJ * x_2.imK =
  x_1.re * x_2.imI + -(c₃ * x_1.imJ * x_2.imK) + x_1.imI * x_2.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
x_1 x_2 : ℍ[R,c₁,c₃]
⊢ 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₁] } =
    (HMul.hMul (α := ℍ[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
have imK : -(x_1.imK * x_2.re) + (x_1.imJ * x_2.imI - (x_1.re * x_2.imK + x_1.imI * x_2.imJ)) =
  -(x_1.re * x_2.imK) + x_1.imJ * x_2.imI - x_1.imI * x_2.imJ + -(x_1.imK * x_2.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
x_1 x_2 : ℍ[R,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 } =
    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 re : 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
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
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
⊢ { 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 imI : 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
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
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
⊢ { 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 imJ : 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
Tactic: ext