awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ a = 0
have ha₂ : ∀
  (h :
    HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2 =
      0),
  0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + 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
-- 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
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
ha₂ :
  ∀
    (h :
      HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2 =
        0),
    0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2
⊢ a = 0
have hb₂ : ∀
  (h :
    HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2 =
      0),
  0 ≤ HPow.hPow (β := ℕ) a.imK 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 :
  ((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
have a₁ : a.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0
Tactic: apply ext a 0
-- 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 :
  ((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₁ : a.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0
⊢ a = 0
have a₂ : a.imI = QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0
Tactic: apply ext a 0
-- 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 :
  ((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₁ : a.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0
a₂ : a.imI = QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0
⊢ a = 0
have a₃ : a.imJ = QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 0
Tactic: apply ext a 0
-- 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 :
  ((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₁ : a.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0
a₂ : a.imI = QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0
a₃ : a.imJ = QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 0
⊢ a = 0
have a₄ : a.imK = QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 0
Tactic: apply ext a 0
-- 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 :
  ((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.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0
have a₁ : HPow.hPow (β := ℕ) a.re 2 = 0
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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₁ : HPow.hPow (β := ℕ) a.re 2 = 0
⊢ a.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0
have a₂ : ℕ
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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.imI = QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0
have a₁ : HPow.hPow (β := ℕ) a.imI 2 = 0
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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₁ : HPow.hPow (β := ℕ) a.imI 2 = 0
⊢ a.imI = QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0
have a₂ : ℕ
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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.imJ = QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 0
have a₁ : HPow.hPow (β := ℕ) a.imJ 2 = 0
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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₁ : HPow.hPow (β := ℕ) a.imJ 2 = 0
⊢ a.imJ = QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 0
have a₂ : ℕ
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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.imK = QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 0
have a₁ : HPow.hPow (β := ℕ) a.imK 2 = 0
Tactic: apply eq_zero_of_pow_eq_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 :
  ((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₁ : HPow.hPow (β := ℕ) a.imK 2 = 0
⊢ a.imK = QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 0
have a₂ : ℕ
Tactic: apply eq_zero_of_pow_eq_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]
⊢ LE.le (α := R) (0 : R) ((normSq : (a : ℍ[R]) → R) a : R)
have rw : 0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2
Tactic: rw [normSq_def']
-- 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_1 a b : ℍ[R]
hab : a * b = 0
⊢ HMul.hMul (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) = 0
have rwa : Eq (α := R) ((normSq : (a : ℍ[R]) → R) (a * b) : R) (0 : R)
Tactic: rwa [← map_mul, normSq_eq_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]
⊢ HPow.hPow (β := ℕ) a 2 = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ a = (↑a.re : ℍ[R])
have rw : star a = a ∨ a = 0 ↔ star a = a
Tactic: rw [← star_eq_self, ← star_mul_self, sq, mul_eq_mul_right_iff, eq_comm]
-- 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]
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ a.re = 0
have simp_rw : HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
Tactic: simp_rw [← star_eq_neg]
-- 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]
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inl : HPow.hPow (α := ℍ[R]) (β := ℕ) 0 2 = -(↑((normSq : (a : ℍ[R]) → R) 0) : ℍ[R]) ↔ Eq.{u_1 + 1} (α := ℍ[R]) (star 0) (-0)
Tactic: obtain rfl | hq0 := eq_or_ne a 0
Cleared hypotheses: a
-- 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]
inl :
  HPow.hPow (α := ℍ[R]) (β := ℕ) 0 2 = -(↑((normSq : (a : ℍ[R]) → R) 0) : ℍ[R]) ↔ Eq.{u_1 + 1} (α := ℍ[R]) (star 0) (-0)
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr : ∀ (hq0 : a ≠ 0), HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
Tactic: obtain rfl | hq0 := eq_or_ne a 0
-- 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]
hq0 : a ≠ 0
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr : HPow.hPow (β := ℕ) a 2 = -(star a * a) ↔ star a = -a
Tactic: rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
-- 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]
hq0 : a ≠ 0
inr : HPow.hPow (β := ℕ) a 2 = -(star a * a) ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr₁ : HPow.hPow (β := ℕ) a 2 = star a * -a ↔ star a = -a
Tactic: rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
-- 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]
hq0 : a ≠ 0
inr : HPow.hPow (β := ℕ) a 2 = -(star a * a) ↔ star a = -a
inr₁ : HPow.hPow (β := ℕ) a 2 = star a * -a ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr₂ : HPow.hPow (β := ℕ) (-a) 2 = star a * -a ↔ star a = -a
Tactic: rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
-- 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]
hq0 : a ≠ 0
inr : HPow.hPow (β := ℕ) a 2 = -(star a * a) ↔ star a = -a
inr₁ : HPow.hPow (β := ℕ) a 2 = star a * -a ↔ star a = -a
inr₂ : HPow.hPow (β := ℕ) (-a) 2 = star a * -a ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr₃ : -a * -a = star a * -a ↔ star a = -a
Tactic: rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
-- 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]
hq0 : a ≠ 0
inr : HPow.hPow (β := ℕ) a 2 = -(star a * a) ↔ star a = -a
inr₁ : HPow.hPow (β := ℕ) a 2 = star a * -a ↔ star a = -a
inr₂ : HPow.hPow (β := ℕ) (-a) 2 = star a * -a ↔ star a = -a
inr₃ : -a * -a = star a * -a ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr₄ : -a = star a ↔ star a = -a
Tactic: rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
-- 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]
hq0 : a ≠ 0
inr : HPow.hPow (β := ℕ) a 2 = -(star a * a) ↔ star a = -a
inr₁ : HPow.hPow (β := ℕ) a 2 = star a * -a ↔ star a = -a
inr₂ : HPow.hPow (β := ℕ) (-a) 2 = star a * -a ↔ star a = -a
inr₃ : -a * -a = star a * -a ↔ star a = -a
inr₄ : -a = star a ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
have inr₅ : star a = -a ↔ star a = -a
Tactic: rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
⊢ Eq.{u_1 + 1} (α := ℍ[R]) 0⁻¹ 0
have rw : HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) 0)⁻¹ : R) (star 0) = 0
Tactic: rw [inv_def, star_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
rw : HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) 0)⁻¹ : R) (star 0) = 0
⊢ Eq.{u_1 + 1} (α := ℍ[R]) 0⁻¹ 0
have rw₁ : HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) 0)⁻¹ : R) 0 = 0
Tactic: rw [inv_def, star_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
rw : HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) 0)⁻¹ : R) (star 0) = 0
rw₁ : HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) 0)⁻¹ : R) 0 = 0
⊢ Eq.{u_1 + 1} (α := ℍ[R]) 0⁻¹ 0
have rw₂ : Eq.{u_1 + 1} (α := ℍ[R]) 0 0
Tactic: rw [inv_def, star_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a_2 b a : ℍ[R]
ha : a ≠ 0
⊢ a * a⁻¹ = 1
have rw : a * HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (star a) = 1
Tactic: rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a_2 b a : ℍ[R]
ha : a ≠ 0
rw : a * HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (star a) = 1
⊢ a * a⁻¹ = 1
have rw₁ : HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (a * star a) = 1
Tactic: rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a_2 b a : ℍ[R]
ha : a ≠ 0
rw : a * HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (star a) = 1
rw₁ : HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (a * star a) = 1
⊢ a * a⁻¹ = 1
have rw₂ : HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R)
    ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) =
  1
