awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have re : (star a * a).re = re (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[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 : (star a * a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
⊢ star a * a = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have imI : (star a * a).imI = imI (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[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 : (star a * a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
imI : (star a * a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
⊢ star a * a = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have imJ : (star a * a).imJ = imJ (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[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 : (star a * a).re = QuaternionAlgebra.re (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
imI : (star a * a).imI = QuaternionAlgebra.imI (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
imJ : (star a * a).imJ = QuaternionAlgebra.imJ (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
⊢ star a * a = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have imK : (star a * a).imK = imK (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[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 * a).imI = imI (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have imI : (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0
Tactic: simp
-- 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).imJ = imJ (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have imJ : (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0
Tactic: simp
-- 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).imK = imK (a := c₁) (b := c₂) (c := c₃) (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
have imK : (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0
Tactic: simp
-- 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 = (↑(a * star a).re : ℍ[R,c₁,c₂,c₃])
have rw : star a * a = (↑(star a * a).re : ℍ[R,c₁,c₂,c₃])
Tactic: rw [← star_comm_self']
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ (star a).re = a.re
have rw : a.re + 0 * a.imI = a.re
Tactic: rw [QuaternionAlgebra.re_star, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
rw : a.re + 0 * a.imI = a.re
⊢ (star a).re = a.re
have rw₁ : a.re + 0 = a.re
Tactic: rw [QuaternionAlgebra.re_star, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
rw : a.re + 0 * a.imI = a.re
rw₁ : a.re + 0 = a.re
⊢ (star a).re = a.re
have rw₂ : a.re = a.re
Tactic: rw [QuaternionAlgebra.re_star, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ star a.im = -a.im
have a₁ : (star a.im).re = (-a.im).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
a₁ : (star a.im).re = (-a.im).re
⊢ star a.im = -a.im
have a₂ : (star a.im).imI = (-a.im).imI
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
a₁ : (star a.im).re = (-a.im).re
a₂ : (star a.im).imI = (-a.im).imI
⊢ star a.im = -a.im
have a₃ : (star a.im).imJ = (-a.im).imJ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
a₁ : (star a.im).re = (-a.im).re
a₂ : (star a.im).imI = (-a.im).imI
a₃ : (star a.im).imJ = (-a.im).imJ
⊢ star a.im = -a.im
have a₄ : (star a.im).imK = (-a.im).imK
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
x : R
⊢ (normSq : (a : ℍ[R]) → R) (↑x : ℍ[R]) = HPow.hPow (β := ℕ) x 2
have rw : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (star (↑x : ℍ[R]))).re = HPow.hPow (β := ℕ) x 2
Tactic: rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
x : R
rw : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (star (↑x : ℍ[R]))).re = HPow.hPow (β := ℕ) x 2
⊢ (normSq : (a : ℍ[R]) → R) (↑x : ℍ[R]) = HPow.hPow (β := ℕ) x 2
have rw₁ : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (↑x : ℍ[R])).re = HPow.hPow (β := ℕ) x 2
Tactic: rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
x : R
rw : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (star (↑x : ℍ[R]))).re = HPow.hPow (β := ℕ) x 2
rw₁ : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (↑x : ℍ[R])).re = HPow.hPow (β := ℕ) x 2
⊢ (normSq : (a : ℍ[R]) → R) (↑x : ℍ[R]) = HPow.hPow (β := ℕ) x 2
have rw₂ : QuaternionAlgebra.re (a := -1) (↑(x * x) : ℍ[R]) = HPow.hPow (β := ℕ) x 2
Tactic: rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
x : R
rw : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (star (↑x : ℍ[R]))).re = HPow.hPow (β := ℕ) x 2
rw₁ : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (↑x : ℍ[R])).re = HPow.hPow (β := ℕ) x 2
rw₂ : QuaternionAlgebra.re (a := -1) (↑(x * x) : ℍ[R]) = HPow.hPow (β := ℕ) x 2
⊢ (normSq : (a : ℍ[R]) → R) (↑x : ℍ[R]) = HPow.hPow (β := ℕ) x 2
have rw₃ : x * x = HPow.hPow (β := ℕ) x 2
Tactic: rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
x : R
rw : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (star (↑x : ℍ[R]))).re = HPow.hPow (β := ℕ) x 2
rw₁ : (HMul.hMul (α := ℍ[R]) (↑x : ℍ[R]) (↑x : ℍ[R])).re = HPow.hPow (β := ℕ) x 2
rw₂ : QuaternionAlgebra.re (a := -1) (↑(x * x) : ℍ[R]) = HPow.hPow (β := ℕ) x 2
rw₃ : x * x = HPow.hPow (β := ℕ) x 2
⊢ (normSq : (a : ℍ[R]) → R) (↑x : ℍ[R]) = HPow.hPow (β := ℕ) x 2
have rw₄ : x * x = x * x
Tactic: rw [normSq_def, star_coe, ← coe_mul, re_coe, sq]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
⊢ (normSq : (a : ℍ[R]) → R) (↑n : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have rw : (normSq : (a : ℍ[R]) → R) (↑(↑n : R) : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
Tactic: rw [← coe_natCast, normSq_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
rw : (normSq : (a : ℍ[R]) → R) (↑(↑n : R) : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
⊢ (normSq : (a : ℍ[R]) → R) (↑n : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
have rw₁ : HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2
Tactic: rw [← coe_natCast, normSq_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
z : ℤ
⊢ (normSq : (a : ℍ[R]) → R) (↑z : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
have rw : (normSq : (a : ℍ[R]) → R) (↑(↑z : R) : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
Tactic: rw [← coe_intCast, normSq_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
z : ℤ
rw : (normSq : (a : ℍ[R]) → R) (↑(↑z : R) : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
⊢ (normSq : (a : ℍ[R]) → R) (↑z : ℍ[R]) = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
have rw₁ : HPow.hPow (α := R) (β := ℕ) (↑z : R) 2 = HPow.hPow (α := R) (β := ℕ) (↑z : R) 2
Tactic: rw [← coe_intCast, normSq_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ a * star a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
have rw : Eq (α := ℍ[R]) (↑(a * star a).re : ℍ[R]) (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
Tactic: rw [mul_star_eq_coe, normSq_def]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
rw : Eq (α := ℍ[R]) (↑(a * star a).re : ℍ[R]) (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
⊢ a * star a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
have rw₁ : Eq (α := ℍ[R]) (↑(a * star a).re : ℍ[R]) (↑(a * star a).re : ℍ[R])
Tactic: rw [mul_star_eq_coe, normSq_def]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ star a * a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
have rw : a * star a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
Tactic: rw [star_comm_self, self_mul_star]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
rw : a * star a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
⊢ star a * a = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R])
have rw₁ : Eq (α := ℍ[R]) ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R])
Tactic: rw [star_comm_self, self_mul_star]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
⊢ HPow.hPow (β := ℕ) a.im 2 = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
have simp_rw : a.im * a.im = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
Tactic: simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
simp_rw : a.im * a.im = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
⊢ HPow.hPow (β := ℕ) a.im 2 = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
have simp_rw₁ : a.im * a.im = -(star a.im * a.im)
Tactic: simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
simp_rw : a.im * a.im = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
simp_rw₁ : a.im * a.im = -(star a.im * a.im)
⊢ HPow.hPow (β := ℕ) a.im 2 = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
have simp_rw₂ : a.im * a.im = -(-a.im * a.im)
Tactic: simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a : ℍ[R]
simp_rw : a.im * a.im = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
simp_rw₁ : a.im * a.im = -(star a.im * a.im)
simp_rw₂ : a.im * a.im = -(-a.im * a.im)
⊢ HPow.hPow (β := ℕ) a.im 2 = -(↑((normSq : (a : ℍ[R]) → R) a.im) : ℍ[R])
have simp_rw₃ : a.im * a.im = - -(a.im * a.im)
Tactic: simp_rw [sq, ← star_mul_self, star_im, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ (normSq : (a : ℍ[R]) → R) (a + b) =
    HAdd.hAdd (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (a * star b).re +
      HAdd.hAdd (β := R) (b * star a).re ((normSq : (a : ℍ[R]) → R) b : R)
have simp_rw : ((a + b) * star (a + b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
Tactic: simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
simp_rw : ((a + b) * star (a + b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
⊢ (normSq : (a : ℍ[R]) → R) (a + b) =
    HAdd.hAdd (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (a * star b).re +
      HAdd.hAdd (β := R) (b * star a).re ((normSq : (a : ℍ[R]) → R) b : R)
have simp_rw₁ : ((a + b) * (star a + star b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
Tactic: simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
simp_rw : ((a + b) * star (a + b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
simp_rw₁ : ((a + b) * (star a + star b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
⊢ (normSq : (a : ℍ[R]) → R) (a + b) =
    HAdd.hAdd (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (a * star b).re +
      HAdd.hAdd (β := R) (b * star a).re ((normSq : (a : ℍ[R]) → R) b : R)
have simp_rw₂ : (a * (star a + star b) + b * (star a + star b)).re =
  (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
Tactic: simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
simp_rw : ((a + b) * star (a + b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
simp_rw₁ : ((a + b) * (star a + star b)).re = (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
simp_rw₂ :
  (a * (star a + star b) + b * (star a + star b)).re =
    (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
⊢ (normSq : (a : ℍ[R]) → R) (a + b) =
    HAdd.hAdd (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (a * star b).re +
      HAdd.hAdd (β := R) (b * star a).re ((normSq : (a : ℍ[R]) → R) b : R)
have simp_rw₃ : (a * star a + a * star b + (b * star a + b * star b)).re =
  (a * star a).re + (a * star b).re + ((b * star a).re + (b * star b).re)
Tactic: simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      ((a * star b).re + (b * star a).re) =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
have rw : HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
    (a * star b + b * star a).re =
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) + 2 * (a * star b).re
Tactic: rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
rw :
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      (a * star b + b * star a).re =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
⊢ HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      ((a * star b).re + (b * star a).re) =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
have rw₁ : HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
    (a * star b + star (a * star b)).re =
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) + 2 * (a * star b).re
Tactic: rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
rw :
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      (a * star b + b * star a).re =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
rw₁ :
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      (a * star b + star (a * star b)).re =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
⊢ HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      ((a * star b).re + (b * star a).re) =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
have rw₂ : HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
    QuaternionAlgebra.re (a := -1) (↑(2 * (a * star b).re) : ℍ[R]) =
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) + 2 * (a * star b).re
Tactic: rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
rw :
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      (a * star b + b * star a).re =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
rw₁ :
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      (a * star b + star (a * star b)).re =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
rw₂ :
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      QuaternionAlgebra.re (a := -1) (↑(2 * (a * star b).re) : ℍ[R]) =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
⊢ HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      ((a * star b).re + (b * star a).re) =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      2 * (a * star b).re
have rw₃ : HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) + 2 * (a * star b).re =
  HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) + 2 * (a * star b).re
Tactic: rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R) ↔ a = 0
have refine : ∀ (h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)), a = 0
Tactic: refine ⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)
⊢ a = 0
have rw : ∀
  (h :
    ((HPow.hPow (β := ℕ) a.re 2 = 0 ∧ HPow.hPow (β := ℕ) a.imI 2 = 0) ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
      HPow.hPow (β := ℕ) a.imK 2 = 0),
  a = 0
Tactic: rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
    at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)
rw :
  ∀
    (h :
      ((HPow.hPow (β := ℕ) a.re 2 = 0 ∧ HPow.hPow (β := ℕ) a.imI 2 = 0) ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    a = 0
⊢ a = 0
have ha : ∀
  (h :
    (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
      HPow.hPow (β := ℕ) a.imK 2 = 0),
  0 ≤ HPow.hPow (β := ℕ) a.re 2
Tactic: rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
    at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)
rw :
  ∀
    (h :
      ((HPow.hPow (β := ℕ) a.re 2 = 0 ∧ HPow.hPow (β := ℕ) a.imI 2 = 0) ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    a = 0
ha :
  ∀
    (h :
      (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    0 ≤ HPow.hPow (β := ℕ) a.re 2
⊢ a = 0
have hb : ∀
  (h :
    (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
      HPow.hPow (β := ℕ) a.imK 2 = 0),
  0 ≤ HPow.hPow (β := ℕ) a.imI 2
Tactic: rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
    at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)
rw :
  ∀
    (h :
      ((HPow.hPow (β := ℕ) a.re 2 = 0 ∧ HPow.hPow (β := ℕ) a.imI 2 = 0) ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    a = 0
ha :
  ∀
    (h :
      (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    0 ≤ HPow.hPow (β := ℕ) a.re 2
hb :
  ∀
    (h :
      (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    0 ≤ HPow.hPow (β := ℕ) a.imI 2
⊢ a = 0
have ha₁ : ∀
  (h :
    HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 = 0 ∧
      HPow.hPow (β := ℕ) a.imK 2 = 0),
  0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2
Tactic: rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
    at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)
rw :
  ∀
    (h :
      ((HPow.hPow (β := ℕ) a.re 2 = 0 ∧ HPow.hPow (β := ℕ) a.imI 2 = 0) ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    a = 0
ha :
  ∀
    (h :
      (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    0 ≤ HPow.hPow (β := ℕ) a.re 2
hb :
  ∀
    (h :
      (HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 = 0 ∧ HPow.hPow (β := ℕ) a.imJ 2 = 0) ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    0 ≤ HPow.hPow (β := ℕ) a.imI 2
ha₁ :
  ∀
    (h :
      HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 = 0 ∧
        HPow.hPow (β := ℕ) a.imK 2 = 0),
    0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2
⊢ a = 0
have hb₁ : ∀
  (h :
    HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 = 0 ∧
      HPow.hPow (β := ℕ) a.imK 2 = 0),
  0 ≤ HPow.hPow (β := ℕ) a.imJ 2
Tactic: rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
    at h
Cleared hypotheses: h