ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>i : ℕ<VAR>n : ℕ<VAR>hi : 2 ≤ i<GOAL>i + (n + 1).factorial < (i + n + 1).factorial
<VAR>i n : ℕ<VAR>hi : 2 ≤ i<VAR>hn : 1 ≤ n<GOAL>i + n.factorial < (i + n).factorial
<VAR>i n : ℕ<GOAL>i + (n + 1).factorial ≤ (i + (n + 1)).factorial
<VAR>i : ℕ<VAR>n : ℕ<VAR>n1 : 1 ≤ n<GOAL>i + n.factorial ≤ (i + n).factorial
<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>n.factorial * n ^ (m - n) ≤ m.factorial
<VAR>n : ℕ<GOAL>n.factorial ≤ n ^ n
<VAR>n : ℕ<GOAL>n.ascFactorial 0 = 1
<VAR>n k : ℕ<GOAL>n.ascFactorial k.succ = (n + k) * n.ascFactorial k
<VAR>k : ℕ<GOAL>Nat.ascFactorial 0 k.succ = 0
<VAR>k : ℕ<GOAL>Nat.ascFactorial 1 k = k.factorial
<VAR>n k : ℕ<GOAL>n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
<VAR>n k : ℕ<GOAL>n.factorial * (n + 1).ascFactorial k = (n + k).factorial
<VAR>n k : ℕ<VAR>h : 0 < n<GOAL>(n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k = (n + k).factorial / n.factorial
<VAR>n k : ℕ<VAR>h : 0 < n<GOAL>n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial
<VAR>n k : ℕ<GOAL>n ^ k ≤ n.ascFactorial k
<VAR>n : ℕ<VAR>k : ℕ<GOAL>2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k ≤ (n + k) ^ k
<VAR>n : ℕ<VAR>k : ℕ<GOAL>2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
<VAR>n k : ℕ<GOAL>0 < (n + 1).ascFactorial k
<VAR>n : ℕ<GOAL>n.descFactorial 0 = 1
<VAR>n k : ℕ<GOAL>n.descFactorial (k + 1) = (n - k) * n.descFactorial k
<VAR>k : ℕ<GOAL>Nat.descFactorial 0 (k + 1) = 0
<VAR>n : ℕ<GOAL>n.descFactorial 1 = n
<VAR>n k : ℕ<GOAL>(n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k
<VAR>n k : ℕ<GOAL>(n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
<VAR>n : ℕ<GOAL>n.descFactorial n = n.factorial
<VAR>n k : ℕ<GOAL>n.descFactorial k = 0 ↔ n < k
<VAR>n k : ℕ<GOAL>(n + k).descFactorial k = (n + 1).ascFactorial k
<VAR>n k : ℕ<GOAL>(n + k - 1).descFactorial k = n.ascFactorial k
<VAR>n k : ℕ<GOAL>k ≤ n → (n - k).factorial * n.descFactorial k = n.factorial
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>n.descFactorial k = n.factorial / (n - k).factorial
<VAR>n k : ℕ<GOAL>(n + 1 - k) ^ k ≤ n.descFactorial k
<VAR>n k : ℕ<GOAL>k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
<VAR>n k : ℕ<GOAL>2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k
<VAR>n k : ℕ<GOAL>n.descFactorial k ≤ n ^ k
<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>k : ℕ<GOAL>2 ≤ k → n.descFactorial k < n ^ k
<VAR>n : ℕ<GOAL>(2 * n).factorial ≤ (2 * n) ^ n * n.factorial
<VAR>n : ℕ<GOAL>2 ^ n * n.factorial ≤ (2 * n).factorial
<VAR>m n : ℕ<GOAL>m <<< n = m * 2 ^ n
<VAR>m n : ℕ<GOAL>Nat.shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
<VAR>b : Bool<VAR>m : ℕ<VAR>h : m ≠ 0<VAR>n : ℕ<GOAL>Nat.shiftLeft' b m n ≠ 0
<VAR>m : ℕ<VAR>n : ℕ<GOAL>n ≠ 0 → Nat.shiftLeft' true m n ≠ 0
<VAR>b : Bool<VAR>n : ℕ<VAR>h : Nat.bit b n ≠ 0<GOAL>(Nat.bit b n).size = n.size.succ
<VAR>b : Bool<VAR>m n : ℕ<VAR>h : Nat.shiftLeft' b m n ≠ 0<GOAL>(Nat.shiftLeft' b m n).size = m.size + n
<VAR>m n : ℕ<GOAL>m.size ≤ n ↔ m < 2 ^ n
<VAR>n : ℕ<GOAL>(2 ^ n).size = n + 1
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m.size ≤ n.size
<VAR>n : ℕ<GOAL>n.bits.length = n.size
<VAR>n : ℕ<GOAL>n.succ.superFactorial = (n + 1).factorial * n.superFactorial
<VAR>n : ℕ<GOAL>∏ x ∈ Finset.Icc 1 n, x.factorial = n.superFactorial
<VAR>n : ℕ<GOAL>∏ x ∈ Finset.range n, (x + 1).factorial = n.superFactorial
<VAR>n : ℕ<GOAL>∏ x ∈ Finset.range (n + 1), x.factorial = n.superFactorial
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<GOAL>(Matrix.vandermonde fun i => ↑↑i).det = ↑n.superFactorial
<VAR>n : ℕ<GOAL>(2 * n).superFactorial = (∏ i ∈ Finset.range n, (2 * i + 1).factorial) ^ 2 * 2 ^ n * n.factorial
<VAR>n : ℕ<GOAL>(4 * n).superFactorial = ((∏ i ∈ Finset.range (2 * n), (2 * i + 1).factorial) * 2 ^ n) ^ 2 * (2 * n).factorial
<VAR>n : ℕ<VAR>v : Fin n → ℕ<GOAL>(Matrix.of fun i j => Polynomial.eval (↑(v i)) (descPochhammer ℤ ↑j)).det = ↑(∏ i : Fin n, (↑i).factorial) * (Matrix.of fun i j => ↑((v i).choose ↑j)).det
<VAR>n : ℕ<VAR>v : Fin (n + 1) → ℤ<GOAL>↑n.superFactorial ∣ (Matrix.vandermonde v).det
<VAR>n m : WithBot ℕ<GOAL>n + m = 0 ↔ n = 0 ∧ m = 0
<VAR>n m : WithBot ℕ<GOAL>n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
<VAR>n m : WithBot ℕ<GOAL>n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0
<VAR>n m : WithBot ℕ<GOAL>n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0
<VAR>n : WithBot ℕ<GOAL>n < 0 ↔ n = ⊥
<VAR>x : WithBot ℕ<GOAL>x < 1 ↔ x ≤ 0
<VAR>n m : WithBot ℕ<VAR>h : n < m<GOAL>n + 1 ≤ m
<VAR>n : ℕ<VAR>a : ℕ<GOAL>a ≡ a [MOD n]
<VAR>n a : ℕ<GOAL>a ≡ a [MOD n]
<VAR>n a b : ℕ<GOAL>a ≡ b [MOD n] → b ≡ a [MOD n]
<VAR>n a b c : ℕ<GOAL>a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n]
<VAR>n a b : ℕ<GOAL>a ≡ b [MOD n] ↔ b ≡ a [MOD n]
<VAR>n a : ℕ<GOAL>a ≡ 0 [MOD n] ↔ n ∣ a
<VAR>n a : ℕ<VAR>h : n ∣ a<GOAL>a ≡ 0 [MOD n]
<VAR>n a : ℕ<VAR>h : n ∣ a<GOAL>0 ≡ a [MOD n]
<VAR>n a b : ℕ<GOAL>a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a
<VAR>n a b : ℕ<VAR>h : a ≤ b<GOAL>a ≡ b [MOD n] ↔ n ∣ b - a
<VAR>a n : ℕ<GOAL>a % n ≡ a [MOD n]
<VAR>m n a b : ℕ<VAR>d : m ∣ n<VAR>h : a ≡ b [MOD n]<GOAL>a ≡ b [MOD m]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>c * a ≡ c * b [MOD c * n]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>c * a ≡ c * b [MOD n]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a * c ≡ b * c [MOD n * c]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a * c ≡ b * c [MOD n]
<VAR>n a b c d : ℕ<VAR>h₁ : a ≡ b [MOD n]<VAR>h₂ : c ≡ d [MOD n]<GOAL>a * c ≡ b * d [MOD n]
<VAR>n a b : ℕ<VAR>m : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a ^ m ≡ b ^ m [MOD n]
<VAR>n a b c d : ℕ<VAR>h₁ : a ≡ b [MOD n]<VAR>h₂ : c ≡ d [MOD n]<GOAL>a + c ≡ b + d [MOD n]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>c + a ≡ c + b [MOD n]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a + c ≡ b + c [MOD n]
<VAR>n a b c d : ℕ<VAR>h₁ : a ≡ b [MOD n]<VAR>h₂ : a + c ≡ b + d [MOD n]<GOAL>c ≡ d [MOD n]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : c + a ≡ c + b [MOD n]<GOAL>a ≡ b [MOD n]
<VAR>n a b c d : ℕ<VAR>h₁ : c ≡ d [MOD n]<VAR>h₂ : a + c ≡ b + d [MOD n]<GOAL>a ≡ b [MOD n]
<VAR>n a b : ℕ<VAR>c : ℕ<VAR>h : a + c ≡ b + c [MOD n]<GOAL>a ≡ b [MOD n]
<VAR>a b c m : ℕ<VAR>hc : c ≠ 0<GOAL>c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]
<VAR>a b c m : ℕ<VAR>hc : c ≠ 0<GOAL>c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m]
<VAR>a b c m : ℕ<VAR>hc : c ≠ 0<GOAL>a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]
<VAR>a b c m : ℕ<VAR>hc : c ≠ 0<GOAL>a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m]
<VAR>n a b : ℕ<VAR>m : ℕ<VAR>h : a ≡ b [MOD m * n]<GOAL>a ≡ b [MOD n]
<VAR>n a b : ℕ<VAR>m : ℕ<GOAL>a ≡ b [MOD n * m] → a ≡ b [MOD n]
<VAR>m a b c : ℕ<VAR>h : a / c ≡ b / c [MOD m / c]<VAR>ha : c ∣ a<GOAL>c ∣ b → c ∣ m → a ≡ b [MOD m]
<VAR>a b : ℕ<VAR>h : b ≤ a<GOAL>a ≡ b [MOD a - b]
<VAR>a b : ℕ<GOAL>a ≡ b [MOD 1]
<VAR>a b : ℕ<GOAL>a ≡ b [MOD 0] ↔ a = b
<VAR>n a : ℕ<GOAL>n + a ≡ a [MOD n]
<VAR>n a : ℕ<GOAL>a + n ≡ a [MOD n]
<VAR>m a b : ℕ<VAR>h1 : a ≡ b [MOD m]<VAR>h2 : a < b + m<GOAL>a ≤ b
<VAR>m a b : ℕ<VAR>h1 : a ≡ b [MOD m]<VAR>h2 : a < b<GOAL>a + m ≤ b
<VAR>m a b d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>hdm : d ∣ m<GOAL>d ∣ a ↔ d ∣ b
<VAR>m a b : ℕ<VAR>h : a ≡ b [MOD m]<GOAL>a.gcd m = b.gcd m
<VAR>m a b : ℕ<VAR>h : a ≡ b [MOD m]<VAR>h2 : |↑b - ↑a| < ↑m<GOAL>a = b
<VAR>m a b : ℕ<VAR>h : a ≡ b [MOD m]<VAR>ha : a < m<VAR>hb : b < m<GOAL>a = b
<VAR>m a b c : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m a b c : ℕ<VAR>hm : 0 < m<VAR>h : a * c ≡ b * c [MOD m]<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m a b c d : ℕ<VAR>hm : 0 < m<VAR>hcd : c ≡ d [MOD m]<VAR>h : c * a ≡ d * b [MOD m]<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m a b c d : ℕ<VAR>hm : 0 < m<VAR>hcd : c ≡ d [MOD m]<VAR>h : a * c ≡ b * d [MOD m]<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m a b c : ℕ<VAR>hmc : m.gcd c = 1<VAR>h : c * a ≡ c * b [MOD m]<GOAL>a ≡ b [MOD m]
<VAR>m a b c : ℕ<VAR>hmc : m.gcd c = 1<VAR>h : a * c ≡ b * c [MOD m]<GOAL>a ≡ b [MOD m]
<VAR>m n a b : ℕ<VAR>h : a ≡ b [MOD n.gcd m]<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<GOAL>↑(Nat.chineseRemainder' h) < n.lcm m
<VAR>m n : ℕ<VAR>co : n.Coprime m<VAR>a b : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<GOAL>↑(Nat.chineseRemainder co a b) < n * m
<VAR>m n a b : ℕ<VAR>hn : a ≡ b [MOD n]<VAR>hm : a ≡ b [MOD m]<GOAL>a ≡ b [MOD n.lcm m]
<VAR>m n : ℕ<VAR>co : n.Coprime m<VAR>a b z : ℕ<VAR>hzan : z ≡ a [MOD n]<VAR>hzbm : z ≡ b [MOD m]<GOAL>z ≡ ↑(Nat.chineseRemainder co a b) [MOD n * m]
<VAR>a b m n : ℕ<VAR>hmn : m.Coprime n<GOAL>a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n]
<VAR>b : ℕ<VAR>a n : ℕ<VAR>h : a * b ≡ 1 [MOD n]<GOAL>a.Coprime n
<VAR>a b c : ℕ<GOAL>((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
<VAR>a b c : ℕ<VAR>hc : a % c + b % c < c<GOAL>(a + b) % c = a % c + b % c
<VAR>a b c : ℕ<VAR>hc : c ≤ a % c + b % c<GOAL>(a + b) % c + c = a % c + b % c
<VAR>a b c : ℕ<VAR>hc0 : 0 < c<GOAL>(a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
<VAR>a b c : ℕ<VAR>hc : a % c + b % c < c<GOAL>(a + b) / c = a / c + b / c
<VAR>a b c : ℕ<VAR>hca : c ∣ a<GOAL>(a + b) / c = a / c + b / c
<VAR>a b c : ℕ<VAR>hca : c ∣ b<GOAL>(a + b) / c = a / c + b / c
<VAR>a b c : ℕ<VAR>hc : c ≤ a % c + b % c<VAR>hc0 : 0 < c<GOAL>(a + b) / c = a / c + b / c + 1
<VAR>a b c : ℕ<GOAL>a / c + b / c ≤ (a + b) / c
<VAR>a b c : ℕ<VAR>h : c ∣ a + b<VAR>ha : ¬c ∣ a<GOAL>c ≤ a % c + b % c
<VAR>n m : ℕ<GOAL>n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1
<VAR>m n : ℕ<VAR>hm1 : m % 2 = 1<VAR>hn1 : n % 2 = 1<GOAL>m * n / 2 = m * (n / 2) + m / 2
<VAR>n : ℕ<GOAL>n % 4 = 1 → n % 2 = 1
<VAR>n : ℕ<GOAL>n % 4 = 3 → n % 2 = 1
<VAR>n : ℕ<GOAL>n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3
<VAR>a b n : ℕ<VAR>h : a ≡ b [MOD n]<VAR>hb : b < n<GOAL>a % n = b
<VAR>p : ℕ → Prop<VAR>DecidablePred p<GOAL>Nat.count p 0 = 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p n = (Finset.filter p (Finset.range n)).card
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p n = Fintype.card { k // k < n ∧ p k }
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p (n + 1) = Nat.count p n + if p n then 1 else 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<GOAL>Monotone (Nat.count p)
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>a b : ℕ<GOAL>Nat.count p (a + b) = Nat.count p a + Nat.count (fun k => p (a + k)) b
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>a b : ℕ<GOAL>Nat.count p (a + b) = Nat.count (fun k => p (k + b)) a + Nat.count p b
<VAR>p : ℕ → Prop<VAR>DecidablePred p<GOAL>Nat.count p 1 = if p 0 then 1 else 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p (n + 1) = Nat.count (fun k => p (k + 1)) n + if p 0 then 1 else 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p n < Nat.count p (n + 1) ↔ p n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p (n + 1) = Nat.count p n + 1 ↔ p n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>Nat.count p (n + 1) = Nat.count p n ↔ ¬p n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<GOAL>↑(Nat.count p n) ≤ Cardinal.mk ↑{k | p k}
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>a b : ℕ<VAR>h : Nat.count p a < Nat.count p b<GOAL>a < b
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>m n : ℕ<VAR>hm : p m<VAR>hmn : m < n<GOAL>Nat.count p m < Nat.count p n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>m n : ℕ<VAR>hm : p m<VAR>hn : p n<VAR>heq : Nat.count p m = Nat.count p n<GOAL>m = n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>hp : (setOf p).Finite<VAR>n : ℕ<GOAL>Nat.count p n ≤ hp.toFinset.card
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hp : (setOf p).Finite<VAR>hpn : p n<GOAL>Nat.count p n < hp.toFinset.card
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hp : ∀ n' < n, p n'<GOAL>Nat.count p n = n
<VAR>n : ℕ<GOAL>Nat.count (fun x => True) n = n
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>n : ℕ<VAR>hp : ∀ n' < n, ¬p n'<GOAL>Nat.count p n = 0
<VAR>n : ℕ<GOAL>Nat.count (fun x => False) n = 0
<VAR>p : ℕ → Prop<VAR>DecidablePred p<VAR>q : ℕ → Prop<VAR>DecidablePred q<VAR>n : ℕ<VAR>hpq : ∀ (k : ℕ), p k → q k<GOAL>Nat.count p n ≤ Nat.count q n
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>0 < Nat.multinomial s f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>(∏ i ∈ s, (f i)!) * Nat.multinomial s f = (∑ i ∈ s, f i)!
<VAR>α : Type u_1<VAR>f : α → ℕ<GOAL>Nat.multinomial ∅ f = 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<VAR>f : α → ℕ<GOAL>Nat.multinomial (Finset.cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * Nat.multinomial s f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>ha : a ∉ s<VAR>f : α → ℕ<GOAL>Nat.multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * Nat.multinomial s f
<VAR>α : Type u_1<VAR>a : α<VAR>f : α → ℕ<GOAL>Nat.multinomial {a} f = 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∉ s<VAR>h₁ : f a = 1<GOAL>Nat.multinomial (insert a s) f = (s.sum f).succ * Nat.multinomial s f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f g : α → ℕ<VAR>h : ∀ a ∈ s, f a = g a<GOAL>Nat.multinomial s f = Nat.multinomial s g
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≠ b<GOAL>Nat.multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≠ b<GOAL>Nat.multinomial {a, b} f = (f a + f b).choose (f a)
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<VAR>DecidableEq α<VAR>hab : a ≠ b<GOAL>(f a)! * (f b)! * Nat.multinomial {a, b} f = (f a + f b)!
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≠ b<VAR>h₁ : f a = 1<GOAL>Nat.multinomial {a, b} f = (f b).succ
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≠ b<GOAL>Nat.multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) = Nat.multinomial {a, b} (Function.update f a (f a).succ) + Nat.multinomial {a, b} (Function.update f b (f b).succ)
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≠ b<GOAL>(f a + f b).succ * Nat.multinomial {a, b} f = (f a).succ * Nat.multinomial {a, b} (Function.update f a (f a).succ)
<VAR>a b : ℕ<GOAL>Nat.multinomial Finset.univ ![a, b] = (a + b)! / (a ! * b !)
<VAR>a b c : ℕ<GOAL>Nat.multinomial Finset.univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)
<VAR>α : Type u_1<VAR>f : α →₀ ℕ<GOAL>f.multinomial = Nat.multinomial f.support ⇑f
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>m : Multiset α<GOAL>m.multinomial = (Multiset.card m).choose (Multiset.count a m) * (Multiset.filter (fun x => a ≠ x) m).multinomial
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Multiset.multinomial 0 = 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>DecidableEq α<VAR>Semiring R<VAR>s : Finset α<VAR>f : α → R<VAR>hc : (↑s).Pairwise fun i j => Commute (f i) (f j)<VAR>n : ℕ<GOAL>(∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * s.noncommProd (fun i => f i ^ k i) ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>DecidableEq α<VAR>Semiring R<VAR>x : α → R<VAR>s : Finset α<VAR>hc : (↑s).Pairwise fun i j => Commute (x i) (x j)<VAR>n : ℕ<GOAL>s.sum x ^ n = ∑ k : { x // x ∈ s.sym n }, ↑(↑↑k).multinomial * (Multiset.map x ↑↑k).noncommProd ⋯
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>DecidableEq α<VAR>CommSemiring R<VAR>s : Finset α<VAR>f : α → R<VAR>n : ℕ<GOAL>(∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * ∏ i ∈ s, f i ^ k i
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<VAR>CommSemiring R<VAR>x : α → R<VAR>n : ℕ<GOAL>s.sum x ^ n = ∑ k ∈ s.sym n, ↑(↑k).multinomial * (Multiset.map x ↑k).prod
<VAR>n : ℕ<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Fin (n + 1)<VAR>s : Sym α (n - ↑m)<VAR>x : α<VAR>hx : x ∉ s<GOAL>(↑(Sym.fill x m s)).multinomial = n.choose ↑m * (↑s).multinomial
<VAR>n : ℕ<GOAL>(Nat.bit true n).bitIndices = 0 :: List.map (fun x => x + 1) n.bitIndices
<VAR>n : ℕ<GOAL>(Nat.bit false n).bitIndices = List.map (fun x => x + 1) n.bitIndices
<VAR>n : ℕ<GOAL>(2 * n + 1).bitIndices = 0 :: List.map (fun x => x + 1) n.bitIndices
<VAR>n : ℕ<GOAL>(2 * n).bitIndices = List.map (fun x => x + 1) n.bitIndices
<VAR>n : ℕ<GOAL>List.Sorted (fun x x_1 => x < x_1) n.bitIndices
<VAR>k n : ℕ<GOAL>(2 ^ k * n).bitIndices = List.map (fun x => x + k) n.bitIndices
<VAR>k : ℕ<GOAL>(2 ^ k).bitIndices = [k]
<VAR>n : ℕ<GOAL>(List.map (fun i => 2 ^ i) n.bitIndices).sum = n
<VAR>L : List ℕ<VAR>hL : List.Sorted (fun x x_1 => x < x_1) L<GOAL>(List.map (fun i => 2 ^ i) L).sum.bitIndices = L
<VAR>n : ℕ<GOAL>n ∉ n.bitIndices
<VAR>n : ℕ<VAR>l : List ℕ<GOAL>l.IsZeckendorfRep → (∀ a ∈ (l ++ [0]).head?, a < n) → (List.map Nat.fib l).sum < Nat.fib n
<VAR>n : ℕ<GOAL>Nat.fib n.greatestFib ≤ n
<VAR>m n : ℕ<GOAL>m ≤ n.greatestFib ↔ Nat.fib m ≤ n
<VAR>m n : ℕ<GOAL>m.greatestFib < n ↔ m < Nat.fib n
<VAR>n : ℕ<GOAL>n < Nat.fib (n.greatestFib + 1)
<VAR>n : ℕ<GOAL>n ≠ 1 → (Nat.fib n).greatestFib = n
<VAR>n : ℕ<GOAL>n.greatestFib = 0 ↔ n = 0
<VAR>n : ℕ<GOAL>n.greatestFib ≠ 0 ↔ n ≠ 0
<VAR>n : ℕ<GOAL>0 < n.greatestFib ↔ 0 < n
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(n - Nat.fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
<VAR>m : ℕ<VAR>hm : 0 < m<GOAL>m - Nat.fib m.greatestFib < m
<VAR>n : ℕ<GOAL>(n + 1).zeckendorf = (n + 1).greatestFib :: (n + 1 - Nat.fib (n + 1).greatestFib).zeckendorf
<VAR>n : ℕ<GOAL>0 < n → n.zeckendorf = n.greatestFib :: (n - Nat.fib n.greatestFib).zeckendorf
<VAR>n : ℕ<GOAL>n.zeckendorf.IsZeckendorfRep
<VAR>l : List ℕ<GOAL>l.IsZeckendorfRep → (List.map Nat.fib l).sum.zeckendorf = l
<VAR>n : ℕ<GOAL>(List.map Nat.fib n.zeckendorf).sum = n
<VAR>self : FP.FloatCfg<GOAL>0 < FP.FloatCfg.prec
<VAR>self : FP.FloatCfg<GOAL>FP.FloatCfg.prec ≤ FP.FloatCfg.emax
<VAR>C : FP.FloatCfg<GOAL>FP.ValidFinite FP.emin 0
<VAR>n p : ℕ<VAR>h : n < p<GOAL>n.factorization p = 0
<VAR>n : ℕ<GOAL>n.factorization 1 = 0
<VAR>n p : ℕ<VAR>hn : n.factorization p ≠ 0<GOAL>p ∣ n
<VAR>p r : ℕ<VAR>i : ℕ<VAR>pp : Nat.Prime p<VAR>hr0 : r ≠ 0<GOAL>¬p ∣ r ↔ (p * i + r).factorization p = 0
<VAR>n : ℕ<GOAL>n.factorization = 0 ↔ n = 0 ∨ n = 1
<VAR>n : ℕ<VAR>β : Type u_1<VAR>CommMonoid β<VAR>f : ℕ → ℕ → β<GOAL>n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p)
<VAR>n : ℕ<VAR>β : Type u_1<VAR>CommMonoid β<VAR>f : ℕ → β<GOAL>∏ p ∈ n.primeFactors, f p = n.factorization.prod fun p x => f p
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p.factorization p = 1
<VAR>n p k : ℕ<VAR>hn : n ≠ 0<VAR>h : n.factorization = Finsupp.single p k<GOAL>n = p ^ k
<VAR>p q : ℕ<VAR>hp : Nat.Prime p<VAR>h : p.factorization q ≠ 0<GOAL>p = q
<VAR>n : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hn : n ≠ 0<VAR>hf : ∀ p ∈ f.support, Nat.Prime p<GOAL>f = n.factorization ↔ (f.prod fun x x_1 => x ^ x_1) = n
<VAR>f : ℕ →₀ ℕ<VAR>hf : ∀ p ∈ f.support, Nat.Prime p<GOAL>↑(Nat.factorizationEquiv.symm ⟨f, hf⟩) = f.prod fun x x_1 => x ^ x_1
<VAR>n p : ℕ<VAR>hp : ¬Nat.Prime p<GOAL>p ^ n.factorization p = 1
<VAR>n p : ℕ<VAR>hp : ¬Nat.Prime p<GOAL>n / p ^ n.factorization p = n
<VAR>n p : ℕ<GOAL>n / p ^ n.factorization p ∣ n
<VAR>n p : ℕ<GOAL>0 < p ^ n.factorization p
<VAR>n : ℕ<VAR>p : ℕ<VAR>hn : n ≠ 0<GOAL>p ^ n.factorization p ≤ n
<VAR>n : ℕ<VAR>p : ℕ<VAR>hn : n ≠ 0<GOAL>0 < n / p ^ n.factorization p
<VAR>n p : ℕ<GOAL>n / p ^ n.factorization p ≤ n
<VAR>n p : ℕ<GOAL>p ^ n.factorization p * (n / p ^ n.factorization p) = n
<VAR>a b : ℕ<VAR>p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
<VAR>a b p : ℕ<GOAL>a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
<VAR>n : ℕ<VAR>p : ℕ<VAR>hn : n ≠ 0<GOAL>n.factorization p < n
<VAR>n p b : ℕ<VAR>hb : n ≤ p ^ b<GOAL>n.factorization p ≤ b
<VAR>d n : ℕ<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>(∀ (p : ℕ), Nat.Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n
<VAR>a b : ℕ<VAR>hb : b ≠ 0<GOAL>a.factorization ≤ (a * b).factorization
<VAR>a b : ℕ<VAR>ha : a ≠ 0<GOAL>b.factorization ≤ (a * b).factorization
<VAR>p k n : ℕ<VAR>pp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>p ^ k ∣ n ↔ k ≤ n.factorization p
<VAR>p k n : ℕ<VAR>pp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p
<VAR>p n : ℕ<VAR>pp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>p ∣ n ↔ 1 ≤ n.factorization p
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hab : a < b<GOAL>∃ p, a.factorization p < b.factorization p
<VAR>d n : ℕ<VAR>h : d ∣ n<GOAL>(n / d).factorization = n.factorization - d.factorization
<VAR>n p : ℕ<VAR>hn : n ≠ 0<VAR>pp : Nat.Prime p<VAR>h : p ∣ n<GOAL>p ∣ p ^ n.factorization p
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>¬p ∣ n / p ^ n.factorization p
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>p.Coprime (n / p ^ n.factorization p)
<VAR>n p : ℕ<GOAL>(n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
<VAR>p d n : ℕ<VAR>hdn : d ∣ n<VAR>hpd : ¬p ∣ d<GOAL>d ∣ n / p ^ n.factorization p
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>hp : p ≠ 1<GOAL>∃ e n', ¬p ∣ n' ∧ n = p ^ e * n'
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∃ k m, Odd m ∧ n = 2 ^ k * m
<VAR>d n : ℕ<VAR>hd : d ≠ 0<VAR>hdn : d ≤ n<GOAL>d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization
<VAR>a b : ℕ<VAR>hb0 : b ≠ 0<VAR>hab : a ∣ b<VAR>p : ℕ<GOAL>p ^ a.factorization p ∣ p ^ b.factorization p
<VAR>a b : ℕ<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<GOAL>(∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b
<VAR>a b : ℕ<VAR>hab : a ∣ b<VAR>p : ℕ<GOAL>a / p ^ a.factorization p ∣ b / p ^ b.factorization p
<VAR>a b : ℕ<GOAL>(∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b
<VAR>n d : ℕ<GOAL>d ∣ n ↔ ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ d → p ^ k ∣ n
<VAR>n : ℕ<GOAL>∏ p ∈ n.primeFactors, p ∣ n
<VAR>a b : ℕ<VAR>ha_pos : a ≠ 0<VAR>hb_pos : b ≠ 0<GOAL>(a.gcd b).factorization = a.factorization ⊓ b.factorization
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.lcm b).factorization = a.factorization ⊔ b.factorization
<VAR>b : ℕ<GOAL>Nat.factorizationLCMLeft 0 b = 1
<VAR>a : ℕ<GOAL>a.factorizationLCMLeft 0 = 1
<VAR>b : ℕ<GOAL>Nat.factorizationLCMRight 0 b = 1
<VAR>a : ℕ<GOAL>a.factorizationLCMRight 0 = 1
<VAR>a b : ℕ<GOAL>0 < a.factorizationLCMLeft b
<VAR>a b : ℕ<GOAL>0 < a.factorizationLCMRight b
<VAR>a b : ℕ<GOAL>(a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b
<VAR>a b : ℕ<GOAL>a.factorizationLCMLeft b ∣ a
<VAR>a b : ℕ<GOAL>a.factorizationLCMRight b ∣ b
<VAR>β : Type u_1<VAR>CommMonoid β<VAR>m n : ℕ<VAR>f : ℕ → β<GOAL>(m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
<VAR>β : Type u_1<VAR>AddCommMonoid β<VAR>m n : ℕ<VAR>f : ℕ → β<GOAL>(m.gcd n).primeFactors.sum f + (m * n).primeFactors.sum f = m.primeFactors.sum f + n.primeFactors.sum f
<VAR>n p : ℕ<VAR>pp : Nat.Prime p<VAR>hn : n ≠ 0<GOAL>{i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)
<VAR>n : ℕ<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>Finset.Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Finset.Ico 1 n)
<VAR>n : ℕ<VAR>p : ℕ<VAR>pp : Nat.Prime p<GOAL>n.factorization p = (Finset.filter (fun i => p ^ i ∣ n) (Finset.Ico 1 n)).card
<VAR>n p b : ℕ<VAR>pp : Nat.Prime p<VAR>hn : n ≠ 0<VAR>hb : n ≤ p ^ b<GOAL>Finset.filter (fun i => p ^ i ∣ n) (Finset.Ico 1 n) = Finset.filter (fun i => p ^ i ∣ n) (Finset.Icc 1 b)
<VAR>p a b : ℕ<VAR>hab : a.Coprime b<VAR>hpa : p ∈ a.primeFactorsList<GOAL>(a * b).factorization p = a.factorization p
<VAR>p a b : ℕ<VAR>hab : a.Coprime b<VAR>hpb : p ∈ b.primeFactorsList<GOAL>(a * b).factorization p = b.factorization p
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a = b ↔ ∀ (p : ℕ), Nat.Prime p → padicValNat p a = padicValNat p b
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>pr : n < m<GOAL>∏ p ∈ Finset.filter Nat.Prime (Finset.range m), p ^ padicValNat p n = n
<VAR>n p : ℕ<GOAL>(Finset.filter (fun e => p ∣ e + 1) (Finset.range n)).card = n / p
<VAR>n p : ℕ<GOAL>(Finset.filter (fun x => p ∣ x) (Finset.Ioc 0 n)).card = n / p
<VAR>N n : ℕ<GOAL>(Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)).card = N / n
<VAR>m n b : ℕ<VAR>hm : m ≠ 1<VAR>hn : 0 < n<VAR>hb : Nat.log m n < b<GOAL>multiplicity m n = ↑(Finset.filter (fun i => m ^ i ∣ n) (Finset.Ico 1 b)).card
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p 1 = 0
<VAR>p m n : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p (m * n) = multiplicity p m + multiplicity p n
<VAR>p m n : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p (m ^ n) = n • multiplicity p m
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p p = 1
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p (p ^ n) = ↑n
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n b : ℕ<GOAL>Nat.log p n < b → multiplicity p n ! = ↑(∑ i ∈ Finset.Ico 1 b, n / p ^ i)