Tactic: rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a_2 b a : ℍ[R]
ha : a ≠ 0
rw : a * HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (star a) = 1
rw₁ : HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (a * star a) = 1
rw₂ :
  HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R)
      ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) =
    1
⊢ a * a⁻¹ = 1
have rw₃ : Eq (α := ℍ[R])
  (↑(HMul.hMul (α := R) (β := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) ((normSq : (a : ℍ[R]) → R) a : R)) : ℍ[R]) 1
Tactic: rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a_2 b a : ℍ[R]
ha : a ≠ 0
rw : a * HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (star a) = 1
rw₁ : HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (a * star a) = 1
rw₂ :
  HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R)
      ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) =
    1
rw₃ :
  Eq (α := ℍ[R])
    (↑(HMul.hMul (α := R) (β := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) ((normSq : (a : ℍ[R]) → R) a : R)) : ℍ[R]) 1
⊢ a * a⁻¹ = 1
have rw₄ : Eq.{u_1 + 1} (α := ℍ[R]) (↑1 : ℍ[R]) 1
Tactic: rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a_2 b a : ℍ[R]
ha : a ≠ 0
rw : a * HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (star a) = 1
rw₁ : HSMul.hSMul (α := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) (a * star a) = 1
rw₂ :
  HSMul.hSMul (α := R) (β := ℍ[R]) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R)
      ((↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) : ℍ[R]) =
    1
rw₃ :
  Eq (α := ℍ[R])
    (↑(HMul.hMul (α := R) (β := R) (((normSq : (a : ℍ[R]) → R) a)⁻¹ : R) ((normSq : (a : ℍ[R]) → R) a : R)) : ℍ[R]) 1
rw₄ : Eq.{u_1 + 1} (α := ℍ[R]) (↑1 : ℍ[R]) 1
⊢ a * a⁻¹ = 1
have rw₅ : Eq.{u_1 + 1} (α := ℍ[R]) 1 1
Tactic: rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₁ : (↑(HDiv.hDiv (α := R) (↑x.num : R) (↑x.den : R)) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₁ : (↑(HDiv.hDiv (α := R) (↑x.num : R) (↑x.den : R)) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₂ : HDiv.hDiv (α := ℍ[R]) (↑(↑x.num : R) : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) =
  HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₁ : (↑(HDiv.hDiv (α := R) (↑x.num : R) (↑x.den : R)) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₂ :
  HDiv.hDiv (α := ℍ[R]) (↑(↑x.num : R) : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) =
    HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₃ : HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
rw : (↑(↑x : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₁ : (↑(HDiv.hDiv (α := R) (↑x.num : R) (↑x.den : R)) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₂ :
  HDiv.hDiv (α := ℍ[R]) (↑(↑x.num : R) : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) =
    HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
rw₃ :
  HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑(↑x.den : R) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
have rw₄ : HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
Tactic: rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ x • x_1 = (↑x : ℍ[R]) * x_1
have rw : x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
Tactic: rw [← coe_nnratCast, coe_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₁ : (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Quaternion (goal)
Goal:
R : Type u_1
inst : Field R
a_1 b_1 : ℍ[R]
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℍ[R]
x : ℚ≥0
x_1 : ℍ[R]
a₁ : (x • x_1).re = (HSMul.hSMul (α := R) (↑x : R) x_1).re
⊢ x • x_1 = HSMul.hSMul (α := R) (↑x : R) x_1
have a₂ : (x • x_1).imI = (HSMul.hSMul (α := R) (↑x : R) x_1).imI
Tactic: ext