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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * x_2 * x_3).imJ = (x_1 * (x_2 * x_3)).imJ
have imJ : (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
              c₁ * c₃ * x_1.imK * x_2.imK) *
            x_3.imJ +
          c₁ *
              (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
                c₃ * x_1.imK * x_2.imJ) *
            x_3.imK +
        (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
            c₁ * x_1.imK * x_2.imI) *
          x_3.re +
      c₂ *
          (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI -
            c₁ * x_1.imK * x_2.imI) *
        x_3.imI -
    c₁ * (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) *
      x_3.imI =
  x_1.re *
            (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
              c₁ * x_2.imK * x_3.imI) +
          c₁ * x_1.imI *
            (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
        x_1.imJ *
          (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
            c₁ * c₃ * x_2.imK * x_3.imK) +
      c₂ * x_1.imJ *
        (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
          c₃ * x_2.imK * x_3.imJ) -
    c₁ * x_1.imK *
      (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK + c₃ * x_2.imK * x_3.imJ)
Tactic: 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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * x_2 * x_3).imK = (x_1 * (x_2 * x_3)).imK
have imK : (x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
              c₁ * c₃ * x_1.imK * x_2.imK) *
            x_3.imK +
          (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
              c₃ * x_1.imK * x_2.imJ) *
            x_3.imJ +
        c₂ *
            (x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK +
              c₃ * x_1.imK * x_2.imJ) *
          x_3.imK -
      (x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI - c₁ * x_1.imK * x_2.imI) *
        x_3.imI +
    (x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re) * x_3.re =
  x_1.re * (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) +
          x_1.imI *
            (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI -
              c₁ * x_2.imK * x_3.imI) +
        c₂ * x_1.imI *
          (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re) -
      x_1.imJ *
        (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK +
          c₃ * x_2.imK * x_3.imJ) +
    x_1.imK *
      (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
        c₁ * c₃ * x_2.imK * x_3.imK)
