awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
h :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ : Fin (Nat.succ 3))
h₁ :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (Nat.succ 3))
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x) =
    x
have h₂ : (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
    ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
    ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ =
  x (⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩ : Fin (Nat.succ 3))
Tactic: ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
c₁ c₂ c₃ : R
x : Fin 4 → R
h :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 3, ⋯⟩ : Fin (Nat.succ 3))
h₁ :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 2, ⋯⟩ : Fin (Nat.succ 3))
h₂ :
  (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x)
      ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ =
    x (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (Nat.succ 3))
⊢ (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
      ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x) =
    x
have h₃ : (fun (a : ℍ[R,c₁,c₂,c₃]) ↦ ![a.re, a.imI, a.imJ, a.imK])
    ((fun (a : Fin 4 → R) ↦ ({ re := a 0, imI := a 1, imJ := a 2, imK := a 3 } : ℍ[R,c₁,c₂,c₃])) x) ⟨0, sorry⟩ =
  x (⟨0, sorry⟩ : Fin (Nat.succ 3))
Tactic: ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
c₁ c₂ c₃ x y : R
inst : AddZeroClass R
⊢ (↑(x + y) : ℍ[R,c₁,c₂,c₃]) = HAdd.hAdd (α := ℍ[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₃]) =
  (HAdd.hAdd (α := ℍ[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 : AddZeroClass R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).re
⊢ (↑(x + y) : ℍ[R,c₁,c₂,c₃]) = HAdd.hAdd (α := ℍ[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₃]) =
  (HAdd.hAdd (α := ℍ[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 : AddZeroClass R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[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₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imI
⊢ (↑(x + y) : ℍ[R,c₁,c₂,c₃]) = HAdd.hAdd (α := ℍ[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₃]) =
  (HAdd.hAdd (α := ℍ[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 : AddZeroClass R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(x + y) : ℍ[R,c₁,c₂,c₃]) =
    (HAdd.hAdd (α := ℍ[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₃]) =
    (HAdd.hAdd (α := ℍ[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₃]) =
    (HAdd.hAdd (α := ℍ[R,c₁,c₂,c₃]) (↑x : ℍ[R,c₁,c₂,c₃]) (↑y : ℍ[R,c₁,c₂,c₃])).imJ
⊢ (↑(x + y) : ℍ[R,c₁,c₂,c₃]) = HAdd.hAdd (α := ℍ[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₃]) =
  (HAdd.hAdd (α := ℍ[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:
R : Type u_3
c₁ c₂ c₃ x : R
inst : AddGroup R
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(-x) : ℍ[R,c₁,c₂,c₃]) (-(↑x : ℍ[R,c₁,c₂,c₃]))
have re : re (a := c₁) (b := c₂) (c := c₃) (↑(-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 : AddGroup R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(-x) : ℍ[R,c₁,c₂,c₃]) =
    QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (-(↑x : ℍ[R,c₁,c₂,c₃]))
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(-x) : ℍ[R,c₁,c₂,c₃]) (-(↑x : ℍ[R,c₁,c₂,c₃]))
have imI : imI (a := c₁) (b := c₂) (c := c₃) (↑(-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 : AddGroup R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(-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₃) (↑(-x) : ℍ[R,c₁,c₂,c₃]) =
    QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (-(↑x : ℍ[R,c₁,c₂,c₃]))
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(-x) : ℍ[R,c₁,c₂,c₃]) (-(↑x : ℍ[R,c₁,c₂,c₃]))
have imJ : imJ (a := c₁) (b := c₂) (c := c₃) (↑(-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 : AddGroup R
re :
  QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(-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₃) (↑(-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₃) (↑(-x) : ℍ[R,c₁,c₂,c₃]) =
    QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (-(↑x : ℍ[R,c₁,c₂,c₃]))
⊢ Eq (α := ℍ[R,c₁,c₂,c₃]) (↑(-x) : ℍ[R,c₁,c₂,c₃]) (-(↑x : ℍ[R,c₁,c₂,c₃]))
have imK : imK (a := c₁) (b := c₂) (c := c₃) (↑(-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:
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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t) • x = s • t • x
have re : ((s • t) • x).re = (s • t • 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : ((s • t) • x).re = (s • t • x).re
⊢ (s • t) • x = s • t • x
have imI : ((s • t) • x).imI = (s • t • 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : ((s • t) • x).re = (s • t • x).re
imI : ((s • t) • x).imI = (s • t • x).imI
⊢ (s • t) • x = s • t • x
have imJ : ((s • t) • x).imJ = (s • t • 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMul S T
inst_3 : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : ((s • t) • x).re = (s • t • x).re
imI : ((s • t) • x).imI = (s • t • x).imI
imJ : ((s • t) • x).imJ = (s • t • x).imJ
⊢ (s • t) • x = s • t • x
have imK : ((s • t) • x).imK = (s • t • x).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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ s • t • x = t • s • x
have re : (s • t • x).re = (t • s • 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : (s • t • x).re = (t • s • x).re
⊢ s • t • x = t • s • x
have imI : (s • t • x).imI = (t • s • 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : (s • t • x).re = (t • s • x).re
imI : (s • t • x).imI = (t • s • x).imI
⊢ s • t • x = t • s • x
have imJ : (s • t • x).imJ = (t • s • 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 : SMul S R
inst_1 : SMul T R
s_1 : S
inst_2 : SMulCommClass S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
re : (s • t • x).re = (t • s • x).re
imI : (s • t • x).imI = (t • s • x).imI
imJ : (s • t • x).imJ = (t • s • x).imJ
⊢ s • t • x = t • s • x
have imK : (s • t • x).imK = (t • s • x).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 : AddCommGroup R
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]
have zero : Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
  (0 : R × R × R × R)
Tactic: apply (equivProd c₁ c₂ c₃).injective.addCommGroup
-- 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 : AddCommGroup R
zero :
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]
have add : ∀ (x y : ℍ[R,c₁,c₂,c₃]),
  (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x + y) =
    HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
Tactic: apply (equivProd c₁ c₂ c₃).injective.addCommGroup
-- 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 : AddCommGroup R
zero :
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)
add :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x + y) =
      HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]
have neg : ∀ (x : ℍ[R,c₁,c₂,c₃]),
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (-x) : R × R × R × R)
    (-(equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
Tactic: apply (equivProd c₁ c₂ c₃).injective.addCommGroup
-- 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 : AddCommGroup R
zero :
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)
add :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x + y) =
      HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
neg :
  ∀ (x : ℍ[R,c₁,c₂,c₃]),
    Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (-x) : R × R × R × R)
      (-(equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]
have sub : ∀ (x y : ℍ[R,c₁,c₂,c₃]),
  (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x - y) =
    HSub.hSub (α := R × R × R × R) (β := R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
      ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
Tactic: apply (equivProd c₁ c₂ c₃).injective.addCommGroup
-- 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 : AddCommGroup R
zero :
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)
add :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x + y) =
      HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
neg :
  ∀ (x : ℍ[R,c₁,c₂,c₃]),
    Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (-x) : R × R × R × R)
      (-(equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
sub :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x - y) =
      HSub.hSub (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]
have nsmul : ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℕ),
  (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x) =
    HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
Tactic: apply (equivProd c₁ c₂ c₃).injective.addCommGroup
-- 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 : AddCommGroup R
zero :
  Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) 0 : R × R × R × R)
    (0 : R × R × R × R)
add :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x + y) =
      HAdd.hAdd (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
neg :
  ∀ (x : ℍ[R,c₁,c₂,c₃]),
    Eq (α := R × R × R × R) ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (-x) : R × R × R × R)
      (-(equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
sub :
  ∀ (x y : ℍ[R,c₁,c₂,c₃]),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (x - y) =
      HSub.hSub (α := R × R × R × R) (β := R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
        ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) y : R × R × R × R)
nsmul :
  ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℕ),
    (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x) =
      HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]
have zsmul : ∀ (x : ℍ[R,c₁,c₂,c₃]) (n : ℤ),
  (equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) (n • x) =
    HSMul.hSMul (β := R × R × R × R) n ((equivProd c₁ c₂ c₃ : (a : ℍ[R,c₁,c₂,c₃]) → R × R × R × R) x : R × R × R × R)
Tactic: apply (equivProd c₁ c₂ c₃).injective.addCommGroup
-- 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 : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(n + 1) : ℍ[R,c₁,c₂,c₃]))
have change : Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
Tactic: change coe _ = -coe _
-- 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 : AddCommGroupWithOne R
n : ℕ
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
have rw : Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(-(↑(n + 1) : R)) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
Tactic: rw [Int.cast_negSucc, coe_neg]
-- 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 : AddCommGroupWithOne R
n : ℕ
rw : Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(-(↑(n + 1) : R)) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
⊢ Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (↑(↑(Int.negSucc n) : R) : ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
have rw₁ : Eq.{u_3 + 1} (α := ℍ[R,c₁,c₂,c₃]) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃])) (-(↑(↑(n + 1) : R) : ℍ[R,c₁,c₂,c₃]))
Tactic: rw [Int.cast_negSucc, coe_neg]
-- 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_3)
have re : (x_1 * x_2 * x_3).re = (x_1 * (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_2 * x_3)).re
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)
have imI : (x_1 * x_2 * x_3).imI = (x_1 * (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_2 * x_3)).re
imI : (x_1 * x_2 * x_3).imI = (x_1 * (x_2 * x_3)).imI
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)
have imJ : (x_1 * x_2 * x_3).imJ = (x_1 * (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_2 * x_3)).re
imI : (x_1 * x_2 * x_3).imI = (x_1 * (x_2 * x_3)).imI
imJ : (x_1 * x_2 * x_3).imJ = (x_1 * (x_2 * x_3)).imJ
⊢ x_1 * x_2 * x_3 = x_1 * (x_2 * x_3)
have imK : (x_1 * x_2 * x_3).imK = (x_1 * (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_2 * x_3)).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.imJ * x_2.imK -
              c₁ * c₃ * x_1.imK * x_2.imK) *
            x_3.re +
          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.imI +
        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.imJ +
      c₂ * 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.imK -
    c₁ * 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.imK =
  x_1.re *
            (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.imI *
            (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.imJ *
          (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₂ * c₃ * x_1.imJ *
        (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) -
    c₁ * c₃ * x_1.imK *
      (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:
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_3)).imI
have imI : (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.imI +
          (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.re +
        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.imI -
      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.imK +
    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.imJ =
  x_1.re *
            (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.imI *
            (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.imI *
          (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.imJ *
        (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) +
    c₃ * x_1.imK *
      (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