awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
r : R
q : ℍ[R]
⊢ (normSq : (a : ℍ[R]) → R) (r • q) = HMul.hMul (β := R) (HPow.hPow (β := ℕ) r 2) ((normSq : (a : ℍ[R]) → R) q : R)

Tactic:
simp only [normSq_def', re_smul, imI_smul, imJ_smul, imK_smul, mul_pow, mul_add, smul_eq_mul]

Premises used: Quaternion.imJ_smul, Quaternion.imI_smul, Quaternion.normSq_def', Quaternion.imK_smul, mul_add, Quaternion.re_smul, smul_eq_mul, mul_pow
-- Module: Mathlib.Algebra.Quaternion
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)
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)
⊢ (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)

Tactic:
simp_rw [normSq_def, star_add, add_mul, mul_add, re_add]

Premises used: add_mul, StarAddMonoid.star_add, Quaternion.normSq_def, Quaternion.re_add, mul_add
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_3
inst : CommRing R
a b : ℍ[R]
⊢ 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) =
    HAdd.hAdd (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) +
      ((a * star b).re + (b * star a).re)

Tactic:
abel
-- Module: Mathlib.Algebra.Quaternion
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
rw₃ 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
⊢ 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

Tactic:
rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]

Premises used: star_mul_star, Quaternion.self_add_star', Quaternion.re_coe, Quaternion.re_add
-- Module: Mathlib.Algebra.Quaternion
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

Tactic:
⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩

Premises used: Quaternion.normSq, Eq.rec, MonoidWithZeroHom.map_zero, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
refine : ∀ (h : Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R)), a = 0
⊢ Eq (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R) ↔ a = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩
-- Module: Mathlib.Algebra.Quaternion
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
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
⊢ 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

Premises used: add_eq_zero_iff_of_nonneg, Quaternion.normSq_def'
-- Module: Mathlib.Algebra.Quaternion
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₄ : a.imK = QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 0
⊢ a = 0

Tactic:
apply ext a 0

Premises used: Quaternion.ext, OfNat.ofNat
-- Module: Mathlib.Algebra.Quaternion
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₂ : ℕ
⊢ a.re = QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) 0

Tactic:
apply eq_zero_of_pow_eq_zero

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Algebra.Quaternion
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₂ : ℕ
⊢ a.imI = QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) 0

Tactic:
apply eq_zero_of_pow_eq_zero

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Algebra.Quaternion
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₂ : ℕ
⊢ a.imJ = QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) 0

Tactic:
apply eq_zero_of_pow_eq_zero

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Algebra.Quaternion
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₂ : ℕ
⊢ a.imK = QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) 0

Tactic:
apply eq_zero_of_pow_eq_zero

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Algebra.Quaternion
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
⊢ HPow.hPow (β := ℕ) a.re 2 = 0

Tactic:
h.1.1.1

Premises used: And.left
-- Module: Mathlib.Algebra.Quaternion
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
⊢ HPow.hPow (β := ℕ) a.imI 2 = 0

Tactic:
h.1.1.2

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Quaternion
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
⊢ HPow.hPow (β := ℕ) a.imJ 2 = 0

Tactic:
h.1.2

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Quaternion
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
⊢ HPow.hPow (β := ℕ) a.imK 2 = 0

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
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:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
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:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
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:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
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:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
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:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
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:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ Ne (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R) ↔ a ≠ 0

Tactic:
normSq_eq_zero.not

Premises used: Quaternion.normSq_eq_zero, Iff.not
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
rw :
  0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2
⊢ LE.le (α := R) (0 : R) ((normSq : (a : ℍ[R]) → R) a : R)

Tactic:
rw [normSq_def']

Premises used: Quaternion.normSq_def'
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ 0 ≤ HPow.hPow (β := ℕ) a.re 2 + HPow.hPow (β := ℕ) a.imI 2 + HPow.hPow (β := ℕ) a.imJ 2 + HPow.hPow (β := ℕ) a.imK 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Premises used: add_nonneg, sq_nonneg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ LE.le (α := R) ((normSq : (a : ℍ[R]) → R) a : R) (0 : R) ↔ a = 0

Tactic:
normSq_nonneg.ge_iff_eq'.trans normSq_eq_zero

Premises used: Quaternion.normSq_eq_zero, Quaternion.normSq_nonneg, LE.le.ge_iff_eq', Iff.trans
-- Module: Mathlib.Algebra.Quaternion
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
rwa : Eq (α := R) ((normSq : (a : ℍ[R]) → R) (a * b) : R) (0 : R)
rwa₁ rwa₂ rwa₃ rwa₄ : a * b = 0
⊢ HMul.hMul (α := R) (β := R) ((normSq : (a : ℍ[R]) → R) a : R) ((normSq : (a : ℍ[R]) → R) b : R) = 0

Tactic:
rwa [← map_mul, normSq_eq_zero]

Premises used: Quaternion.normSq_eq_zero, map_mul
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ IsDomain.{u_1} ℍ[R]

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
rw : star a = a ∨ a = 0 ↔ star a = a
⊢ HPow.hPow (β := ℕ) a 2 = (↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ a = (↑a.re : ℍ[R])

Tactic:
rw [← star_eq_self, ← star_mul_self, sq, mul_eq_mul_right_iff, eq_comm]

Premises used: Quaternion.star_mul_self, mul_eq_mul_right_iff, sq, eq_comm, Quaternion.star_eq_self
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a

Tactic:
or_iff_left_of_imp fun ha ↦ ha.symm ▸ star_zero _

Premises used: or_iff_left_of_imp, Eq.rec, star_zero, Eq.symm, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
⊢ star a = a ∨ a = 0 ↔ star a = a

Tactic:
exact or_iff_left_of_imp fun ha ↦ ha.symm ▸ star_zero _

Premises used: or_iff_left_of_imp
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℍ[R]
simp_rw : HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ a.re = 0

Tactic:
simp_rw [← star_eq_neg]

Premises used: Quaternion.star_eq_neg
-- Module: Mathlib.Algebra.Quaternion
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)
inr : ∀ (hq0 : a ≠ 0), HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a

Tactic:
obtain rfl | hq0 := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
⊢ HPow.hPow (α := ℍ[R]) (β := ℕ) 0 2 = -(↑((normSq : (a : ℍ[R]) → R) 0) : ℍ[R]) ↔ Eq.{u_1 + 1} (α := ℍ[R]) (star 0) (-0)

Tactic:
simp
-- Module: Mathlib.Algebra.Quaternion
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
inr₅ inr₆ : star a = -a ↔ star a = -a
⊢ HPow.hPow (β := ℕ) a 2 = -(↑((normSq : (a : ℍ[R]) → R) a) : ℍ[R]) ↔ star a = -a

Tactic:
rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]