Tactic: 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 : ℍ[R,c₁,c₂,c₃]
⊢ 1 * x_1 = x_1
have re : (1 * x_1).re = x_1.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 : ℍ[R,c₁,c₂,c₃]
re : (1 * x_1).re = x_1.re
⊢ 1 * x_1 = x_1
have imI : (1 * x_1).imI = x_1.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 : ℍ[R,c₁,c₂,c₃]
re : (1 * x_1).re = x_1.re
imI : (1 * x_1).imI = x_1.imI
⊢ 1 * x_1 = x_1
have imJ : (1 * x_1).imJ = x_1.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 : ℍ[R,c₁,c₂,c₃]
re : (1 * x_1).re = x_1.re
imI : (1 * x_1).imI = x_1.imI
imJ : (1 * x_1).imJ = x_1.imJ
⊢ 1 * x_1 = x_1
have imK : (1 * x_1).imK = x_1.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 : ℍ[R,c₁,c₂,c₃]
⊢ x_1 * 1 = x_1
have re : (x_1 * 1).re = x_1.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 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 1).re = x_1.re
⊢ x_1 * 1 = x_1
have imI : (x_1 * 1).imI = x_1.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 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 1).re = x_1.re
imI : (x_1 * 1).imI = x_1.imI
⊢ x_1 * 1 = x_1
have imJ : (x_1 * 1).imJ = x_1.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 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 1).re = x_1.re
imI : (x_1 * 1).imI = x_1.imI
imJ : (x_1 * 1).imJ = x_1.imJ
⊢ x_1 * 1 = x_1
have imK : (x_1 * 1).imK = x_1.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 : ℍ[R,c₁,c₂,c₃]
⊢ 0 * x_1 = 0
have re : (0 * x_1).re = re (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
re : (0 * x_1).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
⊢ 0 * x_1 = 0
have imI : (0 * x_1).imI = imI (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
re : (0 * x_1).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
imI : (0 * x_1).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) 0
⊢ 0 * x_1 = 0
have imJ : (0 * x_1).imJ = imJ (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
re : (0 * x_1).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
imI : (0 * x_1).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) 0
imJ : (0 * x_1).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) 0
⊢ 0 * x_1 = 0
have imK : (0 * x_1).imK = imK (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
⊢ x_1 * 0 = 0
have re : (x_1 * 0).re = re (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 0).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
⊢ x_1 * 0 = 0
have imI : (x_1 * 0).imI = imI (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 0).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
imI : (x_1 * 0).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) 0
⊢ x_1 * 0 = 0
have imJ : (x_1 * 0).imJ = imJ (a := c₁) (b := c₂) (c := c₃) 0
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 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * 0).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) 0
imI : (x_1 * 0).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) 0
imJ : (x_1 * 0).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) 0
⊢ x_1 * 0 = 0
have imK : (x_1 * 0).imK = imK (a := c₁) (b := c₂) (c := c₃) 0
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ x_1 * (x_2 + x_3) = x_1 * x_2 + x_1 * x_3
have re : (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
⊢ x_1 * (x_2 + x_3) = x_1 * x_2 + x_1 * x_3
have imI : (x_1 * (x_2 + x_3)).imI = (x_1 * x_2 + x_1 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
imI : (x_1 * (x_2 + x_3)).imI = (x_1 * x_2 + x_1 * x_3).imI
⊢ x_1 * (x_2 + x_3) = x_1 * x_2 + x_1 * x_3
have imJ : (x_1 * (x_2 + x_3)).imJ = (x_1 * x_2 + x_1 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
re : (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
imI : (x_1 * (x_2 + x_3)).imI = (x_1 * x_2 + x_1 * x_3).imI
imJ : (x_1 * (x_2 + x_3)).imJ = (x_1 * x_2 + x_1 * x_3).imJ
⊢ x_1 * (x_2 + x_3) = x_1 * x_2 + x_1 * x_3
have imK : (x_1 * (x_2 + x_3)).imK = (x_1 * x_2 + x_1 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * (x_2 + x_3)).re = (x_1 * x_2 + x_1 * x_3).re
have re : x_1.re * (x_2.re + x_3.re) + c₁ * x_1.imI * (x_2.imI + x_3.imI) + c₃ * x_1.imJ * (x_2.imJ + x_3.imJ) +
      c₂ * c₃ * x_1.imJ * (x_2.imK + x_3.imK) -
    c₁ * c₃ * x_1.imK * (x_2.imK + x_3.imK) =
  x_1.re * x_2.re + c₁ * x_1.imI * x_2.imI + c₃ * x_1.imJ * x_2.imJ + c₂ * c₃ * x_1.imJ * x_2.imK -
      c₁ * c₃ * x_1.imK * x_2.imK +
    (x_1.re * x_3.re + c₁ * x_1.imI * x_3.imI + c₃ * x_1.imJ * x_3.imJ + c₂ * c₃ * x_1.imJ * x_3.imK -
      c₁ * c₃ * x_1.imK * x_3.imK)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * (x_2 + x_3)).imI = (x_1 * x_2 + x_1 * x_3).imI
have imI : x_1.re * (x_2.imI + x_3.imI) + x_1.imI * (x_2.re + x_3.re) + c₂ * x_1.imI * (x_2.imI + x_3.imI) -
      c₃ * x_1.imJ * (x_2.imK + x_3.imK) +
    c₃ * x_1.imK * (x_2.imJ + x_3.imJ) =
  x_1.re * x_2.imI + x_1.imI * x_2.re + c₂ * x_1.imI * x_2.imI - c₃ * x_1.imJ * x_2.imK + c₃ * x_1.imK * x_2.imJ +
    (x_1.re * x_3.imI + x_1.imI * x_3.re + c₂ * x_1.imI * x_3.imI - c₃ * x_1.imJ * x_3.imK + c₃ * x_1.imK * x_3.imJ)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * (x_2 + x_3)).imJ = (x_1 * x_2 + x_1 * x_3).imJ
have imJ : x_1.re * (x_2.imJ + x_3.imJ) + c₁ * x_1.imI * (x_2.imK + x_3.imK) + x_1.imJ * (x_2.re + x_3.re) +
      c₂ * x_1.imJ * (x_2.imI + x_3.imI) -
    c₁ * x_1.imK * (x_2.imI + x_3.imI) =
  x_1.re * x_2.imJ + c₁ * x_1.imI * x_2.imK + x_1.imJ * x_2.re + c₂ * x_1.imJ * x_2.imI - c₁ * x_1.imK * x_2.imI +
    (x_1.re * x_3.imJ + c₁ * x_1.imI * x_3.imK + x_1.imJ * x_3.re + c₂ * x_1.imJ * x_3.imI - c₁ * x_1.imK * x_3.imI)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 * (x_2 + x_3)).imK = (x_1 * x_2 + x_1 * x_3).imK
have imK : x_1.re * (x_2.imK + x_3.imK) + x_1.imI * (x_2.imJ + x_3.imJ) + c₂ * x_1.imI * (x_2.imK + x_3.imK) -
      x_1.imJ * (x_2.imI + x_3.imI) +
    x_1.imK * (x_2.re + x_3.re) =
  x_1.re * x_2.imK + x_1.imI * x_2.imJ + c₂ * x_1.imI * x_2.imK - x_1.imJ * x_2.imI + x_1.imK * x_2.re +
    (x_1.re * x_3.imK + x_1.imI * x_3.imJ + c₂ * x_1.imI * x_3.imK - x_1.imJ * x_3.imI + x_1.imK * x_3.re)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ (x_1 + x_2) * x_3 = x_1 * x_3 + x_2 * x_3
have re : ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
re : ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
⊢ (x_1 + x_2) * x_3 = x_1 * x_3 + x_2 * x_3
have imI : ((x_1 + x_2) * x_3).imI = (x_1 * x_3 + x_2 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
re : ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
imI : ((x_1 + x_2) * x_3).imI = (x_1 * x_3 + x_2 * x_3).imI
⊢ (x_1 + x_2) * x_3 = x_1 * x_3 + x_2 * x_3
have imJ : ((x_1 + x_2) * x_3).imJ = (x_1 * x_3 + x_2 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
re : ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
imI : ((x_1 + x_2) * x_3).imI = (x_1 * x_3 + x_2 * x_3).imI
imJ : ((x_1 + x_2) * x_3).imJ = (x_1 * x_3 + x_2 * x_3).imJ
⊢ (x_1 + x_2) * x_3 = x_1 * x_3 + x_2 * x_3
have imK : ((x_1 + x_2) * x_3).imK = (x_1 * x_3 + x_2 * x_3).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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ ((x_1 + x_2) * x_3).re = (x_1 * x_3 + x_2 * x_3).re
have re : (x_1.re + x_2.re) * x_3.re + c₁ * (x_1.imI + x_2.imI) * x_3.imI + c₃ * (x_1.imJ + x_2.imJ) * x_3.imJ +
      c₂ * c₃ * (x_1.imJ + x_2.imJ) * x_3.imK -
    c₁ * c₃ * (x_1.imK + x_2.imK) * x_3.imK =
  x_1.re * x_3.re + c₁ * x_1.imI * x_3.imI + c₃ * x_1.imJ * x_3.imJ + c₂ * c₃ * x_1.imJ * x_3.imK -
      c₁ * c₃ * x_1.imK * x_3.imK +
    (x_2.re * x_3.re + c₁ * x_2.imI * x_3.imI + c₃ * x_2.imJ * x_3.imJ + c₂ * c₃ * x_2.imJ * x_3.imK -
      c₁ * c₃ * x_2.imK * x_3.imK)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ ((x_1 + x_2) * x_3).imI = (x_1 * x_3 + x_2 * x_3).imI
have imI : (x_1.re + x_2.re) * x_3.imI + (x_1.imI + x_2.imI) * x_3.re + c₂ * (x_1.imI + x_2.imI) * x_3.imI -
      c₃ * (x_1.imJ + x_2.imJ) * x_3.imK +
    c₃ * (x_1.imK + x_2.imK) * x_3.imJ =
  x_1.re * x_3.imI + x_1.imI * x_3.re + c₂ * x_1.imI * x_3.imI - c₃ * x_1.imJ * x_3.imK + c₃ * x_1.imK * x_3.imJ +
    (x_2.re * x_3.imI + x_2.imI * x_3.re + c₂ * x_2.imI * x_3.imI - c₃ * x_2.imJ * x_3.imK + c₃ * x_2.imK * x_3.imJ)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ ((x_1 + x_2) * x_3).imJ = (x_1 * x_3 + x_2 * x_3).imJ
have imJ : (x_1.re + x_2.re) * x_3.imJ + c₁ * (x_1.imI + x_2.imI) * x_3.imK + (x_1.imJ + x_2.imJ) * x_3.re +
      c₂ * (x_1.imJ + x_2.imJ) * x_3.imI -
    c₁ * (x_1.imK + x_2.imK) * x_3.imI =
  x_1.re * x_3.imJ + c₁ * x_1.imI * x_3.imK + x_1.imJ * x_3.re + c₂ * x_1.imJ * x_3.imI - c₁ * x_1.imK * x_3.imI +
    (x_2.re * x_3.imJ + c₁ * x_2.imI * x_3.imK + x_2.imJ * x_3.re + c₂ * x_2.imJ * x_3.imI - c₁ * x_2.imK * x_3.imI)
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 x_3 : ℍ[R,c₁,c₂,c₃]
⊢ ((x_1 + x_2) * x_3).imK = (x_1 * x_3 + x_2 * x_3).imK
have imK : (x_1.re + x_2.re) * x_3.imK + (x_1.imI + x_2.imI) * x_3.imJ + c₂ * (x_1.imI + x_2.imI) * x_3.imK -
      (x_1.imJ + x_2.imJ) * x_3.imI +
    (x_1.imK + x_2.imK) * x_3.re =
  x_1.re * x_3.imK + x_1.imI * x_3.imJ + c₂ * x_1.imI * x_3.imK - x_1.imJ * x_3.imI + x_1.imK * x_3.re +
    (x_2.re * x_3.imK + x_2.imI * x_3.imJ + c₂ * x_2.imI * x_3.imK - x_2.imJ * x_3.imI + x_2.imK * x_3.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
⊢ (↑(x * y) : ℍ[R,c₁,c₂,c₃]) = HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])
have re : re (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re
⊢ (↑(x * y) : ℍ[R,c₁,c₂,c₃]) = HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])
have imI : imI (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re
imI :
  QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imI
⊢ (↑(x * y) : ℍ[R,c₁,c₂,c₃]) = HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])
have imJ : imJ (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : CommRing R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re
imI :
  QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imI
imJ :
  QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
    (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imJ
⊢ (↑(x * y) : ℍ[R,c₁,c₂,c₃]) = HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])
have imK : imK (a := c₁) (b := c₂) (c := c₃) (↑(x * y) : ℍ[R,c₁,c₂,c₃]) =
  (HMul.hMul (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imK
Tactic: 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₃]
⊢ 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 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 =
  (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₃])).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 :
  (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
⊢ 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 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 =
  (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₃])).imI
Tactic: ext