ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : ℕ → Sort u<VAR>H : (b : Bool) → (n : ℕ) → C (Nat.bit b n)<VAR>b : Bool<VAR>n : ℕ<GOAL>(Nat.bit b n).bitCasesOn H = H b n
<VAR>C : ℕ → Sort u<VAR>H : (b : Bool) → (n : ℕ) → C (Nat.bit b n)<VAR>n : ℕ<GOAL>(2 * n).bitCasesOn H = H false n
<VAR>C : ℕ → Sort u<VAR>H : (b : Bool) → (n : ℕ) → C (Nat.bit b n)<VAR>n : ℕ<GOAL>(2 * n + 1).bitCasesOn H = H true n
<VAR>C : ℕ → Sort u<GOAL>Function.Injective fun H n => n.bitCasesOn H
<VAR>C : ℕ → Sort u<VAR>H₁ H₂ : (b : Bool) → (n : ℕ) → C (Nat.bit b n)<GOAL>((fun n => n.bitCasesOn H₁) = fun n => n.bitCasesOn H₂) ↔ H₁ = H₂
<VAR>n : ℕ<VAR>b : Bool<GOAL>Nat.bit b n = 0 ↔ n = 0 ∧ b = false
<VAR>b : Bool<VAR>m n : ℕ<GOAL>m ≤ n → Nat.bit b m ≤ Nat.bit b n
<VAR>m n : ℕ<VAR>a b : Bool<VAR>h : m < n<GOAL>Nat.bit a m < Nat.bit b n
<VAR>C : ℕ → Sort u_1<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)<VAR>b : Bool<VAR>n : ℕ<VAR>h : f false 0 z = z ∨ (n = 0 → b = true)<GOAL>Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)
<VAR>n : ℕ<VAR>b : Bool<VAR>hn : n = 0 → b = true<GOAL>(Nat.bit b n).bits = b :: n.bits
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(2 * n).bits = false :: n.bits
<VAR>n : ℕ<GOAL>(2 * n + 1).bits = true :: n.bits
<VAR>n : ℕ<GOAL>n.bodd = n.bits.headI
<VAR>n : ℕ<GOAL>n.div2.bits = n.bits.tail
<VAR>a n : ℕ<GOAL>n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x x_1 => x ^ x_1
<VAR>a : ℕ<GOAL>Nat.floorRoot 0 a = 0
<VAR>n : ℕ<GOAL>n.floorRoot 0 = 0
<VAR>a : ℕ<GOAL>Nat.floorRoot 1 a = a
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n.floorRoot 1 = 1
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>n.floorRoot (a ^ n) = a
<VAR>a n : ℕ<GOAL>n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
<VAR>a n : ℕ<GOAL>n.floorRoot a = 0 ↔ n = 0 ∨ a = 0
<VAR>n a : ℕ<GOAL>(n.floorRoot a).factorization = a.factorization ⌊/⌋ n
<VAR>a n : ℕ<GOAL>n.floorRoot a ^ n ∣ a
<VAR>a n : ℕ<GOAL>n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x x_1 => x ^ x_1
<VAR>a : ℕ<GOAL>Nat.ceilRoot 0 a = 0
<VAR>n : ℕ<GOAL>n.ceilRoot 0 = 0
<VAR>a : ℕ<GOAL>Nat.ceilRoot 1 a = a
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n.ceilRoot 1 = 1
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>n.ceilRoot (a ^ n) = a
<VAR>a n : ℕ<GOAL>n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
<VAR>a n : ℕ<GOAL>n.ceilRoot a = 0 ↔ n = 0 ∨ a = 0
<VAR>n a : ℕ<GOAL>(n.ceilRoot a).factorization = a.factorization ⌈/⌉ n
<VAR>a n : ℕ<VAR>hn : n ≠ 0<GOAL>a ∣ n.ceilRoot a ^ n
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>0 < ∏ i ∈ s, (f i)!
<VAR>n k : ℕ<GOAL>n.descFactorial k = ∏ i ∈ Finset.range k, (n - i)
<VAR>n : ℕ<VAR>hn : IsPrimePow n<GOAL>n.minFac ^ n.factorization n.minFac = n
<VAR>n : ℕ<VAR>h : n.minFac ^ n.factorization n.minFac = n<VAR>hn : n ≠ 1<GOAL>IsPrimePow n
<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>IsPrimePow n ↔ n.minFac ^ n.factorization n.minFac = n
<VAR>n : ℕ<GOAL>IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k
<VAR>n : ℕ<GOAL>IsPrimePow n ↔ n.primeFactors.card = 1
<VAR>n : ℕ<VAR>h : IsPrimePow n<GOAL>∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>n : ℕ<GOAL>IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
<VAR>n k : ℕ<VAR>hk : k ≠ 0<GOAL>IsPrimePow (n ^ k) ↔ IsPrimePow n
<VAR>n a b : ℕ<VAR>hab : a.Coprime b<VAR>hn : IsPrimePow n<GOAL>n ∣ a * b ↔ n ∣ a ∨ n ∣ b
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors ∪ b.divisors)
<VAR>n : ℕ<GOAL>n.primeFactorsList.toFinset = n.primeFactors
<VAR>n p : ℕ<GOAL>p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
<VAR>n p : ℕ<VAR>hn : n ≠ 0<GOAL>p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n
<VAR>m n : ℕ<VAR>hmn : m ∣ n<VAR>hn : n ≠ 0<GOAL>m.primeFactors ⊆ n.primeFactors
<VAR>n p : ℕ<GOAL>p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList
<VAR>n p : ℕ<VAR>hp : p ∈ n.primeFactors<GOAL>Nat.Prime p
<VAR>n p : ℕ<VAR>hp : p ∈ n.primeFactors<GOAL>p ∣ n
<VAR>n p : ℕ<VAR>hp : p ∈ n.primeFactors<GOAL>0 < p
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactors<GOAL>p ≤ n
<VAR>n : ℕ<GOAL>n.primeFactors = ∅ ↔ n = 0 ∨ n = 1
<VAR>n : ℕ<GOAL>n.primeFactors.Nonempty ↔ 1 < n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p.primeFactors = {p}
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a * b).primeFactors = a.primeFactors ∪ b.primeFactors
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>(a * b).primeFactors = a.primeFactors ∪ b.primeFactors
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>Disjoint a.primeFactors b.primeFactors
<VAR>n k : ℕ<GOAL>(n ^ (k + 1)).primeFactors = n.primeFactors
<VAR>k : ℕ<VAR>n : ℕ<VAR>hk : k ≠ 0<GOAL>(n ^ k).primeFactors = n.primeFactors
<VAR>k p : ℕ<VAR>hk : k ≠ 0<VAR>hp : Nat.Prime p<GOAL>(p ^ k).primeFactors = {p}
<VAR>n : ℕ<GOAL>n.factorization.support = n.primeFactors
<VAR>n : ℕ<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>n.factorization p = padicValNat p n
<VAR>n p : ℕ<GOAL>List.count p n.primeFactorsList = n.factorization p
<VAR>n : ℕ<GOAL>n.factorization = Multiset.toFinsupp ↑n.primeFactorsList
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : n ≠ 0<VAR>h : p ∣ n<GOAL>0 < n.factorization p
<VAR>n p : ℕ<VAR>pp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>multiplicity p n = ↑(n.factorization p)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(n.factorization.prod fun x x_1 => x ^ x_1) = n
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : ℕ), a.factorization p = b.factorization p<GOAL>a = b
<GOAL>Set.InjOn Nat.factorization {x | x ≠ 0}
<VAR>n p : ℕ<GOAL>n.factorization p = 0 ↔ ¬Nat.Prime p ∨ ¬p ∣ n ∨ n = 0
<VAR>n : ℕ<VAR>p : ℕ<VAR>hp : ¬Nat.Prime p<GOAL>n.factorization p = 0
<VAR>n : ℕ<GOAL>n.factorization 0 = 0
<VAR>n p : ℕ<VAR>h : ¬p ∣ n<GOAL>n.factorization p = 0
<VAR>p r : ℕ<VAR>i : ℕ<VAR>hr : ¬p ∣ r<GOAL>(p * i + r).factorization p = 0
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a * b).factorization = a.factorization + b.factorization
<VAR>d n : ℕ<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>d.factorization ≤ n.factorization ↔ d ∣ n
<VAR>α : Type u_1<VAR>S : Finset α<VAR>g : α → ℕ<VAR>hS : ∀ x ∈ S, g x ≠ 0<GOAL>(S.prod g).factorization = ∑ x ∈ S, (g x).factorization
<VAR>n k : ℕ<GOAL>(n ^ k).factorization = k • n.factorization
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p.factorization = Finsupp.single p 1
<VAR>p k : ℕ<VAR>hp : Nat.Prime p<GOAL>(p ^ k).factorization = Finsupp.single p k
<VAR>n p : ℕ<VAR>hn : n ≠ 0<VAR>hp : Nat.Prime p<GOAL>¬p ^ (n.factorization p + 1) ∣ n
<VAR>f : ℕ →₀ ℕ<VAR>hf : ∀ p ∈ f.support, Nat.Prime p<GOAL>(f.prod fun x x_1 => x ^ x_1).factorization = f
<VAR>p a b : ℕ<VAR>hab : a.Coprime b<GOAL>(a * b).factorization p = a.factorization p + b.factorization p
<VAR>a b : ℕ<VAR>hab : a.Coprime b<GOAL>(a * b).factorization = a.factorization + b.factorization
<VAR>n p : ℕ<GOAL>p ^ n.factorization p ∣ n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h_two : p ≠ 2<VAR>h_three : p ≠ 3<GOAL>5 ≤ p
<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>0 < p.pred
<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>p.pred.succ = p
<VAR>n : ℕ<VAR>n2 : 2 ≤ n<VAR>np : ¬Nat.Prime n<GOAL>∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
<VAR>n : ℕ<VAR>n2 : 2 ≤ n<VAR>np : ¬Nat.Prime n<GOAL>∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
<VAR>m n : ℕ<VAR>h1 : m ∣ n<VAR>h2 : m ≠ 1<VAR>h3 : m ≠ n<GOAL>¬Nat.Prime n
<VAR>m n : ℕ<VAR>h1 : m ∣ n<VAR>h2 : 2 ≤ m<VAR>h3 : m < n<GOAL>¬Nat.Prime n
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n
<VAR>a b : ℕ<VAR>hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ a → p * a ∣ b<GOAL>a ∣ b
<VAR>n : ℕ<GOAL>∃ p, n ≤ p ∧ Nat.Prime p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>Even p ↔ p = 2
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h_two : p ≠ 2<GOAL>Odd p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h2 : p ≠ 2<GOAL>Even (p - 1)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>p % 2 = 1 ↔ p ≠ 2
<VAR>m n : ℕ<VAR>H : ∀ (k : ℕ), Nat.Prime k → k ∣ m → k ∣ n → k ∣ 1<GOAL>m.Coprime n
<VAR>p n : ℕ<VAR>pp : Nat.Prime p<GOAL>p ∣ n ↔ ¬p.Coprime n
<VAR>m n : ℕ<GOAL>¬m.Coprime n ↔ ∃ p, Nat.Prime p ∧ p ∣ m ∧ p ∣ n
<VAR>p m n : ℕ<VAR>pp : Nat.Prime p<VAR>Hm : ¬p ∣ m<VAR>Hn : ¬p ∣ n<GOAL>¬p ∣ m * n
<VAR>n : ℕ<GOAL>Nat.Coprime 2 n ↔ Odd n
<VAR>n : ℕ<GOAL>n.Coprime 2 ↔ Odd n
<VAR>p m n : ℕ<VAR>pp : Nat.Prime p<VAR>h : p ∣ m ^ n<GOAL>p ∣ m
<VAR>x n : ℕ<VAR>hn : n ≠ 1<GOAL>¬Nat.Prime (x ^ n)
<VAR>x n : ℕ<VAR>hn : 2 ≤ n<GOAL>¬Nat.Prime (x ^ n)
<VAR>x n : ℕ<VAR>h : Nat.Prime (x ^ n)<GOAL>n = 1
<VAR>p a k : ℕ<VAR>hp : Nat.Prime p<GOAL>a ^ k = p ↔ a = p ∧ k = 1
<VAR>n k : ℕ<VAR>hk : k ≠ 0<GOAL>(n ^ k).minFac = n.minFac
<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<GOAL>(p ^ k).minFac = p
<VAR>x y p : ℕ<VAR>hp : Nat.Prime p<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<GOAL>x * y = p ^ 2 ↔ x = p ∧ y = p
<VAR>n p : ℕ<GOAL>Nat.Prime p → (p ∣ n ! ↔ p ≤ n)
<VAR>p m a : ℕ<VAR>pp : Nat.Prime p<VAR>h : ¬p ∣ a<GOAL>a.Coprime (p ^ m)
<VAR>p q : ℕ<VAR>pp : Nat.Prime p<VAR>pq : Nat.Prime q<GOAL>p.Coprime q ↔ p ≠ q
<VAR>p q : ℕ<VAR>n m : ℕ<VAR>pp : Nat.Prime p<VAR>pq : Nat.Prime q<VAR>h : p ≠ q<GOAL>(p ^ n).Coprime (q ^ m)
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>i : ℕ<GOAL>p.Coprime i ∨ p ∣ i
<VAR>n p : ℕ<VAR>n_pos : 0 < n<VAR>hlt : n < p<VAR>pp : Nat.Prime p<GOAL>p.Coprime n
<VAR>n p : ℕ<VAR>n_pos : 0 < n<VAR>hle : n ≤ p<VAR>pp : Nat.Prime p<GOAL>p = n ∨ p.Coprime n
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>m i : ℕ<GOAL>i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k
<VAR>p1 p2 n : ℕ<VAR>h_neq : p1 ≠ p2<VAR>pp1 : Nat.Prime p1<VAR>pp2 : Nat.Prime p2<VAR>h1 : p1 ∣ n<VAR>h2 : p2 ∣ n<GOAL>p1 * p2 ∣ n
<VAR>a p k : ℕ<VAR>pp : Nat.Prime p<VAR>h₁ : ¬a ∣ p ^ k<VAR>h₂ : a ∣ p ^ (k + 1)<GOAL>a = p ^ (k + 1)
<VAR>n : ℕ<GOAL>n ≠ 1 ↔ ∃ p, Nat.Prime p ∧ p ∣ n
<VAR>n : ℕ<GOAL>n = 1 ↔ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ n
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ Prime ↑p
<VAR>p q m n : ℕ<VAR>hp : Nat.Prime p<VAR>hq : Nat.Prime q<VAR>h : p ^ (m + 1) = q ^ (n + 1)<GOAL>p = q ∧ m = n
<VAR>c : ℕ<GOAL>∃ n0 > 1, ∀ n ≥ n0, c ^ n < (n - 1)!
<VAR>a c : ℕ<GOAL>∃ n0, ∀ n ≥ n0, a * c ^ n < (n - 1)!
<VAR>n a c : ℕ<GOAL>∃ p > n, Nat.Prime p ∧ a * c ^ p < (p - 1)!
<VAR>R : Type u_1<VAR>Semiring R<VAR>x y : R<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
<VAR>R : Type u_1<VAR>Semiring R<VAR>x y : R<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(x + y) ^ n = ∑ m ∈ Finset.antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x y : R<VAR>n : ℕ<GOAL>(x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
<VAR>n : ℕ<GOAL>∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n
<VAR>m : ℕ<GOAL>∑ i ∈ Finset.range (m + 1), (2 * m + 1).choose i = 4 ^ m
<VAR>n : ℕ<GOAL>(2 * n + 1).choose n ≤ 4 ^ n
<VAR>n : ℕ<GOAL>4 ^ n ≤ (2 * n + 1) * (2 * n).choose n
<VAR>n k : ℕ<GOAL>∑ m ∈ Finset.Icc k n, m.choose k = (n + 1).choose (k + 1)
<VAR>n : ℕ<GOAL>∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>f : ℕ → α<VAR>x : Finset β<GOAL>∑ m ∈ x.powerset, f m.card = ∑ m ∈ Finset.range (x.card + 1), x.card.choose m • f m
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>x : Finset α<GOAL>∑ m ∈ x.powerset, (-1) ^ m.card = if x = ∅ then 1 else 0
<VAR>α : Type u_2<VAR>x : Finset α<VAR>h0 : x.Nonempty<GOAL>∑ m ∈ x.powerset, (-1) ^ m.card = 0
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ Finset.range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i = (∏ i ∈ Finset.range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ Finset.range (n + 1), f (i + 1) (n - i) ^ n.choose i
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 2), (n + 1).choose i • f i (n + 1 - i) = ∑ i ∈ Finset.range (n + 1), n.choose i • f i (n + 1 - i) + ∑ i ∈ Finset.range (n + 1), n.choose i • f (i + 1) (n - i)
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ ij ∈ Finset.antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 = (∏ ij ∈ Finset.antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) * ∏ ij ∈ Finset.antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∑ ij ∈ Finset.antidiagonal (n + 1), (n + 1).choose ij.1 • f ij.1 ij.2 = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • f ij.1 (ij.2 + 1) + ∑ ij ∈ Finset.antidiagonal n, n.choose ij.2 • f (ij.1 + 1) ij.2
<VAR>R : Type u_3<VAR>NonAssocSemiring R<VAR>f : ℕ → ℕ → R<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)
<VAR>R : Type u_3<VAR>NonAssocSemiring R<VAR>f : ℕ → ℕ → R<VAR>n : ℕ<GOAL>∑ ij ∈ Finset.antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 = ∑ ij ∈ Finset.antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) + ∑ ij ∈ Finset.antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
<VAR>d n : ℕ<GOAL>∑ ij ∈ Finset.antidiagonal n, (d + ij.2).choose d = (d + n).choose d + (d + n).choose d.succ
<VAR>S : Type u_1<VAR>Semiring S<VAR>a b : ℕ<GOAL>↑(a.ascFactorial b) = Polynomial.eval (↑a) (ascPochhammer S b)
<VAR>S : Type u_1<VAR>Semiring S<VAR>a b : ℕ<GOAL>↑(a.descFactorial b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)
<VAR>S : Type u_1<VAR>Semiring S<VAR>a : ℕ<GOAL>↑a ! = Polynomial.eval 1 (ascPochhammer S a)
<VAR>S : Type u_1<VAR>Ring S<VAR>a : ℕ<GOAL>↑(a.descFactorial 2) = ↑a * (↑a - 1)
<VAR>p : ℕ → Prop<GOAL>(∃ x, p x) → WellFounded (Nat.Upto.GT p)
<VAR>a : ℕ<GOAL>Irreducible a ↔ Nat.Prime a
<VAR>n : ℕ<VAR>h : Nat.Prime n<GOAL>n ≠ 0
<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>0 < p
<VAR>p : ℕ<GOAL>Nat.Prime p → 2 ≤ p
<VAR>p : ℕ<GOAL>Nat.Prime p → 1 < p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>1 ≤ p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p ≠ 1
<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>m : ℕ<VAR>hm : m ∣ p<GOAL>m = 1 ∨ m = p
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
<VAR>n : ℕ<VAR>h1 : 1 < n<VAR>h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m<GOAL>Nat.Prime n
<VAR>p m : ℕ<VAR>pp : Nat.Prime p<GOAL>m ∣ p ↔ m = 1 ∨ m = p
<VAR>p m : ℕ<VAR>pp : Nat.Prime p<VAR>H : 2 ≤ m<GOAL>m ∣ p ↔ m = p
<VAR>p q : ℕ<VAR>pp : Nat.Prime p<VAR>qp : Nat.Prime q<GOAL>p ∣ q ↔ p = q
<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>¬p ∣ 1
<VAR>a b : ℕ<GOAL>Nat.Prime (a * b) ↔ Nat.Prime a ∧ b = 1 ∨ Nat.Prime b ∧ a = 1
<VAR>a b : ℕ<VAR>a1 : a ≠ 1<VAR>b1 : b ≠ 1<GOAL>¬Nat.Prime (a * b)
<VAR>a b n : ℕ<VAR>h : a * b = n<VAR>h₁ : a ≠ 1<VAR>h₂ : b ≠ 1<GOAL>¬Nat.Prime n
<VAR>p a : ℕ<VAR>hp : Nat.Prime p<VAR>a1 : a ≠ 1<GOAL>a ∣ p ↔ p = a
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p = 2 ∨ p % 2 = 1
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p = 2 ∨ Odd p
<VAR>n k : ℕ<VAR>h : ¬n < k * k<GOAL>n.sqrt - k < n.sqrt + 2 - k
<VAR>n : ℕ<GOAL>n.minFac = if 2 ∣ n then 2 else n.minFacAux 3
<VAR>n : ℕ<VAR>n2 : 2 ≤ n<VAR>k i : ℕ<GOAL>k = 2 * i + 3 → (∀ (m : ℕ), 2 ≤ m → m ∣ n → k ≤ m) → Nat.minFacProp n (n.minFacAux k)
<VAR>n : ℕ<VAR>n1 : n ≠ 1<GOAL>Nat.minFacProp n n.minFac
<VAR>n : ℕ<GOAL>n.minFac ∣ n
<VAR>n : ℕ<VAR>n1 : n ≠ 1<GOAL>Nat.Prime n.minFac
<VAR>n m : ℕ<GOAL>2 ≤ m → m ∣ n → n.minFac ≤ m
<VAR>n : ℕ<GOAL>0 < n.minFac
<VAR>n : ℕ<VAR>H : 0 < n<GOAL>n.minFac ≤ n
<VAR>m n : ℕ<GOAL>n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → m ≤ p
<VAR>m n : ℕ<GOAL>n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), 2 ≤ p → p ∣ n → m ≤ p
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ 2 ≤ p ∧ p.minFac = p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p.minFac = p
<VAR>n : ℕ<VAR>n2 : 2 ≤ n<GOAL>¬Nat.Prime n ↔ n.minFac < n
<VAR>n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Nat.Prime n<GOAL>n.minFac ≤ n / n.minFac
<VAR>n : ℕ<VAR>w : 0 < n<VAR>h : ¬Nat.Prime n<GOAL>n.minFac ^ 2 ≤ n
<VAR>n : ℕ<GOAL>n.minFac = 1 ↔ n = 1
<VAR>n : ℕ<GOAL>n.minFac = 2 ↔ 2 ∣ n
<VAR>k : ℕ<GOAL>(k + 2) / (k + 2).minFac < k + 2
<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>∃ p, Nat.Prime p ∧ p ∣ n
<VAR>m n : ℕ<VAR>H : ∀ (k : ℕ), Nat.Prime k → k ∣ m → ¬k ∣ n<GOAL>m.Coprime n
<VAR>p n : ℕ<VAR>pp : Nat.Prime p<GOAL>p.Coprime n ↔ ¬p ∣ n
<VAR>p m n : ℕ<VAR>pp : Nat.Prime p<GOAL>p ∣ m * n ↔ p ∣ m ∨ p ∣ n
<VAR>p : ℕ<GOAL>Nat.Prime p ↔ Prime p
<VAR>p : ℕ<GOAL>Irreducible p ↔ Prime p
<VAR>n : ℕ<GOAL>(n + 2)‼ = (n + 2) * n‼
<VAR>n : ℕ<GOAL>(n + 1)‼ = (n + 1) * (n - 1)‼
<VAR>n : ℕ<GOAL>(n + 1)! = (n + 1)‼ * n‼
<VAR>n : ℕ<GOAL>n‼ ≤ n !
<VAR>n : ℕ<GOAL>(2 * n)‼ = 2 ^ n * n !
<VAR>n : ℕ<GOAL>(2 * n)‼ = ∏ i ∈ Finset.range n, 2 * (i + 1)
<VAR>n : ℕ<GOAL>(2 * n + 1)‼ = ∏ i ∈ Finset.range n, (2 * (i + 1) + 1)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>n : ℕ<VAR>hn : hf.toFinset.card ≤ n<GOAL>Nat.nth p n = 0
<VAR>p : ℕ → Prop<VAR>h : (setOf p).Finite<VAR>n : ℕ<GOAL>Nat.nth p n = (Finset.sort (fun x x_1 => x ≤ x_1) h.toFinset).getD n 0
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>n : ℕ<VAR>hn : n < hf.toFinset.card<GOAL>Nat.nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<GOAL>StrictMonoOn (Nat.nth p) (Set.Iio hf.toFinset.card)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>m n : ℕ<VAR>h : m < n<VAR>hn : n < hf.toFinset.card<GOAL>Nat.nth p m < Nat.nth p n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>hn : n < hf.toFinset.card<GOAL>Nat.nth p m ≤ Nat.nth p n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>m n : ℕ<VAR>h : Nat.nth p m < Nat.nth p n<VAR>hm : m < hf.toFinset.card<GOAL>m < n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>m n : ℕ<VAR>h : Nat.nth p m ≤ Nat.nth p n<VAR>hm : m < hf.toFinset.card<GOAL>m ≤ n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<GOAL>Set.InjOn (Nat.nth p) (Set.Iio hf.toFinset.card)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<GOAL>Set.range (Nat.nth p) = insert 0 (setOf p)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<GOAL>Nat.nth p '' Set.Iio hf.toFinset.card = setOf p
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hf : (setOf p).Finite<VAR>hlt : n < hf.toFinset.card<GOAL>p (Nat.nth p n)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>x : ℕ<VAR>h : p x<GOAL>∃ n < hf.toFinset.card, Nat.nth p n = x
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<VAR>n : ℕ<GOAL>Nat.nth p n = ↑((Nat.Subtype.orderIsoOfNat (setOf p)) n)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>Nat.nth p = Subtype.val ∘ ⇑(Nat.Subtype.orderIsoOfNat (setOf p))
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>StrictMono (Nat.nth p)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>Function.Injective (Nat.nth p)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>Monotone (Nat.nth p)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<VAR>k n : ℕ<GOAL>Nat.nth p k < Nat.nth p n ↔ k < n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<VAR>k n : ℕ<GOAL>Nat.nth p k ≤ Nat.nth p n ↔ k ≤ n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<GOAL>Set.range (Nat.nth p) = setOf p
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<VAR>n : ℕ<GOAL>p (Nat.nth p n)
<VAR>p : ℕ → Prop<VAR>x : ℕ<VAR>h : p x<GOAL>∃ n, (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) ∧ Nat.nth p n = x
<VAR>p : ℕ → Prop<GOAL>setOf p ⊆ Set.range (Nat.nth p)
<VAR>p : ℕ → Prop<GOAL>Set.range (Nat.nth p) ⊆ insert 0 (setOf p)
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>p (Nat.nth p n)
<VAR>p : ℕ → Prop<VAR>m n : ℕ<VAR>hlt : m < n<VAR>h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>Nat.nth p m < Nat.nth p n
<VAR>p : ℕ → Prop<VAR>m n : ℕ<VAR>hle : m ≤ n<VAR>h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>Nat.nth p m ≤ Nat.nth p n
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>n ≤ Nat.nth p n
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hf : (setOf p).Finite<VAR>hn : n < hf.toFinset.card<GOAL>IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Infinite<VAR>n : ℕ<GOAL>IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
<VAR>p : ℕ → Prop<VAR>n : ℕ<GOAL>Nat.nth p n = sInf {x | p x ∧ ∀ k < n, Nat.nth p k < x}
<VAR>p : ℕ → Prop<GOAL>Nat.nth p 0 = sInf (setOf p)
<VAR>p : ℕ → Prop<VAR>h : p 0<GOAL>Nat.nth p 0 = 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>h : ∃ n, p n<GOAL>Nat.nth p 0 = Nat.find h
<VAR>p : ℕ → Prop<VAR>n : ℕ<GOAL>Nat.nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ (hf : (setOf p).Finite), hf.toFinset.card ≤ n
<VAR>p : ℕ → Prop<VAR>h₀ : ¬p 0<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>ha : Nat.nth p a = 0<GOAL>Nat.nth p b = 0
<VAR>p : ℕ → Prop<VAR>k a : ℕ<VAR>h : a < Nat.nth p (k + 1)<VAR>ha : p a<GOAL>a ≤ Nat.nth p k
<VAR>p : ℕ → Prop<VAR>DecidablePred p<GOAL>Nat.count p (Nat.nth p 0) = 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>k : ℕ<GOAL>Finset.filter p (Finset.range (Nat.nth p (k + 1))) ⊆ insert (Nat.nth p k) (Finset.filter p (Finset.range (Nat.nth p k)))
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>k : ℕ<VAR>hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card<GOAL>Finset.filter p (Finset.range (Nat.nth p (k + 1))) = insert (Nat.nth p k) (Finset.filter p (Finset.range (Nat.nth p k)))
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hf : (setOf p).Finite<VAR>k : ℕ<VAR>hlt : k + 1 < hf.toFinset.card<GOAL>Finset.filter p (Finset.range (Nat.nth p (k + 1))) = insert (Nat.nth p k) (Finset.filter p (Finset.range (Nat.nth p k)))
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Infinite<VAR>k : ℕ<GOAL>Finset.filter p (Finset.range (Nat.nth p (k + 1))) = insert (Nat.nth p k) (Finset.filter p (Finset.range (Nat.nth p k)))
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>Nat.count p (Nat.nth p n) = n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hp : (setOf p).Finite<VAR>hlt : n < hp.toFinset.card<GOAL>Nat.count p (Nat.nth p n) = n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Infinite<VAR>n : ℕ<GOAL>Nat.count p (Nat.nth p n) = n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>Nat.count p (Nat.nth p n + 1) = n + 1
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hpn : p n<GOAL>Nat.nth p (Nat.count p n) = n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n k : ℕ<VAR>h : k < Nat.count p n<GOAL>Nat.nth p k < n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n k : ℕ<VAR>h : n ≤ Nat.nth p k<GOAL>Nat.count p n ≤ k
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.nth p (Nat.count p n) = sInf {i | p i ∧ n ≤ i}
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hpn : ∃ k, p k ∧ n ≤ k<GOAL>n ≤ Nat.nth p (Nat.count p n)
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Infinite<VAR>n : ℕ<GOAL>n ≤ Nat.nth p (Nat.count p n)
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Infinite<GOAL>GaloisConnection (Nat.count p) (Nat.nth p)
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Infinite<VAR>a b : ℕ<GOAL>Nat.count p a ≤ b ↔ a ≤ Nat.nth p b
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Infinite<VAR>a b : ℕ<GOAL>a < Nat.count p b ↔ Nat.nth p a < b
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hp : ∀ n' ≤ n, p n'<GOAL>Nat.nth p n = n
<VAR>n : ℕ<GOAL>Nat.nth (fun x => True) n = n
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hp : ∀ n' ≥ n, ¬p n'<GOAL>Nat.nth p n = 0
<VAR>n : ℕ<GOAL>Nat.nth (fun x => False) n = 0
<VAR>n : ℕ<GOAL>(n + 1).factorial = (n + 1) * n.factorial
<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>n * (n - 1).factorial = n.factorial
<VAR>n : ℕ<GOAL>n.factorial ≠ 0
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m.factorial ∣ n.factorial
<VAR>m n : ℕ<GOAL>0 < m → m ≤ n → m ∣ n.factorial
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m.factorial ≤ n.factorial
<VAR>m n : ℕ<GOAL>m.factorial * (m + 1) ^ n ≤ (m + n).factorial
<VAR>m n : ℕ<VAR>hn : 0 < n<GOAL>n.factorial < m.factorial ↔ n < m
<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>h : n < m<GOAL>n.factorial < m.factorial
<VAR>n : ℕ<GOAL>1 < n.factorial ↔ 1 < n
<VAR>n : ℕ<GOAL>n.factorial = 1 ↔ n ≤ 1
<VAR>m n : ℕ<VAR>hn : 1 < n<GOAL>n.factorial = m.factorial ↔ n = m
<VAR>m n : ℕ<VAR>h : 1 < n ∨ 1 < m<GOAL>n.factorial = m.factorial ↔ n = m
<VAR>n : ℕ<GOAL>n ≤ n.factorial
<VAR>n : ℕ<VAR>hi : 3 ≤ n<GOAL>n < n.factorial