ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n d : ℕ<VAR>x : Fin n → ℕ<GOAL>Set.InjOn ⇑(Behrend.map d) {x | ∀ (i : Fin n), x i < d}
<VAR>n d : ℕ<VAR>x : Fin n → ℕ<VAR>hx : x ∈ Behrend.box n d<GOAL>(Behrend.map (2 * d - 1)) x ≤ ∑ i : Fin n, (d - 1) * (2 * d - 1) ^ ↑i
<VAR>n d k : ℕ<GOAL>ThreeAPFree ↑(Behrend.sphere n d k)
<VAR>n d k : ℕ<VAR>x : Fin n → ℕ<GOAL>ThreeAPFree ↑(Finset.image (⇑(Behrend.map (2 * d - 1))) (Behrend.sphere n d k))
<VAR>n d : ℕ<VAR>x : Fin n → ℕ<VAR>hx : x ∈ Behrend.box n d<GOAL>∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
<VAR>n d : ℕ<GOAL>∑ i : Fin n, d * (2 * d + 1) ^ ↑i = ((2 * d + 1) ^ n - 1) / 2
<VAR>n d : ℕ<GOAL>∑ i : Fin n, d * (2 * d + 1) ^ ↑i < (2 * d + 1) ^ n
<VAR>n d k : ℕ<GOAL>(Behrend.sphere n d k).card ≤ rothNumberNat ((2 * d - 1) ^ n)
<VAR>n d : ℕ<GOAL>∃ k ∈ Finset.range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(Behrend.sphere n d k).card
<VAR>n d : ℕ<GOAL>∃ k, ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(Behrend.sphere n d k).card
<VAR>n d : ℕ<GOAL>↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))
<VAR>n d : ℕ<VAR>hd : d ≠ 0<VAR>hn : 2 ≤ n<GOAL>↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))
<GOAL>Real.log 2 * 2 ≤ √(Real.log 8)
<GOAL>2 / (1 - 2 / rexp 1) ≤ 8
<VAR>N : ℕ<VAR>hN : 4096 ≤ N<GOAL>Real.log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(Real.log ↑N)
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
<VAR>x : ℝ<VAR>hx : 2 / (1 - 2 / rexp 1) ≤ x<GOAL>x / rexp 1 < ↑⌊x / 2⌋₊
<VAR>x : ℝ<VAR>hx : 50 / 19 ≤ x<GOAL>↑⌈x⌉₊ < 1.38 * x
<VAR>N : ℕ<VAR>hN : 2 ≤ N<GOAL>0 < Behrend.nValue N
<VAR>N : ℕ<VAR>hN : 64 ≤ N<GOAL>3 ≤ Behrend.nValue N
<VAR>N : ℕ<VAR>hN₃ : 8 ≤ N<GOAL>0 < Behrend.dValue N
<VAR>N : ℕ<VAR>hN : 2 ≤ N<GOAL>(2 * Behrend.dValue N - 1) ^ Behrend.nValue N ≤ N
<VAR>N : ℕ<VAR>hN : 4096 ≤ N<GOAL>↑N ^ (↑(Behrend.nValue N))⁻¹ / rexp 1 < ↑(Behrend.dValue N)
<VAR>N : ℕ<VAR>hN : 4096 ≤ N<GOAL>↑N * rexp (-4 * √(Real.log ↑N)) < ↑(rothNumberNat N)
<VAR>N : ℕ<VAR>hN : 2 ≤ N<VAR>hN' : N ≤ 4096<GOAL>↑N * rexp (-4 * √(Real.log ↑N)) ≤ 1
<VAR>N : ℕ<VAR>hN : 1 ≤ N<VAR>hN' : N ≤ 4096<GOAL>↑N * rexp (-4 * √(Real.log ↑N)) ≤ 1
<VAR>N : ℕ<GOAL>↑N * rexp (-4 * √(Real.log ↑N)) ≤ ↑(rothNumberNat N)
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hq : ∀ (x : α), p x → q x<VAR>hp : ∀ᶠ (x : α) in f, p x<GOAL>∀ᶠ (x : α) in f, q x
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hq : ∀ (x : α), p x → q x<VAR>hp : ∃ᶠ (x : α) in f, p x<GOAL>∃ᶠ (x : α) in f, q x
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hq : ∀ (x : α), p x ↔ q x<GOAL>(∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x
<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hq : ∀ (x : α), p x ↔ q x<GOAL>(∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x
<VAR>f f' : Sat.Fmla<VAR>self : f.subsumes f'<VAR>x : Sat.Clause<GOAL>x ∈ f' → x ∈ f
<VAR>f : Sat.Fmla<GOAL>f.subsumes f
<VAR>f f₁ f₂ : Sat.Fmla<VAR>H : f.subsumes (f₁.and f₂)<GOAL>f.subsumes f₁
<VAR>f f₁ f₂ : Sat.Fmla<VAR>H : f.subsumes (f₁.and f₂)<GOAL>f.subsumes f₂
<VAR>v : Sat.Valuation<VAR>f : Sat.Fmla<VAR>self : v.satisfies_fmla f<VAR>c : Sat.Clause<GOAL>c ∈ f → v.satisfies c
<VAR>f : Sat.Fmla<VAR>c : Sat.Clause<VAR>H : f.subsumes (Sat.Fmla.one c)<GOAL>f.proof c
<VAR>v : Sat.Valuation<VAR>l : Sat.Literal<VAR>h₁ : v.neg l.negate → False<VAR>h₂ : v.neg l → False<GOAL>False
<VAR>p : Prop<VAR>as ps : List Prop<VAR>as₁ : List Prop<GOAL>as = as₁.reverseAux ps → (Sat.Valuation.mk as).implies p ps as₁.length → p
<VAR>v : Sat.Valuation<VAR>f : Sat.Fmla<VAR>p : Prop<VAR>self : Sat.Fmla.reify v f p<GOAL>¬v.satisfies_fmla f → p
<VAR>p : Prop<VAR>ps : List Prop<VAR>f : Sat.Fmla<VAR>hf : f.proof []<VAR>hv : ∀ (v : Sat.Valuation), v.implies (Sat.Fmla.reify v f p) ps 0<GOAL>p
<VAR>v : Sat.Valuation<VAR>f₁ : Sat.Fmla<VAR>a : Prop<VAR>f₂ : Sat.Fmla<VAR>b : Prop<VAR>h₁ : Sat.Fmla.reify v f₁ a<VAR>h₂ : Sat.Fmla.reify v f₂ b<GOAL>Sat.Fmla.reify v (f₁.and f₂) (a ∨ b)
<VAR>v : Sat.Valuation<VAR>c : Sat.Clause<VAR>p : Prop<VAR>self : Sat.Clause.reify v c p<GOAL>¬v.satisfies c → p
<VAR>v : Sat.Valuation<VAR>c : Sat.Clause<VAR>a : Prop<VAR>h : Sat.Clause.reify v c a<GOAL>Sat.Fmla.reify v (Sat.Fmla.one c) a
<VAR>v : Sat.Valuation<VAR>l : Sat.Literal<VAR>p : Prop<VAR>self : Sat.Literal.reify v l p<GOAL>v.neg l → p
<VAR>v : Sat.Valuation<VAR>l : Sat.Literal<VAR>a : Prop<VAR>c : Sat.Clause<VAR>b : Prop<VAR>h₁ : Sat.Literal.reify v l a<VAR>h₂ : Sat.Clause.reify v c b<GOAL>Sat.Clause.reify v (Sat.Clause.cons l c) (a ∧ b)
<VAR>v : Sat.Valuation<GOAL>Sat.Clause.reify v Sat.Clause.nil True
<VAR>v : Sat.Valuation<VAR>l : Sat.Literal<VAR>a : Prop<VAR>h₁ : Sat.Literal.reify v l a<GOAL>Sat.Clause.reify v (Sat.Clause.cons l Sat.Clause.nil) a
<VAR>v : Sat.Valuation<VAR>a : Prop<VAR>n : ℕ<VAR>h : v n ↔ a<GOAL>Sat.Literal.reify v (Sat.Literal.pos n) ¬a
<VAR>v : Sat.Valuation<VAR>a : Prop<VAR>n : ℕ<VAR>h : v n ↔ a<GOAL>Sat.Literal.reify v (Sat.Literal.neg n) a
<VAR>d : ℕ<VAR>x y : ℤ<VAR>a b : ℤ<VAR>h₁ : ↑d ∣ x<VAR>h₂ : ↑d ∣ y<VAR>h₃ : x * a + y * b = ↑d<GOAL>x.gcd y = d
<VAR>x y : ℕ<VAR>h : y % x = 0<GOAL>x.gcd y = x
<VAR>x y : ℕ<VAR>h : x % y = 0<GOAL>x.gcd y = y
<VAR>d x y a b : ℕ<VAR>hu : x % d = 0<VAR>hv : y % d = 0<VAR>h : y * b = x * a + d<GOAL>x.gcd y = d
<VAR>x y a b : ℕ<VAR>h : y * b = x * a + 1<GOAL>x.gcd y = 1
<VAR>x y a b : ℕ<VAR>h : x * a = y * b + 1<GOAL>x.gcd y = 1
<VAR>x y d m : ℕ<VAR>hd : x.gcd y = d<VAR>d0 : d.beq 0 = false<VAR>dm : x * y = d * m<GOAL>x.lcm y = m
<VAR>x y : ℤ<VAR>x' y' d : ℕ<VAR>hx : x.natAbs = x'<VAR>hy : y.natAbs = y'<VAR>h : x'.gcd y' = d<GOAL>x.gcd y = d
<VAR>x y : ℤ<VAR>x' y' d : ℕ<VAR>hx : x.natAbs = x'<VAR>hy : y.natAbs = y'<VAR>h : x'.lcm y' = d<GOAL>x.lcm y = d
<VAR>x y nx ny z : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat x nx → Mathlib.Meta.NormNum.IsNat y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z
<VAR>x y nx ny z : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat x nx → Mathlib.Meta.NormNum.IsNat y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z
<VAR>x y nx ny : ℤ<VAR>z : ℕ<GOAL>Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z
<VAR>x y nx ny : ℤ<VAR>z : ℕ<GOAL>Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>CharZero α<VAR>a b : α<VAR>a' b' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.beq b' = false → ¬a = b
<VAR>α : Type u_1<VAR>Ring α<VAR>CharZero α<VAR>a b : α<VAR>a' b' : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' = b') = false → ¬a = b
<VAR>α : Type u_1<VAR>Ring α<VAR>n₁ n₂ : ℤ<VAR>a₁ a₂ : α<VAR>Invertible a₁<VAR>Invertible a₂<GOAL>↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
<VAR>α : Type u_1<VAR>Ring α<VAR>CharZero α<VAR>a b : α<VAR>na nb : ℤ<VAR>da db : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na.mul (Int.ofNat db) = nb.mul (Int.ofNat da)) = false → ¬a = b
<VAR>x nx z : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat x nx → nx.sqrt = z → Mathlib.Meta.NormNum.IsNat x.sqrt z
<VAR>x y nx ny : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → IsCoprime nx ny → IsCoprime x y
<VAR>x y nx ny : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → ¬IsCoprime nx ny → ¬IsCoprime x y
<GOAL>Mathlib.Meta.NormNum.IsFibAux 0 0 1
<GOAL>Mathlib.Meta.NormNum.IsFibAux 1 1 1
<VAR>n a b n' a' b' : ℕ<VAR>H : Mathlib.Meta.NormNum.IsFibAux n a b<VAR>hn : 2 * n = n'<VAR>h1 : a * (2 * b - a) = a'<VAR>h2 : a * a + b * b = b'<GOAL>Mathlib.Meta.NormNum.IsFibAux n' a' b'
<VAR>n a b n' a' b' : ℕ<VAR>H : Mathlib.Meta.NormNum.IsFibAux n a b<VAR>hn : 2 * n + 1 = n'<VAR>h1 : a * a + b * b = a'<VAR>h2 : b * (2 * a + b) = b'<GOAL>Mathlib.Meta.NormNum.IsFibAux n' a' b'
<VAR>n a b n' a' : ℕ<VAR>H : Mathlib.Meta.NormNum.IsFibAux n a b<VAR>hn : 2 * n = n'<VAR>h : a * (2 * b - a) = a'<GOAL>Nat.fib n' = a'
<VAR>n a b n' a' : ℕ<VAR>H : Mathlib.Meta.NormNum.IsFibAux n a b<VAR>hn : 2 * n + 1 = n'<VAR>h : a * a + b * b = a'<GOAL>Nat.fib n' = a'
<VAR>x nx z : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat x nx → Nat.fib nx = z → Mathlib.Meta.NormNum.IsNat (Nat.fib x) z
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>m e : ℕ<VAR>n : ℤ<VAR>d : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat (↑(mkRat (↑m) (10 ^ e))) n d → Mathlib.Meta.NormNum.IsRat (OfScientific.ofScientific m true e) n d
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>m e nm ne n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat m nm → Mathlib.Meta.NormNum.IsNat e ne → n = nm.mul (10 ^ ne) → Mathlib.Meta.NormNum.IsNat (OfScientific.ofScientific m false e) n
<VAR>a b r : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a r → Mathlib.Meta.NormNum.IsNat b 0 → Mathlib.Meta.NormNum.IsNat (a / b) 0
<VAR>a b q m a' : ℤ<VAR>b' r : ℕ<VAR>ha : Mathlib.Meta.NormNum.IsInt a a'<VAR>hb : Mathlib.Meta.NormNum.IsNat b b'<VAR>hm : q * ↑b' = m<VAR>h : ↑r + m = a'<VAR>h₂ : r.blt b' = true<GOAL>Mathlib.Meta.NormNum.IsInt (a / b) q
<VAR>a b q q' : ℤ<VAR>h : Mathlib.Meta.NormNum.IsInt (a / -b) q<VAR>hq : -q = q'<GOAL>Mathlib.Meta.NormNum.IsInt (a / b) q'
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : Mathlib.Meta.NormNum.IsInt a (Int.negOfNat b)<GOAL>Mathlib.Meta.NormNum.IsNat (-a) b
<VAR>a b r : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a r → Mathlib.Meta.NormNum.IsNat b 0 → Mathlib.Meta.NormNum.IsInt (a % b) r
<VAR>a b q m a' : ℤ<VAR>b' r : ℕ<VAR>ha : Mathlib.Meta.NormNum.IsInt a a'<VAR>hb : Mathlib.Meta.NormNum.IsNat b b'<VAR>hm : q * ↑b' = m<VAR>h : ↑r + m = a'<VAR>h₂ : r.blt b' = true<GOAL>Mathlib.Meta.NormNum.IsNat (a % b) r
<VAR>a b : ℤ<VAR>r : ℕ<VAR>h : Mathlib.Meta.NormNum.IsNat (a % -b) r<GOAL>Mathlib.Meta.NormNum.IsNat (a % b) r
<VAR>a b a' b' c : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → a'.mul c = b' → a ∣ b
<VAR>a b a' b' : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → (b'.mod a' != 0) = true → ¬a ∣ b
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>a : α<VAR>n : ℕ<VAR>self : Mathlib.Meta.NormNum.IsNat a n<GOAL>a = ↑n
<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n n
<VAR>α : Type u<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>a a' : α<GOAL>Mathlib.Meta.NormNum.IsNat a n → ↑n = a' → a = a'
<VAR>α : Type u<VAR>a : α<VAR>n : ℕ<VAR>AddMonoidWithOne α<GOAL>Mathlib.Meta.NormNum.IsNat a n → a = n.rawCast
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n.rawCast n
<VAR>p : ℕ → Prop<VAR>n n' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n n' → p n' → p n
<VAR>α : Type u<VAR>Ring α<VAR>a : α<VAR>n : ℤ<VAR>self : Mathlib.Meta.NormNum.IsInt a n<GOAL>a = ↑n
<VAR>α : Type u_1<VAR>Ring α<VAR>a : α<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsInt a (Int.ofNat n) → Mathlib.Meta.NormNum.IsNat a n
<VAR>α : Type u_1<VAR>Ring α<VAR>a : α<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)
<VAR>α : Type u<VAR>a : α<VAR>n : ℤ<VAR>Ring α<GOAL>Mathlib.Meta.NormNum.IsInt a n → a = n.rawCast
<VAR>α : Type u_1<VAR>Ring α<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt n.rawCast n
<VAR>α : Type u_1<VAR>Ring α<VAR>n : ℕ<VAR>a a' : α<GOAL>Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → ↑n = a' → a = -a'
<VAR>α : Type u_1<VAR>Ring α<VAR>n : ℕ<VAR>a a' : α<VAR>h : Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)<VAR>e : ↑n = a'<GOAL>a = a'
<VAR>α : Type u_1<VAR>Ring α<VAR>a : α<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) 1 → Mathlib.Meta.NormNum.IsNat a n
<VAR>α : Type u_1<VAR>Ring α<VAR>a : α<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) 1
<VAR>α : Type u_1<VAR>Ring α<VAR>a : α<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsRat a n 1 → Mathlib.Meta.NormNum.IsInt a n
<VAR>α : Type u_1<VAR>Ring α<VAR>a : α<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a n → Mathlib.Meta.NormNum.IsRat a n 1
<VAR>α : Type u<VAR>n : ℤ<VAR>d : ℕ<VAR>DivisionRing α<VAR>a : α<GOAL>Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n d : ℕ<VAR>a n' d' : α<GOAL>Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n) d → ↑n = n' → ↑d = d' → a = -(n' / d')
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n d : ℕ<VAR>a n' d' : α<GOAL>Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) d → ↑n = n' → ↑d = d' → a = n' / d'
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>h : ↑d ≠ 0<GOAL>Mathlib.Meta.NormNum.IsRat (Rat.rawCast n d) n d
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<VAR>n : ℤ<VAR>d : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a n d → ↑d ≠ 0
<VAR>a b n : ℕ<VAR>h : a * b = n<VAR>h₁ : a.ble 1 = false<VAR>h₂ : b.ble 1 = false<GOAL>¬Nat.Prime n
<VAR>n k : ℕ<VAR>h : Mathlib.Meta.NormNum.MinFacHelper n k<GOAL>1 < n
<VAR>n : ℕ<VAR>h1 : Nat.ble 2 n = true<VAR>h2 : 1 = n % 2<GOAL>Mathlib.Meta.NormNum.MinFacHelper n 3
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>h : Mathlib.Meta.NormNum.MinFacHelper n k<VAR>np : n.minFac ≠ k<GOAL>Mathlib.Meta.NormNum.MinFacHelper n k'
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : ¬Nat.Prime k<VAR>h : Mathlib.Meta.NormNum.MinFacHelper n k<GOAL>Mathlib.Meta.NormNum.MinFacHelper n k'
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : (n % k).beq 0 = false<VAR>h : Mathlib.Meta.NormNum.MinFacHelper n k<GOAL>Mathlib.Meta.NormNum.MinFacHelper n k'
<VAR>a : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a.minFac 1
<VAR>a a' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → a' % 2 = 0 → Mathlib.Meta.NormNum.IsNat a.minFac 2
<VAR>n n' : ℕ<VAR>k : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.MinFacHelper n' k → 0 = n' % k → Mathlib.Meta.NormNum.IsNat n.minFac k
<VAR>n n' k : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n n' → Mathlib.Meta.NormNum.MinFacHelper n' k → (k * k).ble n' = false → Mathlib.Meta.NormNum.IsNat n.minFac n'
<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n 0 → ¬Nat.Prime n
<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n 1 → ¬Nat.Prime n
<VAR>n n' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat n n' → Nat.ble 2 n' = true → Mathlib.Meta.NormNum.IsNat n'.minFac n' → Nat.Prime n
<VAR>n n' : ℕ<VAR>h : Mathlib.Meta.NormNum.IsNat n n'<GOAL>¬Nat.Prime n' → ¬Nat.Prime n
<VAR>a na n : ℤ<VAR>b nb d : ℕ<GOAL>Mathlib.Meta.NormNum.IsInt a na → Mathlib.Meta.NormNum.IsNat b nb → Mathlib.Meta.NormNum.IsRat (↑na / ↑nb) n d → Mathlib.Meta.NormNum.IsRat (mkRat a b) n d
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>q : ℚ<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat q n → Mathlib.Meta.NormNum.IsNat (↑q) n
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>q : ℚ<VAR>n : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt q n → Mathlib.Meta.NormNum.IsInt (↑q) n
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>CharZero R<VAR>q : ℚ<VAR>n : ℤ<VAR>d : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat q n d → Mathlib.Meta.NormNum.IsRat (↑q) n d
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>CharZero α<VAR>a : α<VAR>n d : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a (Int.ofNat n.succ) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.ofNat d) n.succ
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<GOAL>Mathlib.Meta.NormNum.IsNat a 1 → Mathlib.Meta.NormNum.IsNat a⁻¹ 1
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<GOAL>Mathlib.Meta.NormNum.IsNat a 0 → Mathlib.Meta.NormNum.IsNat a⁻¹ 0
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<GOAL>Mathlib.Meta.NormNum.IsInt a (Int.negOfNat 1) → Mathlib.Meta.NormNum.IsInt a⁻¹ (Int.negOfNat 1)
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>CharZero α<VAR>a : α<VAR>n d : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n.succ) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.negOfNat d) n.succ
<VAR>a : ℕ<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a 0 = 1
<VAR>a : ℕ<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a 1 = 1
<VAR>b : ℕ<VAR>hb : (b / 2).beq 0 = false<GOAL>Mathlib.Meta.NormNum.jacobiSymNat 0 b = 0
<VAR>b : ℕ<GOAL>Mathlib.Meta.NormNum.jacobiSymNat 1 b = 1
<VAR>p : ℕ<VAR>pp : Fact (Nat.Prime p)<VAR>a r : ℤ<VAR>hr : Mathlib.Meta.NormNum.IsInt (jacobiSym a p) r<GOAL>Mathlib.Meta.NormNum.IsInt (legendreSym p a) r
<VAR>a : ℤ<VAR>b ab' : ℕ<VAR>ab r b' : ℤ<VAR>hb' : ↑b = b'<VAR>hab : a % b' = ab<VAR>h : ↑ab' = ab<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat ab' b = r<GOAL>jacobiSym a b = r
<VAR>a b ab : ℕ<VAR>r : ℤ<VAR>hab : a % b = ab<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat ab b = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b : ℕ<VAR>hb₀ : (b / 2).beq 0 = false<VAR>ha : a % 2 = 0<VAR>hb₁ : b % 2 = 0<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = 0
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 2 = 0<VAR>hc : b / 2 = c<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat a c = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 0<VAR>hb : b % 2 = 1<VAR>hc : a / 4 = c<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 1<VAR>hc : a / 2 = c<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 7<VAR>hc : a / 2 = c<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 3<VAR>hc : a / 2 = c<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = -r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 5<VAR>hc : a / 2 = c<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat c b = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = -r
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 1<VAR>hb : b % 2 = 1<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat b a = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b ab : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 1<VAR>hb : b % 2 = 1<VAR>hab : b % a = ab<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat ab a = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 4 = 1<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat b a = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b ab : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 4 = 1<VAR>hab : b % a = ab<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat ab a = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = r
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 3<VAR>hb : b % 4 = 3<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat b a = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = -r
<VAR>a b ab : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 3<VAR>hb : b % 4 = 3<VAR>hab : b % a = ab<VAR>hr : Mathlib.Meta.NormNum.jacobiSymNat ab a = r<GOAL>Mathlib.Meta.NormNum.jacobiSymNat a b = -r
<VAR>a na : ℤ<VAR>b nb : ℕ<VAR>r : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a na → Mathlib.Meta.NormNum.IsNat b nb → jacobiSym na nb = r → Mathlib.Meta.NormNum.IsInt (jacobiSym a b) r
<VAR>a na b nb : ℕ<VAR>r : ℤ<GOAL>Mathlib.Meta.NormNum.IsNat a na → Mathlib.Meta.NormNum.IsNat b nb → Mathlib.Meta.NormNum.jacobiSymNat na nb = r → Mathlib.Meta.NormNum.IsInt (Mathlib.Meta.NormNum.jacobiSymNat a b) r
<VAR>a : ℕ<GOAL>a.pow 0 = 1
<VAR>a : ℕ<GOAL>a.pow 1 = a
<VAR>b : ℕ<GOAL>Nat.pow 0 b.succ = 0
<VAR>b : ℕ<GOAL>Nat.pow 1 b = 1
<VAR>p : Prop<VAR>a b c : ℕ<VAR>self : Mathlib.Meta.NormNum.IsNatPowT p a b c<GOAL>p → a.pow b = c
<VAR>a b c : ℕ<VAR>p : Mathlib.Meta.NormNum.IsNatPowT (a.pow 1 = a) a b c<GOAL>a.pow b = c
<VAR>a b c : ℕ<VAR>p : Prop<VAR>b' c' : ℕ<VAR>h1 : Mathlib.Meta.NormNum.IsNatPowT p a b c<VAR>h2 : Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a b' c'<GOAL>Mathlib.Meta.NormNum.IsNatPowT p a b' c'
<VAR>a b c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b) (c.mul c)
<VAR>a b c : ℕ<GOAL>Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b + 1) (c.mul (c.mul a))
<VAR>a b c : ℕ<VAR>h1 : a.pow b = c<GOAL>(Int.ofNat a).pow b = Int.ofNat c
<VAR>α : Type u_1<VAR>Semiring α<VAR>f : α → ℕ → α<VAR>a : α<VAR>b a' b' c : ℕ<GOAL>f = HPow.hPow → Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.pow b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → ℕ → α<VAR>a : α<VAR>b : ℕ<VAR>a' : ℤ<VAR>b' : ℕ<VAR>c : ℤ<GOAL>f = HPow.hPow → Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.pow b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
<VAR>α : Type u_1<VAR>Ring α<VAR>f : α → ℕ → α<VAR>a : α<VAR>an cn : ℤ<VAR>ad b b' cd : ℕ<GOAL>f = HPow.hPow → Mathlib.Meta.NormNum.IsRat a an ad → Mathlib.Meta.NormNum.IsNat b b' → an.pow b' = cn → ad.pow b' = cd → Mathlib.Meta.NormNum.IsRat (f a b) cn cd
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsNat b nb<VAR>pe' : Mathlib.Meta.NormNum.IsNat (a ^ nb) ne<GOAL>Mathlib.Meta.NormNum.IsNat (a ^ b) ne
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)<VAR>pe' : Mathlib.Meta.NormNum.IsNat (a ^ nb)⁻¹ ne<GOAL>Mathlib.Meta.NormNum.IsNat (a ^ b) ne
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsNat b nb<VAR>pe' : Mathlib.Meta.NormNum.IsInt (a ^ nb) (Int.negOfNat ne)<GOAL>Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)<VAR>pe' : Mathlib.Meta.NormNum.IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)<GOAL>Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsNat b nb<VAR>pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb) num den<GOAL>Mathlib.Meta.NormNum.IsRat (a ^ b) num den
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)<VAR>pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb)⁻¹ num den<GOAL>Mathlib.Meta.NormNum.IsRat (a ^ b) num den
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>a' b' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = true → a ≤ b
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>a b : α<VAR>a' b' : ℕ<VAR>ha : Mathlib.Meta.NormNum.IsNat a a'<VAR>hb : Mathlib.Meta.NormNum.IsNat b b'<VAR>h : b'.ble a' = true<GOAL>¬a < b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>na nb : ℤ<VAR>da db : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na.mul (Int.ofNat db) ≤ nb.mul (Int.ofNat da)) = true → a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Nontrivial α<VAR>a b : α<VAR>na nb : ℤ<VAR>da db : ℕ<GOAL>Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na * ↑db < nb * ↑da) = true → a < b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>Nontrivial α<VAR>a b : α<VAR>na nb : ℤ<VAR>da db : ℕ<VAR>ha : Mathlib.Meta.NormNum.IsRat a na da<VAR>hb : Mathlib.Meta.NormNum.IsRat b nb db<VAR>h : decide (nb * ↑da < na * ↑db) = true<GOAL>¬a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a b : α<VAR>na nb : ℤ<VAR>da db : ℕ<VAR>ha : Mathlib.Meta.NormNum.IsRat a na da<VAR>hb : Mathlib.Meta.NormNum.IsRat b nb db<VAR>h : decide (nb * ↑da ≤ na * ↑db) = true<GOAL>¬a < b
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>CharZero α<VAR>a b : α<VAR>a' b' : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.ble a' = false → a < b
<VAR>α : Type u_1<VAR>OrderedSemiring α<VAR>CharZero α<VAR>a b : α<VAR>a' b' : ℕ<VAR>ha : Mathlib.Meta.NormNum.IsNat a a'<VAR>hb : Mathlib.Meta.NormNum.IsNat b b'<VAR>h : a'.ble b' = false<GOAL>¬a ≤ b
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>a b : α<VAR>a' b' : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' ≤ b') = true → a ≤ b
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>Nontrivial α<VAR>a b : α<VAR>a' b' : ℤ<GOAL>Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' < b') = true → a < b
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>Nontrivial α<VAR>a b : α<VAR>a' b' : ℤ<VAR>ha : Mathlib.Meta.NormNum.IsInt a a'<VAR>hb : Mathlib.Meta.NormNum.IsInt b b'<VAR>h : decide (b' < a') = true<GOAL>¬a ≤ b
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>a b : α<VAR>a' b' : ℤ<VAR>ha : Mathlib.Meta.NormNum.IsInt a a'<VAR>hb : Mathlib.Meta.NormNum.IsInt b b'<VAR>h : decide (b' ≤ a') = true<GOAL>¬a < b
<VAR>a b : ℕ<GOAL>a = b ↔ ↑a = ↑b
<VAR>a b : ℕ<GOAL>a ≤ b ↔ ↑a ≤ ↑b
<VAR>a b : ℕ<GOAL>a < b ↔ ↑a < ↑b
<VAR>a b : ℕ<GOAL>a ≠ b ↔ ↑a ≠ ↑b
<VAR>a b : ℕ<GOAL>a ∣ b ↔ ↑a ∣ ↑b
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>m n k : ℕ<VAR>h : m + k ≤ n<GOAL>↑(n - m) = ↑n - ↑m
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>m n : ℕ<VAR>h : m < n<GOAL>↑(n - m) = ↑n - ↑m