ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<GOAL>(p - 1) * (multiplicity p n !).get ⋯ = n - (p.digits n).sum
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Nat.Prime p<GOAL>multiplicity p (p * n)! = multiplicity p n ! + ↑n
<VAR>p n r b : ℕ<VAR>hp : Nat.Prime p<VAR>hbn : Nat.log p n < b<GOAL>p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Finset.Ico 1 b, n / p ^ i
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n : ℕ<GOAL>multiplicity p n ! ≤ ↑(n / (p - 1))
<VAR>p n b k : ℕ<VAR>hp : Nat.Prime p<VAR>hkn : k ≤ n<GOAL>∑ i ∈ Finset.Ico 1 b, n / p ^ i = ∑ i ∈ Finset.Ico 1 b, k / p ^ i + ∑ i ∈ Finset.Ico 1 b, (n - k) / p ^ i + (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Nat.Prime p<VAR>hnb : Nat.log p (n + k) < b<GOAL>multiplicity p ((n + k).choose k) = ↑(Finset.filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Nat.Prime p<VAR>hkn : k ≤ n<VAR>hnb : Nat.log p n < b<GOAL>multiplicity p (n.choose k) = ↑(Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n k : ℕ<GOAL>multiplicity p n ≤ multiplicity p (n.choose k) + multiplicity p k
<VAR>p n k : ℕ<VAR>hp : Nat.Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<GOAL>multiplicity p ((p ^ n).choose k) + multiplicity p k = ↑n
<VAR>p n k : ℕ<VAR>hp : Nat.Prime p<VAR>hkn : k ≤ p ^ n<VAR>hk0 : k ≠ 0<GOAL>multiplicity p ((p ^ n).choose k) = ↑(n - (multiplicity p k).get ⋯)
<VAR>p n k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<VAR>hkp : k ≠ p ^ n<GOAL>p ∣ (p ^ n).choose k
<VAR>p n k : ℕ<VAR>hp : Nat.Prime p<GOAL>p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n
<VAR>n : ℕ<GOAL>n ≠ 0 → multiplicity 2 n ! < ↑n
<VAR>n : ℕ<GOAL>Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1)
<VAR>n : ℕ<GOAL>n ≠ 0 → Nat.fib (n + 1) = Nat.fib (n - 1) + Nat.fib n
<VAR>n : ℕ<GOAL>Nat.fib n ≤ Nat.fib (n + 1)
<VAR>n : ℕ<GOAL>Nat.fib n = 0 ↔ n = 0
<VAR>n : ℕ<GOAL>0 < Nat.fib n ↔ 0 < n
<VAR>n : ℕ<GOAL>Nat.fib (n + 2) - Nat.fib (n + 1) = Nat.fib n
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>Nat.fib n < Nat.fib (n + 1)
<GOAL>StrictMono fun n => Nat.fib (n + 2)
<GOAL>StrictMonoOn Nat.fib (Set.Ici 2)
<VAR>m : ℕ<VAR>hm : 2 ≤ m<VAR>n : ℕ<GOAL>Nat.fib m < Nat.fib n ↔ m < n
<VAR>n : ℕ<VAR>five_le_n : 5 ≤ n<GOAL>n ≤ Nat.fib n
<VAR>n : ℕ<GOAL>n ≤ Nat.fib n + 1
<VAR>n : ℕ<GOAL>(Nat.fib n).Coprime (Nat.fib (n + 1))
<VAR>m n : ℕ<GOAL>Nat.fib (m + n + 1) = Nat.fib m * Nat.fib n + Nat.fib (m + 1) * Nat.fib (n + 1)
<VAR>n : ℕ<GOAL>Nat.fib (2 * n) = Nat.fib n * (2 * Nat.fib (n + 1) - Nat.fib n)
<VAR>n : ℕ<GOAL>Nat.fib (2 * n + 1) = Nat.fib (n + 1) ^ 2 + Nat.fib n ^ 2
<VAR>n : ℕ<GOAL>Nat.fib (2 * n + 2) = Nat.fib (n + 1) * (2 * Nat.fib n + Nat.fib (n + 1))
<VAR>n : ℕ<GOAL>(Nat.bit false n).fastFibAux = let p := n.fastFibAux; (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
<VAR>n : ℕ<GOAL>(Nat.bit true n).fastFibAux = let p := n.fastFibAux; (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
<VAR>n : ℕ<GOAL>n.fastFibAux = (Nat.fib n, Nat.fib (n + 1))
<VAR>n : ℕ<GOAL>n.fastFib = Nat.fib n
<VAR>m n : ℕ<GOAL>(Nat.fib m).gcd (Nat.fib (n + m)) = (Nat.fib m).gcd (Nat.fib n)
<VAR>m n k : ℕ<GOAL>(Nat.fib m).gcd (Nat.fib (n + k * m)) = (Nat.fib m).gcd (Nat.fib n)
<VAR>m n : ℕ<GOAL>Nat.fib (m.gcd n) = (Nat.fib m).gcd (Nat.fib n)
<VAR>m n : ℕ<VAR>h : m ∣ n<GOAL>Nat.fib m ∣ Nat.fib n
<VAR>n : ℕ<GOAL>Nat.fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
<VAR>n : ℕ<GOAL>Nat.fib (n + 1) = ∑ k ∈ Finset.range n, Nat.fib k + 1
<VAR>α : Type u<VAR>a b : Array α<VAR>i j : Nat<VAR>h : j ≤ a.size<GOAL>(a ++ b).extract i j = a.extract i j
<VAR>α : Type u<VAR>a b : Array α<VAR>i j : Nat<VAR>h : a.size ≤ i<GOAL>(a ++ b).extract i j = b.extract (i - a.size) (j - a.size)
<VAR>α : Type u<VAR>l p : Nat<VAR>a : Array α<VAR>h : a.size ≤ l<GOAL>a.extract p l = a.extract p a.size
<VAR>α : Type u<VAR>s1 e2 e1 s2 : Nat<VAR>a : Array α<VAR>h : s1 + e2 ≤ e1<GOAL>(a.extract s1 e1).extract s2 e2 = a.extract (s1 + s2) (s1 + e2)
<VAR>f : Bool → Bool → Bool<VAR>m : ℕ<GOAL>Nat.bitwise f 0 m = if f false true = true then m else 0
<VAR>f : Bool → Bool → Bool<VAR>n : ℕ<GOAL>Nat.bitwise f n 0 = if f true false = true then n else 0
<VAR>f : Bool → Bool → Bool<GOAL>Nat.bitwise f 0 0 = 0
<VAR>f : Bool → Bool → Bool<VAR>n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<GOAL>Nat.bitwise f n m = Nat.bit (f n.bodd m.bodd) (Nat.bitwise f (n / 2) (m / 2))
<VAR>C : ℕ → Sort u_1<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>Nat.binaryRec z f n = ⋯ ▸ f n.bodd n.div2 (Nat.binaryRec z f n.div2)
<VAR>f : Bool → Bool → Bool<VAR>h : f false false = false := by rfl<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)
<VAR>a : Bool<VAR>x : ℕ<GOAL>Nat.bit a x % 2 = if a = true then 1 else 0
<VAR>a : Bool<VAR>x : ℕ<GOAL>Nat.bit a x % 2 = 0 ↔ (!a) = true
<VAR>a : Bool<VAR>x : ℕ<GOAL>Nat.bit a x % 2 = 1 ↔ a = true
<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>Nat.bit a m ||| Nat.bit b n = Nat.bit (a || b) (m ||| n)
<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>Nat.bit a m &&& Nat.bit b n = Nat.bit (a && b) (m &&& n)
<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(Nat.bit a m).ldiff (Nat.bit b n) = Nat.bit (a && !b) (m.ldiff n)
<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>Nat.bit a m ^^^ Nat.bit b n = Nat.bit (a != b) (m ^^^ n)
<VAR>m n k : ℕ<GOAL>(m ||| n).testBit k = (m.testBit k || n.testBit k)
<VAR>m n k : ℕ<GOAL>(m &&& n).testBit k = (m.testBit k && n.testBit k)
<VAR>m n k : ℕ<GOAL>(m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
<GOAL>Nat.bit true = fun x => 2 * x + 1
<VAR>n : ℕ<VAR>b : Bool<GOAL>Nat.bit b n ≠ 0 ↔ n = 0 → b = true
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>ham : m = 0 → a = true<VAR>hbn : n = 0 → b = true<GOAL>Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)
<VAR>f : Bool → Bool → Bool<GOAL>Nat.bitwise f = Nat.binaryRec (fun n => bif f false true then n else 0) fun a m Ia => Nat.binaryRec (bif f true false then Nat.bit a m else 0) fun b n x => Nat.bit (f a b) (Ia n)
<VAR>n : ℕ<VAR>h : ∀ (i : ℕ), n.testBit i = false<GOAL>n = 0
<VAR>n i : ℕ<GOAL>n.testBit i = n.bits.getI i
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
<VAR>n m : ℕ<VAR>i : ℕ<VAR>hn : n.testBit i = false<VAR>hm : m.testBit i = true<VAR>hnm : ∀ (j : ℕ), i < j → n.testBit j = m.testBit j<GOAL>n < m
<VAR>n m : ℕ<GOAL>((2 ^ n).testBit m = true) = (n = m)
<VAR>f : Bool → Bool → Bool<GOAL>Nat.bitwise (Function.swap f) = Function.swap (Nat.bitwise f)
<VAR>f : Bool → Bool → Bool<VAR>hf : ∀ (b b' : Bool), f b b' = f b' b<VAR>n m : ℕ<GOAL>Nat.bitwise f n m = Nat.bitwise f m n
<VAR>n m : ℕ<GOAL>n ||| m = m ||| n
<VAR>n m : ℕ<GOAL>n &&& m = m &&& n
<VAR>n m : ℕ<GOAL>n ^^^ m = m ^^^ n
<VAR>n : ℕ<GOAL>0 ^^^ n = n
<VAR>n : ℕ<GOAL>n ^^^ 0 = n
<VAR>n m k : ℕ<GOAL>n &&& m &&& k = n &&& (m &&& k)
<VAR>n : ℕ<GOAL>n ^^^ n = 0
<VAR>n : ℕ<GOAL>Function.Injective (HXor.hXor n)
<VAR>n : ℕ<GOAL>Function.Injective fun m => m ^^^ n
<VAR>n m m' : ℕ<GOAL>n ^^^ m = n ^^^ m' ↔ m = m'
<VAR>n m m' : ℕ<GOAL>m ^^^ n = m' ^^^ n ↔ m = m'
<VAR>n m : ℕ<GOAL>n ^^^ m ≠ 0 ↔ n ≠ m
<VAR>a b c : ℕ<VAR>h : a ≠ b ^^^ c<GOAL>b ^^^ c < a ∨ a ^^^ c < b ∨ a ^^^ b < c
<VAR>a b c : ℕ<VAR>h : a < b ^^^ c<GOAL>a ^^^ c < b ∨ a ^^^ b < c
<VAR>b : Bool<VAR>x n : ℕ<GOAL>Nat.bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n
<VAR>f : Bool → Bool → Bool<VAR>x y n : ℕ<VAR>hx : x < 2 ^ n<VAR>hy : y < 2 ^ n<GOAL>Nat.bitwise f x y < 2 ^ n
<GOAL>⇑ENat.toENNRealOrderEmbedding = ENat.toENNReal
<GOAL>⇑ENat.toENNRealRingHom = ENat.toENNReal
<VAR>x : ℕ∞<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>m n : ℕ∞<GOAL>↑(min m n) = min ↑m ↑n
<VAR>m n : ℕ∞<GOAL>↑(max m n) = max ↑m ↑n
<VAR>m n : ℕ∞<GOAL>↑(m - n) = ↑m - ↑n
<VAR>x y : ℕ<GOAL>↑x = ↑y ↔ x = y
<VAR>x : ℕ<VAR>x.AtLeastTwo<GOAL>(OfNat.ofNat x).Dom
<VAR>x y : PartENat<GOAL>x ≤ y ↔ ∃ (h : y.Dom → x.Dom), ∀ (hy : y.Dom), x.get ⋯ ≤ y.get hy
<VAR>P : PartENat → Prop<VAR>a : PartENat<GOAL>P ⊤ → (∀ (n : ℕ), P ↑n) → P a
<VAR>x : PartENat<GOAL>⊤ + x = ⊤
<VAR>x : ℕ<GOAL>(↑x).get ⋯ = x
<VAR>x : ℕ<VAR>y : PartENat<VAR>h : (↑x + y).Dom<GOAL>(↑x + y).get h = x + y.get ⋯
<VAR>x y : PartENat<VAR>h : (x + y).Dom<GOAL>(x + y).get h = x.get ⋯ + y.get ⋯
<VAR>h : Part.Dom 0<GOAL>Part.get 0 h = 0
<VAR>h : Part.Dom 1<GOAL>Part.get 1 h = 1
<VAR>x : ℕ<VAR>x.AtLeastTwo<VAR>h : (OfNat.ofNat x).Dom<GOAL>(OfNat.ofNat x).get h = OfNat.ofNat x
<VAR>x y : PartENat<GOAL>x ≤ y → y.Dom → x.Dom
<VAR>x y : ℕ<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>x y : ℕ<GOAL>↑x < ↑y ↔ x < y
<VAR>x : PartENat<VAR>n : ℕ<GOAL>x ≤ ↑n ↔ ∃ (h : x.Dom), x.get h ≤ n
<VAR>n : ℕ<VAR>x : PartENat<GOAL>↑n < x ↔ ∀ (h : x.Dom), n < x.get h
<VAR>x : PartENat<GOAL>x = 0 ↔ x ≤ 0
<VAR>x : PartENat<GOAL>x ≠ 0 ↔ ⊥ < x
<VAR>x y : PartENat<GOAL>x < y → x.Dom
<VAR>x : ℕ<GOAL>↑x < ⊤
<VAR>x : ℕ<VAR>x.AtLeastTwo<GOAL>OfNat.ofNat x < ⊤
<VAR>x : ℕ<GOAL>↑x ≠ ⊤
<VAR>x : ℕ<VAR>x.AtLeastTwo<GOAL>OfNat.ofNat x ≠ ⊤
<VAR>x : ℕ<GOAL>¬IsMax ↑x
<VAR>x : PartENat<GOAL>¬x.Dom ↔ x = ⊤
<VAR>x y : PartENat<VAR>h : x < y<GOAL>x ≠ ⊤
<VAR>x : PartENat<GOAL>x = ⊤ ↔ ∀ (n : ℕ), ↑n < x
<VAR>x : PartENat<GOAL>x = ⊤ ↔ ∀ (n : ℕ), ↑n ≤ x
<VAR>x : PartENat<GOAL>0 < x ↔ 1 ≤ x
<VAR>x y z : PartENat<VAR>hz : z ≠ ⊤<GOAL>x + z < y + z ↔ x < y
<VAR>a b c : PartENat<VAR>ha : a ≠ ⊤<GOAL>a + b = a + c ↔ b = c
<VAR>h : Decidable (Part.Dom 0)<GOAL>PartENat.toWithTop 0 = 0
<VAR>h : Decidable (Part.Dom 1)<GOAL>PartENat.toWithTop 1 = 1
<VAR>n : ℕ<GOAL>(↑n).toWithTop = ↑n
<VAR>n : ℕ<GOAL>∀ {x : Decidable (↑n).Dom}, (↑n).toWithTop = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>∀ {x : Decidable (Part.Dom (OfNat.ofNat n))}, (OfNat.ofNat n).toWithTop = OfNat.ofNat n
<VAR>x y : PartENat<VAR>Decidable x.Dom<VAR>Decidable y.Dom<GOAL>x.toWithTop < y.toWithTop ↔ x < y
<VAR>n : ℕ∞<GOAL>∀ {x : Decidable (↑n).Dom}, (↑n).toWithTop = n
<VAR>x : PartENat<GOAL>∀ {x_1 : Decidable x.Dom}, ↑x.toWithTop = x
<VAR>x y : ℕ∞<GOAL>↑x < ↑y ↔ x < y
<VAR>x : ℕ∞<GOAL>PartENat.withTopEquiv.symm x = ↑x
<VAR>x : PartENat<GOAL>PartENat.withTopEquiv x = x.toWithTop
<GOAL>PartENat.withTopEquiv ⊤ = ⊤
<VAR>n : ℕ<GOAL>PartENat.withTopEquiv ↑n = ↑n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>PartENat.withTopEquiv (OfNat.ofNat n) = OfNat.ofNat n
<VAR>x y : PartENat<GOAL>PartENat.withTopEquiv x ≤ PartENat.withTopEquiv y ↔ x ≤ y
<VAR>x y : PartENat<GOAL>PartENat.withTopEquiv x < PartENat.withTopEquiv y ↔ x < y
<GOAL>PartENat.withTopEquiv.symm ⊤ = ⊤
<VAR>n : ℕ<GOAL>PartENat.withTopEquiv.symm ↑n = ↑n
<GOAL>PartENat.withTopEquiv.symm 0 = 0
<GOAL>PartENat.withTopEquiv.symm 1 = 1
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>PartENat.withTopEquiv.symm (OfNat.ofNat n) = OfNat.ofNat n
<VAR>x y : ℕ∞<GOAL>PartENat.withTopEquiv.symm x ≤ PartENat.withTopEquiv.symm y ↔ x ≤ y
<VAR>x y : ℕ∞<GOAL>PartENat.withTopEquiv.symm x < PartENat.withTopEquiv.symm y ↔ x < y
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>h : (PartENat.find P).Dom<GOAL>(PartENat.find P).get h = Nat.find h
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>h : ∃ n, P n<GOAL>(PartENat.find P).Dom
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>h : ∀ m ≤ n, ¬P m<GOAL>↑n < PartENat.find P
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<GOAL>↑n < PartENat.find P ↔ ∀ m ≤ n, ¬P m
<VAR>P : ℕ → Prop<VAR>DecidablePred P<VAR>n : ℕ<VAR>h : P n<GOAL>PartENat.find P ≤ ↑n
<VAR>P : ℕ → Prop<VAR>DecidablePred P<GOAL>PartENat.find P = ⊤ ↔ ∀ (n : ℕ), ¬P n
<VAR>r : ℝ<VAR>h : r ≠ 0<GOAL>r.sign = -1 ∨ r.sign = 1
<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>n.primeFactorsList.Nodup
<VAR>n : ℕ<GOAL>Squarefree n ↔ ∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ n
<VAR>n : ℕ<VAR>p : ℕ<VAR>hn : Squarefree n<GOAL>n.factorization p ≤ 1
<VAR>n p : ℕ<VAR>hn : Squarefree n<VAR>hp : Nat.Prime p<VAR>hpn : p ∣ n<GOAL>n.factorization p = 1
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn' : ∀ (p : ℕ), n.factorization p ≤ 1<GOAL>Squarefree n
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Squarefree n ↔ ∀ (p : ℕ), n.factorization p ≤ 1
<VAR>n m : ℕ<VAR>hn : Squarefree n<VAR>hm : Squarefree m<GOAL>n = m ↔ ∀ (p : ℕ), Nat.Prime p → (p ∣ n ↔ p ∣ m)
<VAR>n k : ℕ<VAR>hn : n ≠ 1<VAR>hk : k ≠ 0<GOAL>Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1
<VAR>n : ℕ<GOAL>Squarefree n ∧ IsPrimePow n ↔ Nat.Prime n
<VAR>n : ℕ<VAR>k : ℕ<VAR>pk : Nat.Prime k<VAR>dk : k ∣ n<VAR>dkk : ¬k * k ∣ n<VAR>o : Option ℕ<VAR>H : (n / k).MinSqFacProp o<GOAL>n.MinSqFacProp o
<VAR>n : ℕ<VAR>k : ℕ<VAR>n0 : 0 < n<VAR>i : ℕ<VAR>e : k = 2 * i + 3<VAR>ih : ∀ (m : ℕ), Nat.Prime m → m ∣ n → k ≤ m<GOAL>n.MinSqFacProp (n.minSqFacAux k)
<VAR>n : ℕ<GOAL>n.MinSqFacProp n.minSqFac
<VAR>n d : ℕ<VAR>h : n.minSqFac = some d<GOAL>Nat.Prime d
<VAR>n d : ℕ<VAR>h : n.minSqFac = some d<GOAL>d * d ∣ n
<VAR>n d : ℕ<VAR>h : n.minSqFac = some d<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>md : m * m ∣ n<GOAL>d ≤ m
<VAR>n : ℕ<GOAL>Squarefree n ↔ n.minSqFac = none
<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>Finset.filter Squarefree n.divisors = n.divisors
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>(Finset.filter Squarefree n.divisors).val = Multiset.map (fun x => x.val.prod) (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset.val
<VAR>n : ℕ<VAR>h0 : n ≠ 0<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>f : ℕ → α<GOAL>∑ i ∈ Finset.filter Squarefree n.divisors, f i = ∑ i ∈ (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset, f i.val.prod
<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
<VAR>n : ℕ<GOAL>∃ a b, b ^ 2 * a = n ∧ Squarefree a
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n
<VAR>m n : ℕ<VAR>h : Squarefree (m * n)<GOAL>m.Coprime n
<VAR>m n : ℕ<GOAL>Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n
<VAR>m n : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<GOAL>(m / m.gcd n).Coprime n
<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>∏ p ∈ n.primeFactors, p = n
<VAR>s : Finset ℕ<VAR>hs : ∀ p ∈ s, Nat.Prime p<GOAL>(∏ p ∈ s, p).primeFactors = s
<VAR>m n : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<GOAL>(m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors
<GOAL>Set.InvOn (fun n => n.factorization.support) (fun s => ∏ p ∈ s, p) {s | ∀ p ∈ s, Nat.Prime p} {n | Squarefree n}
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>t : Finset ℕ<VAR>ht : t ⊆ n.primeFactors<GOAL>∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a
<VAR>n : ℕ<GOAL>0 < n.succ
<VAR>m n : ℕ<GOAL>m.succ ≠ n.succ ↔ m ≠ n
<VAR>n : ℕ<GOAL>n.succ.succ ≠ 1
<VAR>n : ℕ<GOAL>1 < n.succ.succ
<VAR>n : ℕ<GOAL>¬n.succ < n
<VAR>m n : ℕ<GOAL>m.succ ≤ n ↔ m < n
<VAR>m n : ℕ<GOAL>m ≤ n.succ ↔ m ≤ n ∨ m = n.succ
<VAR>m n : ℕ<GOAL>0 < n → (m < n ↔ m ≤ n - 1)
<VAR>n : ℕ<VAR>m : ℕ<GOAL>m.pred < n → m ≤ n
<VAR>m n : ℕ<GOAL>m < n ↔ m + 1 ≤ n
<VAR>m n : ℕ<GOAL>m < 1 + n ↔ m ≤ n
<VAR>m n : ℕ<GOAL>1 + m ≤ n ↔ m < n
<VAR>n : ℕ<GOAL>1 ≤ n ↔ n ≠ 0
<VAR>n : ℕ<GOAL>1 < n ↔ n ≠ 0 ∧ n ≠ 1
<VAR>n : ℕ<GOAL>n ≤ 1 ↔ n = 0 ∨ n = 1
<VAR>n : ℕ<GOAL>n < 1 ↔ n = 0
<VAR>a b : ℕ<VAR>h : a < b<GOAL>1 ≤ b
<VAR>m n : ℕ<GOAL>min m n = 0 ↔ m = 0 ∨ n = 0
<VAR>m n : ℕ<GOAL>max m n = 0 ↔ m = 0 ∧ n = 0
<VAR>n : ℕ<GOAL>(1 + n).pred = n
<VAR>n : ℕ<GOAL>n.pred = n ↔ n = 0
<VAR>m n : ℕ<VAR>H : m = n.succ<GOAL>m.pred = n
<VAR>m n : ℕ<GOAL>n - 1 = m + 1 ↔ n = m + 2
<VAR>p : ℕ → Prop<GOAL>(p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n
<VAR>p : ℕ → Prop<GOAL>(p 0 ∨ ∃ n, p (n + 1)) ↔ ∃ n, p n
<VAR>n : ℕ<VAR>p : ℕ → Prop<GOAL>(∀ (m : ℕ), m < n + 1 → p m) ↔ (∀ (m : ℕ), m < n → p m) ∧ p n
<VAR>n : ℕ<VAR>p : ℕ → Prop<GOAL>(∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n
<VAR>n : ℕ<GOAL>n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n
<VAR>m n : ℕ<GOAL>m + n.succ - 1 = m + n
<VAR>n m : ℕ<GOAL>m.succ + n - 1 = m + n
<VAR>n m : ℕ<GOAL>n.pred - m = (n - m).pred
<VAR>n : ℕ<GOAL>n + (n - 1) = 2 * n - 1
<VAR>n : ℕ<GOAL>n - 1 + n = 2 * n - 1
<VAR>n : ℕ<GOAL>n + n.pred = (2 * n).pred
<VAR>n : ℕ<GOAL>n.pred + n = (2 * n).pred
<VAR>m n : ℕ<GOAL>m.pred ≤ n ↔ m ≤ n.succ
<VAR>m n : ℕ<VAR>h : m < n - 1<GOAL>m < n
<VAR>b : ℕ<VAR>a : ℕ<VAR>hb : b ≠ 0<GOAL>a ≤ b + (a - 1)
<VAR>m n : ℕ<GOAL>m.add n = m + n
<VAR>a b : ℕ<GOAL>a + b = a ↔ b = 0
<VAR>a b : ℕ<GOAL>a + b = b ↔ a = 0
<VAR>n : ℕ<GOAL>2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
<VAR>m n : ℕ<GOAL>m + n = max m n ↔ m = 0 ∨ n = 0
<VAR>m n : ℕ<GOAL>m + n = min m n ↔ m = 0 ∧ n = 0
<VAR>m n : ℕ<GOAL>m + n = 0 ↔ m = 0 ∧ n = 0
<VAR>m n : ℕ<GOAL>0 < m + n ↔ 0 < m ∨ 0 < n
<VAR>m n : ℕ<GOAL>m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
<VAR>m n : ℕ<GOAL>m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0
<VAR>m n : ℕ<GOAL>m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0
<VAR>m n : ℕ<GOAL>m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
<VAR>m n : ℕ<GOAL>n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
<VAR>a b c d : ℕ<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a + c + 1 < b + d
<VAR>a b c d : ℕ<VAR>h : a + c = b + d - 1<GOAL>b ≤ a ∨ d ≤ c
<VAR>m n : ℕ<GOAL>m - n.succ = m - n - 1
<VAR>a b c : ℕ<VAR>h : a = b + c<GOAL>a - b = c
<VAR>a b c : ℕ<VAR>h : c + b = a<GOAL>c = a - b
<VAR>a b c : ℕ<VAR>h : b + c = a<GOAL>c = a - b
<VAR>a b c : ℕ<GOAL>a < c - b ↔ a + b < c
<VAR>a b c : ℕ<GOAL>a < c - b ↔ b + a < c
<VAR>a b c : ℕ<VAR>hba : b ≤ a<GOAL>a - b < c ↔ a < b + c
<VAR>a b c : ℕ<VAR>hba : b ≤ a<GOAL>a - b < c ↔ a < c + b
<VAR>a b c : ℕ<VAR>h : c ≤ b<GOAL>a - c - (b - c) = a - b
<VAR>a b c : ℕ<VAR>h : c ≤ a<GOAL>a + b - (a - c) = b + c
<VAR>a b c : ℕ<VAR>hab : b ≤ a<VAR>hcb : c ≤ b<GOAL>a - b + (b - c) = a - c
<VAR>a b : ℕ<GOAL>a < b.pred ↔ a.succ < b
<VAR>a b c : ℕ<VAR>h : c ≤ a<GOAL>a - c < b - c ↔ a < b
<VAR>m n : ℕ<GOAL>m.mul n = m * n
<VAR>m n : ℕ<GOAL>0 = m * n ↔ m = 0 ∨ n = 0
<VAR>m n : ℕ<GOAL>2 * n ≠ 2 * m + 1
<VAR>a b c : ℕ<VAR>ha : a ≠ 0<GOAL>b * a = c * a ↔ b = c
<VAR>a b c : ℕ<VAR>ha : a ≠ 0<GOAL>a * b = a * c ↔ b = c
<VAR>a b c : ℕ<VAR>ha : a ≠ 0<GOAL>b * a ≠ c * a ↔ b ≠ c
<VAR>a b c : ℕ<VAR>ha : a ≠ 0<GOAL>a * b ≠ a * c ↔ b ≠ c
<VAR>a b : ℕ<VAR>ha : a ≠ 0<GOAL>a * b = a ↔ b = 1
<VAR>a b : ℕ<VAR>hb : b ≠ 0<GOAL>a * b = b ↔ a = 1
<VAR>a b : ℕ<VAR>ha : 0 < a<GOAL>a * b = a ↔ b = 1
<VAR>a b : ℕ<VAR>hb : 0 < b<GOAL>a * b = b ↔ a = 1
<VAR>a b c : ℕ<VAR>h : a * c ≤ b * c<VAR>hc : 0 < c<GOAL>a ≤ b
<VAR>m n : ℕ<GOAL>1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
<VAR>m n : ℕ<VAR>H : m * n = 1<GOAL>m = 1
<VAR>m n : ℕ<VAR>H : m * n = 1<GOAL>n = 1
<VAR>a b : ℕ<VAR>hb : 0 < b<GOAL>b < a * b ↔ 1 < a
<VAR>a b : ℕ<VAR>ha : 0 < a<GOAL>a < a * b ↔ 1 < b
<VAR>n : ℕ<VAR>h : 2 * n ≤ n<GOAL>n = 0
<VAR>m n : ℕ<VAR>hb : 2 ≤ n<VAR>h : n * m ≤ m<GOAL>m = 0
<VAR>n : ℕ<VAR>m : ℕ<VAR>hn : 0 < n<GOAL>0 < m.succ * n
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m * m ≤ n * n
<VAR>a b c d : ℕ<VAR>hac : a < c<VAR>hbd : b < d<GOAL>a * b < c * d
<VAR>m n : ℕ<VAR>h : m < n<GOAL>m * m < n * n
<VAR>m n : ℕ<GOAL>m * m ≤ n * n ↔ m ≤ n
<VAR>m n : ℕ<GOAL>m * m < n * n ↔ m < n
<VAR>n : ℕ<GOAL>n ≤ n * n
<VAR>m n : ℕ<GOAL>m * m = n * n ↔ m = n
<VAR>n : ℕ<GOAL>n < n * n ↔ 1 < n
<VAR>a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a + b - 1 ≤ a * b
<VAR>a : ℕ<VAR>ha : 2 ≤ a<VAR>b : ℕ<GOAL>2 ≤ b → a + b ≤ a * b
<VAR>a b c : ℕ<VAR>hb : 0 < b<GOAL>a / b ≤ c ↔ a ≤ b * c + (b - 1)
<VAR>a b : ℕ<GOAL>(a + 1) / (b + 2) < a + 1
<VAR>a b c : ℕ<VAR>hb : 0 < b<GOAL>a ≤ c / b ↔ a * b ≤ c
<VAR>a b c : ℕ<VAR>hb : 0 < b<GOAL>a / b < c ↔ a < c * b
<VAR>a b : ℕ<VAR>hb : 0 < b<GOAL>1 ≤ a / b ↔ b ≤ a
<VAR>a b : ℕ<VAR>hb : 0 < b<GOAL>a / b < 1 ↔ a < b
<VAR>a b c : ℕ<VAR>h : a ≤ b<GOAL>a / c ≤ b / c
<VAR>a b c : ℕ<VAR>h : a / c < b / c<GOAL>a < b
<VAR>a b : ℕ<VAR>hba : b ≤ a<VAR>hb : 0 < b<GOAL>0 < a / b
<VAR>a b c : ℕ<VAR>h : a / c < b<VAR>hc : 0 < c<GOAL>a < b * c
<VAR>a b c : ℕ<GOAL>a * (b / c) ≤ a * b / c
<VAR>a b c : ℕ<VAR>H1 : b ∣ a<VAR>H2 : a / b = c<GOAL>a = c * b
<VAR>a b : ℕ<VAR>Hd : a ∣ b<GOAL>a * (b / a) = b
<VAR>a b : ℕ<VAR>hb : 0 < b<GOAL>a < a / b * b + b
<VAR>a b d : ℕ<VAR>hda : d ∣ a<VAR>hdb : d ∣ b<GOAL>a / d = b / d ↔ a = b
<VAR>a b c d : ℕ<GOAL>b ∣ a → d ∣ c → a / b * (c / d) = a * c / (b * d)
<VAR>a b c d : ℕ<VAR>hba : b ∣ a<VAR>hdc : d ∣ c<GOAL>a * c / (b * d) = a / b * (c / d)
<VAR>m n : ℕ<VAR>hn : 2 ≤ n<VAR>h : m ≤ m / n<GOAL>m = 0
<VAR>a b c : ℕ<GOAL>a / c * b / a ≤ b / c
<VAR>n : ℕ<VAR>h : n ≤ n / 2<GOAL>n = 0
<VAR>a b : ℕ<VAR>h : a / 2 < a - b<GOAL>b ≤ a / 2
<VAR>a b : ℕ<VAR>h : a - b ≤ a / 2<GOAL>a / 2 ≤ b
<VAR>m n k : ℕ<VAR>h : m ≤ k * n<GOAL>m / k ≤ n
<VAR>m n : ℕ<GOAL>m / n ≤ m
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>2 * (n / 2) = n - 1
<VAR>a b c : ℕ<VAR>hcb : c ≤ b<VAR>hc : 0 < c<GOAL>a / b ≤ a / c
<VAR>m n : ℕ<GOAL>m / n = m ↔ m = 0 ∨ n = 1
<VAR>m n : ℕ<GOAL>m / n = (m - m % n) / n
<VAR>a b c : ℕ<VAR>hc : c ≠ 0<VAR>h : a * c = b<GOAL>a = b / c
<VAR>a b c : ℕ<VAR>hc : c ≠ 0<VAR>h : c * a = b<GOAL>a = b / c
<VAR>k x y : ℕ<VAR>h : x ≤ y / k<GOAL>x * k ≤ y
<VAR>a b c d : ℕ<GOAL>a / b * (c / d) ≤ a * c / (b * d)
<VAR>a b : ℕ<VAR>h : a < b<VAR>n : ℕ<GOAL>n ≠ 0 → a ^ n < b ^ n
<VAR>a m n : ℕ<VAR>ha : 1 < a<VAR>h : m < n<GOAL>a ^ m < a ^ n
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n ≤ b ^ n ↔ a ≤ b
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n < b ^ n ↔ a < b
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Function.Injective fun a => a ^ n
<VAR>a : ℕ<VAR>ha : 2 ≤ a<GOAL>Function.Injective fun x => a ^ x
<VAR>a n : ℕ<GOAL>a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
<VAR>a b : ℕ<VAR>ha : 1 < a<GOAL>a ^ b = a ↔ b = 1
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>a ≤ a ^ n
<VAR>a : ℕ<VAR>ha : 1 < a<VAR>n : ℕ<GOAL>n < a ^ n
<VAR>n : ℕ<GOAL>n < 2 ^ n
<VAR>n m : ℕ<VAR>h : 0 < m<GOAL>1 ≤ m ^ n
<VAR>n m : ℕ<GOAL>1 ≤ (m + 1) ^ n
<VAR>a n : ℕ<VAR>hn : n ≠ 0<VAR>ha : 1 < a<GOAL>1 < a ^ n
<VAR>n : ℕ<GOAL>2 ^ (n + 1) = 2 ^ n + 2 ^ n
<VAR>n m : ℕ<GOAL>1 < (m + 2) ^ (n + 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>1 < a ^ n ↔ 1 < a
<VAR>n : ℕ<GOAL>1 < 2 ^ (n + 1)
<VAR>a b n : ℕ<VAR>ha : 0 < a<VAR>hb : 1 < b<GOAL>n * b < a * b ^ (n + 1)
<VAR>a b : ℕ<GOAL>a ^ 2 - b ^ 2 = (a + b) * (a - b)
<VAR>a b c : ℕ<VAR>h : a ∣ b<GOAL>(b / a) ^ c = b ^ c / a ^ c
<VAR>C : ℕ → Sort u_1<VAR>h0 : C 0<VAR>h : (n : ℕ) → C n → C (n + 1)<GOAL>Nat.rec h0 h 0 = h0
<VAR>C : ℕ → Sort u_1<VAR>h0 : C 0<VAR>h : (n : ℕ) → C n → C (n + 1)<VAR>n : ℕ<GOAL>Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)
<VAR>C : ℕ → Sort u_1<VAR>h0 : C 0<VAR>h : (n : ℕ) → C n → C (n + 1)<GOAL>Nat.rec h0 h 1 = h 0 h0
<VAR>n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<GOAL>Nat.leRec refl le_succ_of_le ⋯ = refl
<VAR>m n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<VAR>h1 : n ≤ m<VAR>h2 : n ≤ m + 1<GOAL>Nat.leRec refl le_succ_of_le h2 = le_succ_of_le h1 (Nat.leRec refl le_succ_of_le h1)
<VAR>n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<GOAL>Nat.leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
<VAR>n m k : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<VAR>hnm : n ≤ m<VAR>hmk : m ≤ k<GOAL>Nat.leRec refl le_succ_of_le ⋯ = Nat.leRec (Nat.leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) hmk
<VAR>n : ℕ<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<VAR>m : ℕ<VAR>h1 : n ≤ m<VAR>h2 : n + 1 ≤ m<GOAL>Nat.leRec (le_succ_of_le ⋯ refl) (fun k h ih => le_succ_of_le ⋯ ih) h2 = Nat.leRec refl le_succ_of_le h1
<VAR>C : ℕ → Sort u_1<VAR>n : ℕ<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>x : C n<GOAL>Nat.leRecOn ⋯ (fun {k} => next) x = x
<VAR>C : ℕ → Sort u_1<VAR>n m : ℕ<VAR>h1 : n ≤ m<VAR>h2 : n ≤ m + 1<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>x : C n<GOAL>Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k} => next) x)
<VAR>C : ℕ → Sort u_1<VAR>n : ℕ<VAR>h : n ≤ n + 1<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>x : C n<GOAL>Nat.leRecOn h (fun {k} => next) x = next x
<VAR>C : ℕ → Sort u_1<VAR>n m k : ℕ<VAR>hnm : n ≤ m<VAR>hmk : m ≤ k<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>x : C n<GOAL>Nat.leRecOn ⋯ next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)
<VAR>C : ℕ → Sort u_1<VAR>n m : ℕ<VAR>next : {k : ℕ} → C k → C (k + 1)<VAR>x : C n<VAR>h1 : n ≤ m<VAR>h2 : n + 1 ≤ m<GOAL>Nat.leRecOn h2 (fun {k} => next) (next x) = Nat.leRecOn h1 (fun {k} => next) x