ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℝ<GOAL>Real.sin x ^ 2 = 1 - Real.cos x ^ 2
<VAR>x : ℝ<GOAL>Real.sin x ^ 2 = 1 / 2 - Real.cos (2 * x) / 2
<VAR>x : ℝ<GOAL>|Real.sin x| = √(1 - Real.cos x ^ 2)
<VAR>x : ℝ<GOAL>|Real.cos x| = √(1 - Real.sin x ^ 2)
<VAR>x : ℝ<VAR>hx : Real.cos x ≠ 0<GOAL>(1 + Real.tan x ^ 2)⁻¹ = Real.cos x ^ 2
<VAR>x : ℝ<VAR>hx : Real.cos x ≠ 0<GOAL>Real.tan x ^ 2 / (1 + Real.tan x ^ 2) = Real.sin x ^ 2
<VAR>x : ℝ<VAR>hx : 0 < Real.cos x<GOAL>(√(1 + Real.tan x ^ 2))⁻¹ = Real.cos x
<VAR>x : ℝ<VAR>hx : 0 < Real.cos x<GOAL>Real.tan x / √(1 + Real.tan x ^ 2) = Real.sin x
<VAR>x : ℝ<GOAL>Real.cos (3 * x) = 4 * Real.cos x ^ 3 - 3 * Real.cos x
<VAR>x : ℝ<GOAL>Real.sin (3 * x) = 3 * Real.sin x - 4 * Real.sin x ^ 3
<VAR>x : ℝ<GOAL>Real.sinh x = (Real.exp x - Real.exp (-x)) / 2
<VAR>x : ℝ<GOAL>Real.sinh (-x) = -Real.sinh x
<VAR>x y : ℝ<GOAL>Real.sinh (x + y) = Real.sinh x * Real.cosh y + Real.cosh x * Real.sinh y
<VAR>x : ℝ<GOAL>Real.cosh x = (Real.exp x + Real.exp (-x)) / 2
<VAR>x : ℝ<GOAL>Real.cosh (-x) = Real.cosh x
<VAR>x : ℝ<GOAL>Real.cosh |x| = Real.cosh x
<VAR>x y : ℝ<GOAL>Real.cosh (x + y) = Real.cosh x * Real.cosh y + Real.sinh x * Real.sinh y
<VAR>x y : ℝ<GOAL>Real.sinh (x - y) = Real.sinh x * Real.cosh y - Real.cosh x * Real.sinh y
<VAR>x y : ℝ<GOAL>Real.cosh (x - y) = Real.cosh x * Real.cosh y - Real.sinh x * Real.sinh y
<VAR>x : ℝ<GOAL>Real.tanh x = Real.sinh x / Real.cosh x
<VAR>x : ℝ<GOAL>Real.tanh (-x) = -Real.tanh x
<VAR>x : ℝ<GOAL>Real.cosh x + Real.sinh x = Real.exp x
<VAR>x : ℝ<GOAL>Real.sinh x + Real.cosh x = Real.exp x
<VAR>x : ℝ<GOAL>Real.exp x - Real.cosh x = Real.sinh x
<VAR>x : ℝ<GOAL>Real.exp x - Real.sinh x = Real.cosh x
<VAR>x : ℝ<GOAL>Real.cosh x - Real.sinh x = Real.exp (-x)
<VAR>x : ℝ<GOAL>Real.sinh x - Real.cosh x = -Real.exp (-x)
<VAR>x : ℝ<GOAL>Real.cosh x ^ 2 - Real.sinh x ^ 2 = 1
<VAR>x : ℝ<GOAL>Real.cosh x ^ 2 = Real.sinh x ^ 2 + 1
<VAR>x : ℝ<GOAL>Real.cosh x ^ 2 = 1 + Real.sinh x ^ 2
<VAR>x : ℝ<GOAL>Real.sinh x ^ 2 = Real.cosh x ^ 2 - 1
<VAR>x : ℝ<GOAL>Real.cosh (2 * x) = Real.cosh x ^ 2 + Real.sinh x ^ 2
<VAR>x : ℝ<GOAL>Real.sinh (2 * x) = 2 * Real.sinh x * Real.cosh x
<VAR>x : ℝ<GOAL>Real.cosh (3 * x) = 4 * Real.cosh x ^ 3 - 3 * Real.cosh x
<VAR>x : ℝ<GOAL>Real.sinh (3 * x) = 4 * Real.sinh x ^ 3 + 3 * Real.sinh x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i / ↑i.factorial ≤ Real.exp x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>n : ℕ<GOAL>x ^ n / ↑n.factorial ≤ Real.exp x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>1 + x + x ^ 2 / 2 ≤ Real.exp x
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>x + 1 < Real.exp x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>x + 1 ≤ Real.exp x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>1 ≤ Real.exp x
<VAR>x : ℝ<GOAL>0 < Real.exp x
<VAR>x : ℝ<GOAL>0 ≤ Real.exp x
<VAR>x : ℝ<GOAL>|Real.exp x| = Real.exp x
<VAR>x : ℝ<GOAL>Real.exp |x| ≤ Real.exp x + Real.exp (-x)
<VAR>x y : ℝ<VAR>h : x < y<GOAL>Real.exp x < Real.exp y
<VAR>x y : ℝ<VAR>h : x ≤ y<GOAL>Real.exp x ≤ Real.exp y
<VAR>x y : ℝ<GOAL>Real.exp x < Real.exp y ↔ x < y
<VAR>x y : ℝ<GOAL>Real.exp x ≤ Real.exp y ↔ x ≤ y
<VAR>x y : ℝ<GOAL>Real.exp x = Real.exp y ↔ x = y
<VAR>x : ℝ<GOAL>Real.exp x = 1 ↔ x = 0
<VAR>x : ℝ<GOAL>1 < Real.exp x ↔ 0 < x
<VAR>x : ℝ<GOAL>Real.exp x < 1 ↔ x < 0
<VAR>x : ℝ<GOAL>Real.exp x ≤ 1 ↔ x ≤ 0
<VAR>x : ℝ<GOAL>1 ≤ Real.exp x ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>0 < Real.cosh x
<VAR>x : ℝ<GOAL>Real.sinh x < Real.cosh x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<GOAL>∑ m ∈ Finset.filter (fun k => n ≤ k) (Finset.range j), 1 / ↑m.factorial ≤ ↑n.succ / (↑n.factorial * ↑n)
<VAR>x : ℂ<VAR>hx : Complex.abs x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Complex.abs (Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial) ≤ Complex.abs x ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : Complex.abs x / ↑n.succ ≤ 1 / 2<GOAL>Complex.abs (Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial) ≤ Complex.abs x ^ n / ↑n.factorial * 2
<VAR>x : ℂ<VAR>hx : Complex.abs x ≤ 1<GOAL>Complex.abs (Complex.exp x - 1) ≤ 2 * Complex.abs x
<VAR>x : ℂ<VAR>hx : Complex.abs x ≤ 1<GOAL>Complex.abs (Complex.exp x - 1 - x) ≤ Complex.abs x ^ 2
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>|Real.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Real.exp x ≤ ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|Real.exp x - 1| ≤ 2 * |x|
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|Real.exp x - 1 - x| ≤ x ^ 2
<VAR>x r : ℝ<GOAL>Real.expNear 0 x r = r
<VAR>n : ℕ<VAR>x r : ℝ<GOAL>Real.expNear (n + 1) x r = Real.expNear n x (1 + x / (↑n + 1) * r)
<VAR>n : ℕ<VAR>x r₁ r₂ : ℝ<GOAL>Real.expNear n x r₁ - Real.expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)
<VAR>n m : ℕ<VAR>x : ℝ<VAR>e₁ : n + 1 = m<VAR>h : |x| ≤ 1<GOAL>|Real.exp x - Real.expNear m x 0| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)
<VAR>n : ℕ<VAR>x a₁ b₁ : ℝ<VAR>m : ℕ<VAR>e₁ : n + 1 = m<VAR>a₂ b₂ : ℝ<VAR>e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂<VAR>h : |Real.exp x - Real.expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂<GOAL>|Real.exp x - Real.expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
<VAR>n : ℕ<VAR>x a b : ℝ<VAR>m : ℕ<VAR>e₁ : n + 1 = m<VAR>rm : ℝ<VAR>er : ↑m = rm<VAR>h : |x| ≤ 1<VAR>e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)<GOAL>|Real.exp x - Real.expNear n x a| ≤ |x| ^ n / ↑n.factorial * b
<VAR>n : ℕ<VAR>a₁ b₁ : ℝ<VAR>m : ℕ<VAR>en : n + 1 = m<VAR>rm : ℝ<VAR>er : ↑m = rm<VAR>h : |Real.exp 1 - Real.expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)<GOAL>|Real.exp 1 - Real.expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁
<VAR>x a b : ℝ<VAR>h : |Real.exp x - Real.expNear 0 x a| ≤ |x| ^ 0 / ↑(Nat.factorial 0) * b<GOAL>|Real.exp x - a| ≤ b
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|Real.cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>|Real.sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 4 * (5 / 96)
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<GOAL>0 < Real.cos x
<VAR>x : ℝ<VAR>hx0 : 0 < x<VAR>hx : x ≤ 1<GOAL>0 < Real.sin x
<VAR>x : ℝ<VAR>hx0 : 0 < x<VAR>hx : x ≤ 2<GOAL>0 < Real.sin x
<VAR>x : ℝ<VAR>h1 : 0 < x<VAR>h2 : x < 1<GOAL>Real.exp x < 1 / (1 - x)
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x < 1<GOAL>Real.exp x ≤ 1 / (1 - x)
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>x + 1 < Real.exp x
<VAR>x : ℝ<GOAL>x + 1 ≤ Real.exp x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>1 - x < Real.exp (-x)
<VAR>x : ℝ<GOAL>1 - x ≤ Real.exp (-x)
<VAR>n : ℕ<VAR>t : ℝ<VAR>ht' : t ≤ ↑n<GOAL>(1 - t / ↑n) ^ n ≤ Real.exp (-t)
<VAR>x : ℝ<GOAL>Complex.abs (Complex.cos ↑x + Complex.sin ↑x * Complex.I) = 1
<VAR>x : ℝ<GOAL>Complex.abs (Complex.exp ↑x) = Real.exp x
<VAR>x : ℝ<GOAL>Complex.abs (Complex.exp (↑x * Complex.I)) = 1
<VAR>z : ℂ<GOAL>Complex.abs (Complex.exp z) = Real.exp z.re
<VAR>x y : ℂ<GOAL>Complex.abs (Complex.exp x) = Complex.abs (Complex.exp y) ↔ x.re = y.re
<VAR>α : Type u_1<VAR>One α<VAR>Add α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>One α<VAR>Add α<GOAL>↑PosNum.one = 1
<VAR>α : Type u_1<VAR>One α<VAR>Add α<VAR>n : PosNum<GOAL>↑n.bit0 = ↑n + ↑n
<VAR>α : Type u_1<VAR>One α<VAR>Add α<VAR>n : PosNum<GOAL>↑n.bit1 = ↑n + ↑n + 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : PosNum<GOAL>↑↑n = ↑n
<VAR>n : PosNum<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : PosNum<GOAL>↑↑n = ↑n
<VAR>n : PosNum<GOAL>↑n.succ = ↑n + 1
<VAR>n : PosNum<GOAL>1 + n = n.succ
<VAR>n : PosNum<GOAL>n + 1 = n.succ
<VAR>m n : PosNum<GOAL>↑(m + n) = ↑m + ↑n
<VAR>m n : PosNum<GOAL>m + n.succ = (m + n).succ
<VAR>n : PosNum<GOAL>n + n = n.bit0
<VAR>n : PosNum<GOAL>n + n + 1 = n.bit1
<VAR>m n : PosNum<GOAL>↑(m * n) = ↑m * ↑n
<VAR>m n : PosNum<GOAL>↑m < ↑n → ↑m.bit1 < ↑n.bit0
<VAR>m n : PosNum<GOAL>(m.cmp n).swap = n.cmp m
<VAR>m n : PosNum<GOAL>Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
<VAR>m n : PosNum<GOAL>↑m < ↑n ↔ m < n
<VAR>m n : PosNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>n : Num<GOAL>n + 1 = n.succ
<VAR>m n : Num<GOAL>m + n.succ = (m + n).succ
<VAR>n : Num<GOAL>n + n + 1 = n.bit1
<VAR>b : Bool<VAR>n : ℕ<GOAL>Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)
<VAR>n : Num<GOAL>n.bit1.succ = n.succ.bit0
<VAR>n : ℕ<GOAL>Num.ofNat' (n + 1) = Num.ofNat' n + 1
<VAR>m n : ℕ<GOAL>Num.ofNat' (m + n) = Num.ofNat' m + Num.ofNat' n
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<GOAL>↑Num.zero = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>n : PosNum<GOAL>↑(Num.pos n) = ↑n
<VAR>n : Num<GOAL>↑n.succ' = ↑n + 1
<VAR>n : Num<GOAL>↑n.succ = ↑n + 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : Num<GOAL>↑↑n = ↑n
<VAR>m n : Num<GOAL>↑(m + n) = ↑m + ↑n
<VAR>m n : Num<GOAL>↑(m * n) = ↑m * ↑n
<VAR>m n : Num<GOAL>Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
<VAR>m n : Num<GOAL>↑m < ↑n ↔ m < n
<VAR>m n : Num<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>n : PosNum<GOAL>Num.ofNat' ↑n = Num.pos n
<VAR>n : Num<GOAL>Num.ofNat' ↑n = n
<VAR>m n : Num<GOAL>↑m = ↑n ↔ m = n
<VAR>n : Num<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : Num<GOAL>↑↑n = ↑n
<VAR>n : ℕ<GOAL>↑↑n = n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>m n : Num<GOAL>↑m ∣ ↑n ↔ m ∣ n
<VAR>n : PosNum<GOAL>↑↑n = Num.pos n
<VAR>m n : PosNum<GOAL>↑m = ↑n ↔ m = n
<VAR>n : PosNum<GOAL>↑n.pred' = (↑n).pred
<VAR>n : Num<GOAL>n.succ'.pred' = n
<VAR>n : PosNum<GOAL>n.pred'.succ' = n
<VAR>m n : PosNum<GOAL>↑m ∣ ↑n ↔ m ∣ n
<VAR>n : PosNum<GOAL>↑n.size = (↑n).size
<VAR>n : PosNum<GOAL>↑n.size = n.natSize
<VAR>n : PosNum<GOAL>n.natSize = (↑n).size
<VAR>n : PosNum<GOAL>↑n = Num.pos n
<VAR>b : Bool<VAR>n : PosNum<GOAL>↑(PosNum.bit b n) = Nat.bit b ↑n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>m n : PosNum<GOAL>↑(m + n) = ↑m + ↑n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : PosNum<GOAL>↑n.succ = ↑n + 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>CharZero α<VAR>m n : PosNum<GOAL>↑m = ↑n ↔ m = n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>n : PosNum<GOAL>1 ≤ ↑n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>n : PosNum<GOAL>0 < ↑n
<VAR>α : Type u_1<VAR>Semiring α<VAR>m n : PosNum<GOAL>↑(m * n) = ↑m * ↑n
<VAR>m n : PosNum<GOAL>m.cmp n = Ordering.eq ↔ m = n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>m n : PosNum<GOAL>↑m < ↑n ↔ m < n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>m n : PosNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>b : Bool<VAR>n : Num<GOAL>↑(Num.bit b n) = Nat.bit b ↑n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : Num<GOAL>↑n.succ' = ↑n + 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : Num<GOAL>↑n.succ = ↑n + 1
<VAR>α : Type u_1<VAR>Semiring α<VAR>m n : Num<GOAL>↑(m + n) = ↑m + ↑n
<VAR>α : Type u_1<VAR>Semiring α<VAR>n : Num<GOAL>↑n.bit0 = 2 * ↑n
<VAR>α : Type u_1<VAR>Semiring α<VAR>n : Num<GOAL>↑n.bit1 = 2 * ↑n + 1
<VAR>α : Type u_1<VAR>Semiring α<VAR>m n : Num<GOAL>↑(m * n) = ↑m * ↑n
<VAR>n : Num<GOAL>↑n.size = (↑n).size
<VAR>n : Num<GOAL>↑n.size = n.natSize
<VAR>n : Num<GOAL>n.natSize = (↑n).size
<VAR>n : ℕ<GOAL>Num.ofNat' n = ↑n
<VAR>n : Num<GOAL>-n.toZNum = n.toZNumNeg
<VAR>n : Num<GOAL>-n.toZNumNeg = n.toZNum
<VAR>m n : Num<GOAL>m.toZNum = n.toZNum ↔ m = n
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>Neg α<VAR>n : Num<GOAL>↑n.toZNum = ↑n
<VAR>α : Type u_1<VAR>AddGroup α<VAR>One α<VAR>n : Num<GOAL>↑n.toZNumNeg = -↑n
<VAR>m n : Num<GOAL>(m + n).toZNum = m.toZNum + n.toZNum
<VAR>n : PosNum<VAR>h : 1 < n<GOAL>↑n.pred = (↑n).pred
<VAR>a : PosNum<GOAL>a.sub' 1 = a.pred'.toZNum
<VAR>a : PosNum<GOAL>PosNum.sub' 1 a = a.pred'.toZNumNeg
<VAR>m n : PosNum<GOAL>m < n ↔ m.cmp n = Ordering.lt
<VAR>m n : PosNum<GOAL>m ≤ n ↔ m.cmp n ≠ Ordering.gt
<VAR>n : Num<GOAL>↑n.pred = (↑n).pred
<VAR>n : Num<GOAL>castNum <$> n.ppred = (↑n).ppred
<VAR>m n : Num<GOAL>(m.cmp n).swap = n.cmp m
<VAR>m n : Num<GOAL>m.cmp n = Ordering.eq ↔ m = n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>m n : Num<GOAL>↑m < ↑n ↔ m < n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>m n : Num<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>LinearOrderedSemiring α<VAR>m n : Num<GOAL>↑m = ↑n ↔ m = n
<VAR>m n : Num<GOAL>m < n ↔ m.cmp n = Ordering.lt
<VAR>m n : Num<GOAL>m ≤ n ↔ m.cmp n ≠ Ordering.gt
<VAR>f : Num → Num → Num<VAR>g : Bool → Bool → Bool<VAR>p : PosNum → PosNum → Num<VAR>gff : g false false = false<VAR>f00 : f 0 0 = 0<VAR>f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0<VAR>fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0<VAR>fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n<VAR>p11 : p 1 1 = bif g true true then 1 else 0<VAR>p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0)<VAR>pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0)<VAR>pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)<VAR>m n : Num<GOAL>↑(f m n) = Nat.bitwise g ↑m ↑n
<VAR>m n : Num<GOAL>↑(m ||| n) = ↑m ||| ↑n
<VAR>m n : Num<GOAL>↑(m &&& n) = ↑m &&& ↑n
<VAR>m n : Num<GOAL>↑(m.ldiff n) = (↑m).ldiff ↑n
<VAR>m n : Num<GOAL>↑(m ^^^ n) = ↑m ^^^ ↑n
<VAR>m : Num<VAR>n : ℕ<GOAL>↑(m <<< n) = ↑m <<< n
<VAR>m : Num<VAR>n : ℕ<GOAL>↑(m >>> n) = ↑m >>> n
<VAR>m : Num<VAR>n : ℕ<GOAL>m.testBit n = (↑m).testBit n
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>Neg α<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>Neg α<GOAL>↑ZNum.zero = 0
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>Neg α<GOAL>↑1 = 1
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>Neg α<VAR>n : PosNum<GOAL>↑(ZNum.pos n) = ↑n
<VAR>α : Type u_1<VAR>Zero α<VAR>One α<VAR>Add α<VAR>Neg α<VAR>n : PosNum<GOAL>↑(ZNum.neg n) = -↑n
<VAR>α : Type u_1<VAR>AddGroup α<VAR>One α<VAR>n : ZNum<GOAL>↑(-n) = -↑n
<VAR>n : PosNum<GOAL>-ZNum.pos n = ZNum.neg n
<VAR>n : PosNum<GOAL>-ZNum.neg n = ZNum.pos n
<VAR>n : ZNum<GOAL>-n.bit1 = (-n).bitm1
<VAR>n : ZNum<GOAL>-n.bitm1 = (-n).bit1
<VAR>n : ZNum<GOAL>-n.succ = (-n).pred
<VAR>n : ZNum<GOAL>-n.pred = (-n).succ
<VAR>n : ZNum<GOAL>↑n.abs = (↑n).natAbs
<VAR>n : Num<GOAL>n.toZNum.abs = n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ZNum<GOAL>↑↑n = ↑n
<VAR>n : ZNum<GOAL>n + n + 1 = n.bit1
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ZNum<GOAL>↑n.bit0 = ↑n + ↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ZNum<GOAL>↑n.bit1 = ↑n + ↑n + 1
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ZNum<GOAL>↑n.bitm1 = ↑n + ↑n - 1
<VAR>n : ZNum<GOAL>n + 1 = n.succ
<VAR>n : PosNum<GOAL>↑n = ZNum.pos n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>m n : PosNum<GOAL>↑(m.sub' n) = ↑m - ↑n
<VAR>n : PosNum<GOAL>↑n = ↑n.pred' + 1
<VAR>n : PosNum<GOAL>↑n = ↑↑n.pred' + 1
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>m n : Num<GOAL>↑(m.sub' n) = ↑m - ↑n
<VAR>n : Num<GOAL>n.succ.toZNum = n.toZNum.succ
<VAR>n : Num<GOAL>n.succ.toZNumNeg = n.toZNumNeg.pred
<VAR>n : ℤ<GOAL>ZNum.ofInt' (n + 1) = ZNum.ofInt' n + 1
<VAR>n : ℕ<GOAL>(↑n).toZNum = ZNum.ofInt' ↑n
<VAR>m : Num<VAR>n : ZNum<GOAL>m ∈ Num.ofZNum' n ↔ n = m.toZNum
<VAR>n : ZNum<GOAL>castNum <$> Num.ofZNum' n = (↑n).toNat'
<VAR>n : ZNum<GOAL>↑(Num.ofZNum n) = (↑n).toNat
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ZNum<GOAL>↑(Num.ofZNum n) = ↑(↑n).toNat
<VAR>m n : Num<GOAL>↑(m - n) = ↑m - ↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>m n : ZNum<GOAL>↑(m + n) = ↑m + ↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ZNum<GOAL>↑n.succ = ↑n + 1
<VAR>m n : ZNum<GOAL>↑(m * n) = ↑m * ↑n
<VAR>α : Type u_1<VAR>Ring α<VAR>m n : ZNum<GOAL>↑(m * n) = ↑m * ↑n
<VAR>n : ℤ<GOAL>ZNum.ofInt' (-n) = -ZNum.ofInt' n
<VAR>n : ZNum<GOAL>ZNum.ofInt' ↑n = n
<VAR>m n : ZNum<GOAL>↑m = ↑n ↔ m = n
<VAR>m n : ZNum<GOAL>Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
<VAR>m n : ZNum<GOAL>↑m < ↑n ↔ m < n
<VAR>m n : ZNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>m n : ZNum<GOAL>↑m < ↑n ↔ m < n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>m n : ZNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>m n : ZNum<GOAL>↑m = ↑n ↔ m = n
<VAR>a b : ZNum<GOAL>a ≤ b → ∀ (c : ZNum), c + a ≤ c + b
<VAR>α : Type u_1<VAR>Ring α<VAR>m n : ZNum<GOAL>↑(m - n) = ↑m - ↑n
<VAR>n : ℤ<GOAL>↑(-n) = -↑n
<VAR>n : ℤ<GOAL>ZNum.ofInt' n = ↑n
<VAR>n : ℕ<GOAL>(↑n).toZNum = ↑n
<VAR>n : ℤ<GOAL>↑↑n = n
<VAR>n : ℕ<GOAL>(↑n).toZNumNeg = -↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>m n : ZNum<GOAL>↑m ∣ ↑n ↔ m ∣ n
<VAR>n d : PosNum<VAR>q r : Num<VAR>h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n<VAR>h₂ : ↑r < 2 * ↑d<GOAL>↑(d.divModAux q r).2 + ↑d * ↑(d.divModAux q r).1 = ↑n ∧ ↑(d.divModAux q r).2 < ↑d
<VAR>n d : PosNum<GOAL>↑(n.div' d) = ↑n / ↑d
<VAR>n d : PosNum<GOAL>↑(n.mod' d) = ↑n % ↑d
<VAR>n d : Num<GOAL>↑(n / d) = ↑n / ↑d
<VAR>n d : Num<GOAL>↑(n % d) = ↑n % ↑d
<VAR>n : ℕ<VAR>a b : Num<GOAL>a ≤ b → (a * b).natSize ≤ n → ↑(Num.gcdAux n a b) = (↑a).gcd ↑b
<VAR>a b : Num<GOAL>↑(a.gcd b) = (↑a).gcd ↑b
<VAR>n d : ZNum<GOAL>↑(n / d) = ↑n / ↑d
<VAR>n d : ZNum<GOAL>↑(n % d) = ↑n % ↑d
<VAR>a b : ZNum<GOAL>↑(a.gcd b) = (↑a).gcd ↑b