Premises used: Quaternion.star_mul_self, Iff.mpr, neg_sq, sq, eq_comm, neg_ne_zero, mul_left_inj', mul_neg
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) (↑q : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := ℍ[R]) (im (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: Quaternion.im, QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) (↑q : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ
⊢ Eq.{u_1 + 1} (α := ℍ[R]) (im (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: Quaternion.im, QuaternionAlgebra.im, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) (↑q : ℍ[R])) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := ℍ[R]) (↑(↑q : R) : ℍ[R]) (↑q : ℍ[R])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
q : ℚ
⊢ Eq.{u_1 + 1} (α := ℍ[R]) (↑(↑q : R) : ℍ[R]) (↑q : ℍ[R])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := ℍ[R]) (↑(ofScientific m s e) : ℍ[R]) (ofScientific m s e)

Tactic:
rfl

Premises used: Quaternion.coe, QuaternionAlgebra.coe, rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.re (a := -1) (b := 0) (c := -1) (ofScientific m s e)) (ofScientific m s e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imI (a := -1) (b := 0) (c := -1) (ofScientific m s e)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imJ (a := -1) (b := 0) (c := -1) (ofScientific m s e)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := R) (QuaternionAlgebra.imK (a := -1) (b := 0) (c := -1) (ofScientific m s e)) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Quaternion
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := ℍ[R]) 0 0
⊢ Eq.{u_1 + 1} (α := ℍ[R]) 0⁻¹ 0

Tactic:
rw [inv_def, star_zero, smul_zero]

Premises used: Quaternion.inv_def, smul_zero, star_zero
-- Module: Mathlib.Algebra.Quaternion
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
rw₅ rw₆ : Eq.{u_1 + 1} (α := ℍ[R]) 1 1
⊢ a * 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]

Premises used: Iff.mpr, Algebra.mul_smul_comm, Quaternion.inv_def, Quaternion.normSq, Quaternion.smul_coe, Quaternion.coe_one, Inv.inv, Quaternion.self_mul_star, Quaternion.normSq_ne_zero, DFunLike.coe, inv_mul_cancel₀, Star.star
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ Eq (α := ℍ[R]) (↑x⁻¹ : ℍ[R]) (↑x : ℍ[R])⁻¹

Tactic:
map_inv₀ (algebraMap R ℍ[R]) _

Premises used: Quaternion.coe, Algebra.algebraMap, map_inv₀, QuaternionAlgebra.coe, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y : R
⊢ (↑(x / y) : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x : ℍ[R]) (↑y : ℍ[R])

Tactic:
map_div₀ (algebraMap R ℍ[R]) x y

Premises used: Quaternion.coe, Algebra.algebraMap, QuaternionAlgebra.coe, map_div₀, Quaternion
-- Module: Mathlib.Algebra.Quaternion
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
z : ℤ
⊢ (↑(x ^ z) : ℍ[R]) = HPow.hPow (α := ℍ[R]) (↑x : ℍ[R]) z

Tactic:
map_zpow₀ (algebraMap R ℍ[R]) x z

Premises used: Quaternion.coe, Algebra.algebraMap, QuaternionAlgebra.coe, map_zpow₀, Quaternion
-- Module: Mathlib.Algebra.Quaternion
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])
rw₄ rw₅ : HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])
⊢ (↑x : ℍ[R]) = HDiv.hDiv (α := ℍ[R]) (↑x.num : ℍ[R]) (↑x.den : ℍ[R])

Tactic:
rw [← coe_nnratCast, NNRat.cast_def, coe_div, coe_natCast, coe_natCast]

Premises used: Quaternion.coe_natCast, NNRat.cast_def, Quaternion.coe_div, Quaternion.coe_nnratCast