ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>self : ℍ[R,c₁,c₂]<GOAL>(QuaternionAlgebra.imKₗ c₁ c₂) self = self.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>⇑(QuaternionAlgebra.linearEquivTuple c₁ c₂) = ⇑(QuaternionAlgebra.equivTuple c₁ c₂)
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>⇑(QuaternionAlgebra.linearEquivTuple c₁ c₂).symm = ⇑(QuaternionAlgebra.equivTuple c₁ c₂).symm
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>q : ℍ[R,c₁,c₂]<GOAL>⇑((QuaternionAlgebra.basisOneIJK c₁ c₂).repr q) = ![q.re, q.imI, q.imJ, q.imK]
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>StrongRankCondition R<GOAL>Module.rank R ℍ[R,c₁,c₂] = 4
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>StrongRankCondition R<GOAL>FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₂,c₁]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).imJ = t.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₁,c₂]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂) t).imI = t.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₁,c₂]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂) t).imK = -t.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₁,c₂]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂) t).re = t.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₂,c₁]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).imI = t.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₁,c₂]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂) t).imJ = t.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₂,c₁]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).re = t.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>t : ℍ[R,c₂,c₁]<GOAL>((QuaternionAlgebra.swapEquiv c₁ c₂).symm t).imK = -t.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x y : R<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>r : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>↑r * a = a * ↑r
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>r : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>Commute (↑r) a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>r : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>↑r * a = r • a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>r : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a * ↑r = r • a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>⇑(algebraMap R ℍ[R,c₁,c₂]) = QuaternionAlgebra.coe
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x y : R<GOAL>x • ↑y = ↑(x * y)
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(star a).re = a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(star a).imI = -a.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(star a).imJ = -a.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(star a).imK = -a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>(star a).im = -a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a₁ a₂ a₃ a₄ : R<GOAL>star { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a + star a = ↑(2 * a.re)
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a + star a = 2 * ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a + a = ↑(2 * a.re)
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a + a = 2 * ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a = ↑(2 * a.re) - a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>x : R<GOAL>star ↑x = ↑x
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a.im = -a.im
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>Monoid S<VAR>DistribMulAction S R<VAR>s : S<VAR>a : ℍ[R,c₁,c₂]<GOAL>star (s • a) = s • star a
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<VAR>x : R<VAR>h : a = ↑x<GOAL>a = ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a = ↑a.re ↔ a ∈ Set.range QuaternionAlgebra.coe
<VAR>R : Type u_3<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a = a ↔ a = ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a = -a ↔ a.re = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>star a * a = ↑(star a * a).re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : ℍ[R,c₁,c₂]<GOAL>a * star a = ↑(a * star a).re
<VAR>R : Type u_3<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>⇑QuaternionAlgebra.starAe = MulOpposite.op ∘ star
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>a : R × R × R × R<GOAL>((Quaternion.equivProd R).symm a).imI = a.2.1
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>a : R × R × R × R<GOAL>((Quaternion.equivProd R).symm a).imJ = a.2.2.1
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>a : R × R × R × R<GOAL>((Quaternion.equivProd R).symm a).re = a.1
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>a : R × R × R × R<GOAL>((Quaternion.equivProd R).symm a).imK = a.2.2.2
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>a : ℍ[R,-1,-1]<GOAL>(Quaternion.equivProd R) a = (a.re, a.imI, a.imJ, a.imK)
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>a : Fin 4 → R<GOAL>(Quaternion.equivTuple R).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>x : ℍ[R]<GOAL>(Quaternion.equivTuple R) x = ![x.re, x.imI, x.imJ, x.imK]
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>a = b ↔ a.re = b.re ∧ a.imI = b.imI ∧ a.imJ = b.imJ ∧ a.imK = b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a.im.re = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a.im.imI = a.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a.im.imJ = a.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a.im.imK = a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a.im.im = a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>↑a.re + a.im = a
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a - a.im = ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a - ↑a.re = a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>(↑x).re = x
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>(↑x).imI = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>(↑x).imJ = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>(↑x).imK = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>(↑x).im = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.re 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.imI 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.imJ 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.imK 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.im 0 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>↑0 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.re 1 = 1
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.imI 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.imJ 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.imK 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Quaternion.im 1 = 0
<VAR>R : Type u_3<VAR>CommRing R<GOAL>↑1 = 1
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a + b).re = a.re + b.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a + b).imI = a.imI + b.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a + b).imJ = a.imJ + b.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a + b).imK = a.imK + b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a + b).im = a.im + b.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>x y : R<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(-a).re = -a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(-a).imI = -a.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(-a).imJ = -a.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(-a).imK = -a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(-a).im = -a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>↑(-x) = -↑x
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a - b).re = a.re - b.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a - b).imI = a.imI - b.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a - b).imJ = a.imJ - b.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a - b).imK = a.imK - b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a - b).im = a.im - b.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>x y : R<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>(a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>x y : R<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>(↑n).re = ↑n
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>(↑n).imI = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>(↑n).imJ = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>(↑n).imK = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>(↑n).im = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>(↑z).re = ↑z
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>(↑z).imI = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>(↑z).imJ = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>(↑z).imK = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>(↑z).im = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>↑↑z = ↑z
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Function.Injective Quaternion.coe
<VAR>R : Type u_3<VAR>CommRing R<VAR>x y : R<GOAL>↑x = ↑y ↔ x = y
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).re = s • a.re
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).imI = s • a.imI
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).imJ = s • a.imJ
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<VAR>SMul S R<VAR>s : S<GOAL>(s • a).imK = s • a.imK
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<VAR>SMulZeroClass S R<VAR>s : S<GOAL>(s • a).im = s • a.im
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>SMulZeroClass S R<VAR>s : S<VAR>r : R<GOAL>↑(s • r) = s • ↑r
<VAR>R : Type u_3<VAR>CommRing R<VAR>r : R<VAR>a : ℍ[R]<GOAL>↑r * a = a * ↑r
<VAR>R : Type u_3<VAR>CommRing R<VAR>r : R<VAR>a : ℍ[R]<GOAL>Commute (↑r) a
<VAR>R : Type u_3<VAR>CommRing R<VAR>r : R<VAR>a : ℍ[R]<GOAL>↑r * a = r • a
<VAR>R : Type u_3<VAR>CommRing R<VAR>r : R<VAR>a : ℍ[R]<GOAL>a * ↑r = r • a
<VAR>R : Type u_3<VAR>CommRing R<GOAL>⇑(algebraMap R ℍ[R]) = Quaternion.coe
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Function.Injective ⇑(algebraMap R ℍ[R])
<VAR>R : Type u_3<VAR>CommRing R<VAR>x y : R<GOAL>x • ↑y = ↑(x * y)
<VAR>R : Type u_3<VAR>CommRing R<VAR>StrongRankCondition R<GOAL>Module.rank R ℍ[R] = 4
<VAR>R : Type u_3<VAR>CommRing R<VAR>StrongRankCondition R<GOAL>FiniteDimensional.finrank R ℍ[R] = 4
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(star a).re = a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(star a).imI = -a.imI
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(star a).imJ = -a.imJ
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(star a).imK = -a.imK
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>(star a).im = -a.im
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a + star a = ↑(2 * a.re)
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a + star a = 2 * ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>star a + a = ↑(2 * a.re)
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>star a + a = 2 * ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>star a = ↑(2 * a.re) - a
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>star ↑x = ↑x
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>star a.im = -a.im
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommRing R<VAR>Monoid S<VAR>DistribMulAction S R<VAR>s : S<VAR>a : ℍ[R]<GOAL>star (s • a) = s • star a
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<VAR>x : R<VAR>h : a = ↑x<GOAL>a = ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a = ↑a.re ↔ a ∈ Set.range Quaternion.coe
<VAR>R : Type u_3<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>a : ℍ[R]<GOAL>star a = a ↔ a = ↑a.re
<VAR>R : Type u_3<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>a : ℍ[R]<GOAL>star a = -a ↔ a.re = 0
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>star a * a = ↑(star a * a).re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a * star a = ↑(a * star a).re
<VAR>R : Type u_3<VAR>CommRing R<GOAL>⇑Quaternion.starAe = MulOpposite.op ∘ star
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq a = (a * star a).re
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
<VAR>R : Type u_3<VAR>CommRing R<VAR>x : R<GOAL>Quaternion.normSq ↑x = x ^ 2
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq (star a) = Quaternion.normSq a
<VAR>R : Type u_3<VAR>CommRing R<VAR>n : ℕ<GOAL>Quaternion.normSq ↑n = ↑n ^ 2
<VAR>R : Type u_3<VAR>CommRing R<VAR>z : ℤ<GOAL>Quaternion.normSq ↑z = ↑z ^ 2
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq (-a) = Quaternion.normSq a
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a * star a = ↑(Quaternion.normSq a)
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>star a * a = ↑(Quaternion.normSq a)
<VAR>R : Type u_3<VAR>CommRing R<VAR>a : ℍ[R]<GOAL>a.im ^ 2 = -↑(Quaternion.normSq a.im)
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>↑(Quaternion.normSq (a + b)) = ↑(Quaternion.normSq a) + a * star b + b * star a + ↑(Quaternion.normSq b)
<VAR>R : Type u_3<VAR>CommRing R<VAR>r : R<VAR>q : ℍ[R]<GOAL>Quaternion.normSq (r • q) = r ^ 2 * Quaternion.normSq q
<VAR>R : Type u_3<VAR>CommRing R<VAR>a b : ℍ[R]<GOAL>Quaternion.normSq (a + b) = Quaternion.normSq a + Quaternion.normSq b + 2 * (a * star b).re
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq a ≠ 0 ↔ a ≠ 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>0 ≤ Quaternion.normSq a
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq a ≤ 0 ↔ a = 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>a ^ 2 = ↑(Quaternion.normSq a) ↔ a = ↑a.re
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>a ^ 2 = -↑(Quaternion.normSq a) ↔ a.re = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>a : ℍ[R]<GOAL>a⁻¹ = (Quaternion.normSq a)⁻¹ • star a
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>x : R<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>x y : R<GOAL>↑(x / y) = ↑x / ↑y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>x : R<VAR>z : ℤ<GOAL>↑(x ^ z) = ↑x ^ z
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ≥0<GOAL>(↑q).re = ↑q
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ≥0<GOAL>(↑q).im = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ≥0<GOAL>(↑q).imI = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ≥0<GOAL>(↑q).imJ = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ≥0<GOAL>(↑q).imK = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>(↑q).re = ↑q
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>(↑q).im = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>(↑q).imI = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>(↑q).imJ = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>(↑q).imK = 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>↑↑q = ↑q
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>a : ℍ[R]<GOAL>Quaternion.normSq a⁻¹ = (Quaternion.normSq a)⁻¹
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>a b : ℍ[R]<GOAL>Quaternion.normSq (a / b) = Quaternion.normSq a / Quaternion.normSq b
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>a : ℍ[R]<VAR>z : ℤ<GOAL>Quaternion.normSq (a ^ z) = Quaternion.normSq a ^ z
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>q : ℚ<GOAL>↑(Quaternion.normSq ↑q) = ↑q ^ 2
<VAR>R : Type u_1<VAR>Infinite R<GOAL>Cardinal.mk R ^ 4 = Cardinal.mk R
<VAR>R : Type u_1<VAR>c₁ c₂ : R<GOAL>Cardinal.mk ℍ[R,c₁,c₂] = Cardinal.mk R ^ 4
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>Infinite R<GOAL>Cardinal.mk ℍ[R,c₁,c₂] = Cardinal.mk R
<VAR>R : Type u_1<VAR>c₁ c₂ : R<GOAL>Cardinal.mk ↑Set.univ = Cardinal.mk R ^ 4
<VAR>R : Type u_1<VAR>c₁ c₂ : R<VAR>Infinite R<GOAL>Cardinal.mk ↑Set.univ = Cardinal.mk R
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<GOAL>Cardinal.mk ℍ[R] = Cardinal.mk R ^ 4
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>Infinite R<GOAL>Cardinal.mk ℍ[R] = Cardinal.mk R
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<GOAL>Cardinal.mk ↑Set.univ = Cardinal.mk R ^ 4
<VAR>R : Type u_1<VAR>One R<VAR>Neg R<VAR>Infinite R<GOAL>Cardinal.mk ↑Set.univ = Cardinal.mk R
<VAR>α : Sort u_3<VAR>s t : Setoid α<GOAL>(∀ (a b : α), Setoid.r a b ↔ Setoid.r a b) → s = t
<VAR>α : Sort u_4<VAR>r : α → α → Prop<VAR>β : Quot r → Prop<VAR>q : Quot r<VAR>h : ∀ (a : α), β (Quot.mk r a)<GOAL>β q
<VAR>α : Type u_4<VAR>r s : α → α → Prop<VAR>h : ∀ (x y : α), r x y → s x y<GOAL>Quot.factor r s h ∘ Quot.mk r = Quot.mk s
<VAR>α : Sort u_1<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>f : α → γ<VAR>h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂<VAR>a : α<GOAL>Quot.lift f h (Quot.mk r a) = f a
<VAR>α : Sort u_1<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>a : α<VAR>f : α → γ<VAR>h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂<GOAL>(Quot.mk r a).liftOn f h = f a
<VAR>α : Sort u_1<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>f : α → γ<VAR>h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂<GOAL>Function.Surjective (Quot.lift f h) ↔ Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α → β → γ<VAR>hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂<VAR>hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b<VAR>a : α<VAR>b : β<GOAL>Quot.lift₂ f hr hs (Quot.mk r a) (Quot.mk s b) = f a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>a : α<VAR>b : β<VAR>f : α → β → γ<VAR>hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂<VAR>hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b<GOAL>(Quot.mk r a).liftOn₂ (Quot.mk s b) f hr hs = f a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : α → β → γ<VAR>hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → t (f a b₁) (f a b₂)<VAR>hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → t (f a₁ b) (f a₂ b)<VAR>a : α<VAR>b : β<GOAL>Quot.map₂ f hr hs (Quot.mk r a) (Quot.mk s b) = Quot.mk t (f a b)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>δ : Quot r → Quot s → Prop<VAR>q₁ : Quot r<VAR>q₂ : Quot s<VAR>h : ∀ (a : α) (b : β), δ (Quot.mk r a) (Quot.mk s b)<GOAL>δ q₁ q₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>δ : Quot r → Quot s → Quot t → Prop<VAR>q₁ : Quot r<VAR>q₂ : Quot s<VAR>q₃ : Quot t<VAR>h : ∀ (a : α) (b : β) (c : γ), δ (Quot.mk r a) (Quot.mk s b) (Quot.mk t c)<GOAL>δ q₁ q₂ q₃
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>sa : Setoid α<VAR>sb : Setoid β<VAR>f : α → β<VAR>h : ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) f f<VAR>x : α<GOAL>Quotient.map f h ⟦x⟧ = ⟦f x⟧
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>sa : Setoid α<VAR>sb : Setoid β<VAR>γ : Sort u_4<VAR>sc : Setoid γ<VAR>f : α → β → γ<VAR>h : ((fun x x_1 => x ≈ x_1) ⇒ (fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) f f<VAR>x : α<VAR>y : β<GOAL>Quotient.map₂ f h ⟦x⟧ ⟦y⟧ = ⟦f x y⟧
<VAR>α : Type u_3<VAR>r : α → α → Prop<VAR>x y : α<GOAL>Quot.mk r x = Quot.mk r y ↔ EqvGen r x y
<VAR>α : Sort u_1<VAR>r : Setoid α<VAR>x y : α<GOAL>⟦x⟧ = ⟦y⟧ ↔ x ≈ y
<VAR>α : Sort u_3<VAR>s : Setoid α<VAR>p : Quotient s → Prop<GOAL>(∀ (a : Quotient s), p a) ↔ ∀ (a : α), p ⟦a⟧
<VAR>α : Sort u_3<VAR>s : Setoid α<VAR>p : Quotient s → Prop<GOAL>(∃ a, p a) ↔ ∃ a, p ⟦a⟧
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>f : α → β<VAR>h : ∀ (a b : α), a ≈ b → f a = f b<VAR>x : α<GOAL>Quotient.lift f h ⟦x⟧ = f x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Setoid α<VAR>f : α → β<VAR>h : ∀ (a b : α), a ≈ b → f a = f b<GOAL>Quotient.lift f h ∘ Quotient.mk inst✝ = f
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>γ : Sort u_5<VAR>Setoid α<VAR>Setoid β<VAR>f : α → β → γ<VAR>h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂<VAR>a : α<VAR>b : β<GOAL>Quotient.lift₂ f h ⟦a⟧ ⟦b⟧ = f a b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>f : α → β<VAR>h : ∀ (a b : α), a ≈ b → f a = f b<VAR>x : α<GOAL>⟦x⟧.liftOn f h = f x
<VAR>α : Sort u_3<VAR>β : Sort u_4<VAR>Setoid α<VAR>f : α → α → β<VAR>h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂<VAR>x y : α<GOAL>⟦x⟧.liftOn₂ ⟦y⟧ f h = f x y
<VAR>α : Sort u_1<VAR>r : α → α → Prop<GOAL>Function.Surjective (Quot.mk r)
<VAR>α : Sort u_3<VAR>s : Setoid α<GOAL>Function.Surjective (Quotient.mk s)
<VAR>α : Sort u_3<VAR>s : Setoid α<GOAL>Function.Surjective Quotient.mk'
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>q : Quot r<GOAL>Quot.mk r q.out = q
<VAR>α : Sort u_1<VAR>s : Setoid α<VAR>q : Quotient s<GOAL>⟦q.out⟧ = q
<VAR>α : Sort u_1<VAR>Setoid α<VAR>a : α<GOAL>⟦a⟧.out ≈ a
<VAR>α : Sort u_1<VAR>s : Setoid α<VAR>x : α<VAR>y : Quotient s<GOAL>⟦x⟧ = y ↔ x ≈ y.out
<VAR>α : Sort u_1<VAR>s : Setoid α<VAR>x : Quotient s<VAR>y : α<GOAL>x = ⟦y⟧ ↔ x.out ≈ y
<VAR>α : Sort u_1<VAR>s : Setoid α<VAR>x y : Quotient s<GOAL>x.out ≈ y.out ↔ x = y
<VAR>α : Sort u_1<VAR>s : Setoid α<GOAL>Function.Injective Quotient.out
<VAR>α : Sort u_1<VAR>s : Setoid α<VAR>x y : Quotient s<GOAL>x.out = y.out ↔ x = y
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Setoid (α i)<VAR>f : (i : ι) → α i<GOAL>(Quotient.choice fun i => ⟦f i⟧) = ⟦f⟧
<VAR>ι : Type u_3<VAR>α : ι → Sort u_4<VAR>s : (i : ι) → Setoid (α i)<VAR>p : ((i : ι) → Quotient (s i)) → Prop<VAR>f : (i : ι) → Quotient (s i)<VAR>h : ∀ (a : (i : ι) → α i), p fun i => ⟦a i⟧<GOAL>p f
<VAR>α : Sort u_1<VAR>s : Setoid α<GOAL>Nonempty (Quotient s) ↔ Nonempty α
<VAR>α : Sort u_1<GOAL>Equivalence fun x x => True
<VAR>α : Sort u_1<VAR>β : Trunc α → Prop<GOAL>(∀ (a : α), β (Trunc.mk a)) → ∀ (q : Trunc α), β q
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>c : ∀ (a b : α), f a = f b<VAR>a : α<GOAL>Trunc.lift f c (Trunc.mk a) = f a
<VAR>α : Sort u_1<VAR>β : Trunc α → Prop<VAR>q : Trunc α<VAR>h : ∀ (a : α), β (Trunc.mk a)<GOAL>β q
<VAR>α : Sort u_1<VAR>q : Trunc α<GOAL>∃ a, Trunc.mk a = q
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>C : Trunc α → Trunc β → Prop<VAR>q₁ : Trunc α<VAR>q₂ : Trunc β<VAR>h : ∀ (a : α) (b : β), C (Trunc.mk a) (Trunc.mk b)<GOAL>C q₁ q₂
<VAR>α : Sort u_1<VAR>a b : Trunc α<GOAL>a = b
<VAR>α : Sort u_1<VAR>q : Trunc α<GOAL>Trunc.mk q.out = q
<VAR>α : Sort u_1<VAR>q : Trunc α<GOAL>Nonempty α
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<GOAL>Function.Surjective Quotient.mk''
<VAR>α : Sort u_1<VAR>φ : Sort u_4<VAR>s₁ : Setoid α<VAR>f : α → φ<VAR>h : ∀ (a b : α), Setoid.r a b → f a = f b<VAR>x : α<GOAL>(Quotient.mk'' x).liftOn' f h = f x
<VAR>α : Sort u_1<VAR>φ : Sort u_4<VAR>s₁ : Setoid α<VAR>f : α → φ<VAR>h : ∀ (a b : α), Setoid.r a b → f a = f b<GOAL>(Function.Surjective fun x => x.liftOn' f h) ↔ Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>s₁ : Setoid α<VAR>s₂ : Setoid β<VAR>f : α → β → γ<VAR>h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁ → Setoid.r a₂ b₂ → f a₁ a₂ = f b₁ b₂<VAR>a : α<VAR>b : β<GOAL>(Quotient.mk'' a).liftOn₂' (Quotient.mk'' b) f h = f a b
<VAR>α : Sort u_1<VAR>s₁ : Setoid α<VAR>p : Quotient s₁ → Prop<VAR>h : ∀ (a : α), p (Quotient.mk'' a)<VAR>q : Quotient s₁<GOAL>p q