awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this_1 : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
nt₁ : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
na₁ : n ≤ xn hw1 j
te₁ : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this₁ : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
⊢ n ^ k % t = m % t

Tactic:
rw [← te] at nt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this_1 : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
mpr : ∀ (this : n ^ k = m % t), n ^ k = m
mpr₁ mpr₂ mpr₃ mpr₄ : ∀ (this : n ^ k = m), n ^ k = m
⊢ n ^ k = m

Tactic:
rwa [Nat.mod_eq_of_lt (Nat.cast_lt.1 nt), Nat.mod_eq_of_lt mt] at this

Premises used: Nat.mod_eq_of_lt, Iff.mp, Nat.cast_lt
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ φ n % n = 1

Tactic:
mod_eq_of_modEq (ModEq.pow_totient h) hn

Premises used: Nat.mod_eq_of_modEq, Nat.ModEq.pow_totient
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ φ n % n = 1

Tactic:
exact mod_eq_of_modEq (ModEq.pow_totient h) hn

Premises used: Nat.mod_eq_of_modEq, Nat.ModEq.pow_totient
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
rw : x ^ k % n * 1 % n = x ^ k % n
⊢ x ^ (k + φ n) % n = x ^ k % n

Tactic:
rw [pow_add, mul_mod, pow_totient_mod_eq_one hn h]

Premises used: pow_add, Nat.mul_mod, Nat.pow_totient_mod_eq_one
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ k % n * 1 % n = x ^ k % n

Tactic:
simp only [mul_one, dvd_refl, mod_mod_of_dvd]

Premises used: Nat.mod_mod_of_dvd, mul_one, dvd_refl
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k + 0 * φ n) % n = x ^ k % n

Tactic:
simp
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
succ : x ^ (k + (l * φ n + 1 * φ n)) % n = x ^ k % n
succ₁ : x ^ (k + (l * φ n + φ n)) % n = x ^ k % n
succ₂ : x ^ (k + l * φ n + φ n) % n = x ^ k % n
succ₃ : x ^ (k + l * φ n) % n = x ^ k % n
succ₄ succ₅ : x ^ k % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n

Tactic:
rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]

Premises used: add_mul, add_assoc, Nat.pow_add_totient_mod_eq, one_mul
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x k l n : ℕ
hn : 1 < n
h : x.Coprime n
zero : x ^ (k + 0 * φ n) % n = x ^ k % n
succ : ∀ (l : ℕ) (ih : x ^ (k + l * φ n) % n = x ^ k % n), x ^ (k + (l + 1) * φ n) % n = x ^ k % n
⊢ x ^ (k + l * φ n) % n = x ^ k % n

Tactic:
induction l with
  | zero => simp
  | succ l ih =>
    rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]

Premises used: add_mul, add_assoc, Nat.zero, Nat.pow_add_totient_mod_eq, Nat.succ, one_mul
-- Module: Mathlib.NumberTheory.PowModTotient
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
rw : x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
rw₁ : x ^ (k % φ n + k / φ n * φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
rw₂ : x ^ (k % φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
rw₃ : x ^ (k % φ n) % n = x ^ (k % φ n % φ n) % n
rw₄ rw₅ : x ^ (k % φ n) % n = x ^ (k % φ n) % n
⊢ x ^ k % n = x ^ (k % φ n) % n

Tactic:
rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]

Premises used: Nat.mod_mod, Nat.totient, Nat.div_add_mod', add_comm, Nat.pow_add_mul_totient_mod_eq, Nat.add_mul_mod_self_right
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ π n = π' (n + 1)

Tactic:
rfl

Premises used: Nat.primeCounting, rfl
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
zero : π (HSub.hSub (α := ℕ) 0 1) = π' 0
succ : ∀ (n : ℕ), π (n + 1 - 1) = π' (n + 1)
⊢ π (n - 1) = π' n

Tactic:
cases n
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ π (HSub.hSub (α := ℕ) 0 1) = π' 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ π (n + 1 - 1) = π' (n + 1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ Monotone π'

Tactic:
count_monotone Prime

Premises used: Nat.Prime, Nat.primeCounting', Nat.count_monotone
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ Monotone π

Tactic:
monotone_primeCounting'.comp (monotone_id.add_const _)

Premises used: Nat.monotone_primeCounting', Nat.primeCounting', monotone_id, Monotone.comp, Monotone.add_const, Nat.primeCounting, Nat.count
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ π' (nth Prime n) = n

Tactic:
count_nth_of_infinite infinite_setOf_prime _

Premises used: Nat.infinite_setOf_prime, Nat.primeCounting', Nat.count_nth_of_infinite
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ n + 2 ≤ nth Prime n

Tactic:
nth_prime_zero_eq_two ▸ (nth_strictMono infinite_setOf_prime).add_le_nat n 0

Premises used: Nat.nth_strictMono, Nat.infinite_setOf_prime, StrictMono.add_le_nat, Eq.rec, Nat.nth_prime_zero_eq_two, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ Function.Surjective π'

Tactic:
Nat.surjective_count_of_infinite_setOf infinite_setOf_prime

Premises used: Nat.infinite_setOf_prime, Nat.primeCounting', Nat.surjective_count_of_infinite_setOf
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
suffices : Function.Surjective (α := ℕ) (π ∘ fun (n : ℕ) ↦ n - 1)
⊢ Function.Surjective π

Tactic:
suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ Function.Surjective π'

Tactic:
surjective_primeCounting'

Premises used: Nat.surjective_primeCounting'
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
h : (π ∘ fun (n : ℕ) ↦ n - 1) = π'
⊢ Function.Surjective (α := ℕ) (π ∘ fun (n : ℕ) ↦ n - 1)

Tactic:
convert! surjective_primeCounting'

Premises used: Nat.surjective_primeCounting'
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
h : ∀ (x : ℕ), (π ∘ fun (n : ℕ) ↦ n - 1) x = π' x
⊢ (π ∘ fun (n : ℕ) ↦ n - 1) = π'

Tactic:
ext
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
x : ℕ
⊢ (π ∘ fun (n : ℕ) ↦ n - 1) x = π' x

Tactic:
primeCounting_sub_one _

Premises used: Nat.primeCounting_sub_one, Nat.primeCounting', Nat.primeCounting, Nat.count
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
x : ℕ
⊢ (π ∘ fun (n : ℕ) ↦ n - 1) x = π' x

Tactic:
exact primeCounting_sub_one _

Premises used: Nat.primeCounting_sub_one
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
apply : ¬BddAbove (Set.range π')
⊢ Tendsto π' atTop atTop

Tactic:
apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'

Premises used: Nat.monotone_primeCounting', Filter.tendsto_atTop_atTop_of_monotone'
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ ¬BddAbove (Set.range π')

Tactic:
simp [Set.range_eq_univ.mpr surjective_primeCounting']

Premises used: Iff.mpr, Set.range_eq_univ, Nat.surjective_primeCounting'
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ Tendsto π atTop atTop

Tactic:
(tendsto_add_atTop_iff_nat 1).mpr tendsto_primeCounting'

Premises used: Iff.mpr, Nat.primeCounting, Filter.tendsto_add_atTop_iff_nat, Nat.tendsto_primeCounting', OfNat.ofNat
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ Prime (nth Prime n)

Tactic:
nth_mem_of_infinite infinite_setOf_prime _

Premises used: Nat.infinite_setOf_prime, Nat.nth_mem_of_infinite
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
rw : count Prime n = 0 ↔ n ≤ 2
rw₁ : n ≤ nth Prime 0 ↔ n ≤ 2
rw₂ rw₃ : n ≤ 2 ↔ n ≤ 2
⊢ π' n = 0 ↔ n ≤ 2

Tactic:
rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]

Premises used: Nat.primeCounting', Nat.prime_two, Exists.intro, Nat.nth_prime_zero_eq_two, Nat.count_eq_zero
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ π n = 0 ↔ n ≤ 1

Tactic:
simp [primeCounting, -Order.add_one_le_iff]

Premises used: Nat.primeCounting, Order.add_one_le_iff
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ π 0 = 0

Tactic:
primeCounting_eq_zero_iff.mpr zero_le_one

Premises used: Iff.mpr, zero_le_one, Nat.primeCounting_eq_zero_iff
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ π 1 = 0

Tactic:
primeCounting_eq_zero_iff.mpr le_rfl

Premises used: Iff.mpr, le_rfl, Nat.primeCounting_eq_zero_iff
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ n.primesBelow = filter Prime (range n)

Tactic:
rfl

Premises used: rfl, Nat.primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ n.primesLE = filter Prime (range (n + 1))

Tactic:
rfl

Premises used: Nat.primesLE, rfl, Nat.primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ primesBelow 0 = ∅

Tactic:
decide
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ primesBelow 1 = ∅

Tactic:
decide
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ primesBelow 2 = ∅

Tactic:
decide
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ primesLE 0 = ∅

Tactic:
primesBelow_one

Premises used: Nat.primesLE, Nat.primesBelow_one
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ primesLE 1 = ∅

Tactic:
primesBelow_two

Premises used: Nat.primesLE, Nat.primesBelow_two
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
zero : primesBelow 0 = (HSub.hSub (α := ℕ) 0 1).primesLE
succ : ∀ (n : ℕ), (n + 1).primesBelow = (n + 1 - 1).primesLE
⊢ n.primesBelow = (n - 1).primesLE

Tactic:
cases n
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
⊢ primesBelow 0 = (HSub.hSub (α := ℕ) 0 1).primesLE

Tactic:
simp [primesLE]

Premises used: Nat.primesLE
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ (n + 1).primesBelow = (n + 1 - 1).primesLE

Tactic:
simp [primesLE]

Premises used: Nat.primesLE
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
k n : ℕ
⊢ n ∈ k.primesBelow ↔ n < k ∧ Prime n

Tactic:
simp [primesBelow]

Premises used: Nat.primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
⊢ p ∈ n.primesLE ↔ p ≤ n ∧ Prime p

Tactic:
simp [primesLE, mem_primesBelow]

Premises used: Nat.primesLE, Nat.mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
h : p ∈ n.primesBelow
⊢ Prime p

Tactic:
(Finset.mem_filter.mp h).2

Premises used: And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
hp : p ∈ n.primesLE
⊢ Prime p

Tactic:
prime_of_mem_primesBelow hp

Premises used: Nat.prime_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
h : p ∈ n.primesBelow
⊢ p < n

Tactic:
Finset.mem_range.mp <| Finset.mem_of_mem_filter p h

Premises used: Finset.mem_range, Finset.mem_of_mem_filter, Iff.mp
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
hp : p ∈ n.primesLE
⊢ p ≤ n

Tactic:
(mem_primesLE.mp hp).1

Premises used: Nat.mem_primesLE, And.left, Iff.mp
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
hp : p ∈ n.primesBelow
⊢ 1 < p

Tactic:
(prime_of_mem_primesBelow hp).one_lt

Premises used: Nat.Prime.one_lt, Nat.prime_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
hp : p ∈ n.primesLE
⊢ 1 < p

Tactic:
one_lt_of_mem_primesBelow hp

Premises used: Nat.one_lt_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
hp : p ∈ n.primesBelow
⊢ 2 ≤ p

Tactic:
(prime_of_mem_primesBelow hp).two_le

Premises used: Nat.Prime.two_le, Nat.prime_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
p n : ℕ
hp : p ∈ n.primesLE
⊢ 2 ≤ p

Tactic:
two_le_of_mem_primesBelow hp

Premises used: Nat.two_le_of_mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 0 n)
⊢ n.primesBelow = filter Prime (Ico 0 n)

Tactic:
ext p
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 0 n)

Tactic:
simp [primesBelow_eq_filter_range]

Premises used: Nat.primesBelow_eq_filter_range
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 0 n)
⊢ n.primesLE = filter Prime (Icc 0 n)

Tactic:
ext p
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 0 n)

Tactic:
simp [primesLE_eq_filter_range]

Premises used: Nat.primesLE_eq_filter_range
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 1 n)
⊢ n.primesBelow = filter Prime (Ico 1 n)

Tactic:
ext p
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 1 n)

Tactic:
simp +contextual [primesBelow_eq_filter_range, Nat.Prime.one_le]

Premises used: Nat.Prime.one_le, Nat.primesBelow_eq_filter_range
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 1 n)
⊢ n.primesLE = filter Prime (Icc 1 n)

Tactic:
ext p
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 1 n)

Tactic:
simp +contextual [primesLE_eq_filter_range, Nat.Prime.one_le]

Premises used: Nat.Prime.one_le, Nat.primesLE_eq_filter_range
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 2 n)
⊢ n.primesBelow = filter Prime (Ico 2 n)

Tactic:
ext p
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 2 n)

Tactic:
simp +contextual [primesBelow_eq_filter_range, Nat.Prime.two_le]

Premises used: Nat.primesBelow_eq_filter_range, Nat.Prime.two_le
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 2 n)
⊢ n.primesLE = filter Prime (Icc 2 n)

Tactic:
ext p
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n p : ℕ
⊢ p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 2 n)

Tactic:
simp +contextual [primesLE_eq_filter_range, Nat.Prime.two_le]

Premises used: Nat.Prime.two_le, Nat.primesLE_eq_filter_range
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n m : ℕ
h : n ≤ m
p : ℕ
simp : p < n → Prime p → p < m ∧ Prime p
⊢ p ∈ n.primesBelow → p ∈ m.primesBelow

Tactic:
simp [mem_primesBelow]

Premises used: Nat.mem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n m : ℕ
h : n ≤ m
p : ℕ
⊢ p < n → Prime p → p < m ∧ Prime p

Tactic:
grind
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n m : ℕ
h : n ≤ m
p : ℕ
simp : p ≤ n → Prime p → p ≤ m ∧ Prime p
⊢ p ∈ n.primesLE → p ∈ m.primesLE

Tactic:
simp [mem_primesLE]

Premises used: Nat.mem_primesLE
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n m : ℕ
h : n ≤ m
p : ℕ
⊢ p ≤ n → Prime p → p ≤ m ∧ Prime p

Tactic:
grind
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
rw : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n n.primesBelow else n.primesBelow
rw₁ : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
rw₂ :
  {p ∈ insert n (range n) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
rw₃ rw₄ :
  (if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}) =
    if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow

Tactic:
rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]

Premises used: Finset.range_add_one, Finset.filter_insert, Nat.primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ (n + 1).primesLE = if Prime (n + 1) then insert (n + 1) n.primesLE else n.primesLE

Tactic:
primesBelow_succ (n + 1)

Premises used: Nat.primesLE, Nat.primesBelow_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ n ∉ n.primesBelow

Tactic:
fun hn ↦ (lt_of_mem_primesBelow hn).false

Premises used: Nat.lt_of_mem_primesBelow, LT.lt.false, Not
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ n + 1 ∉ n.primesLE

Tactic:
notMem_primesBelow (n + 1)

Premises used: Set.Mem, setOf, HAdd.hAdd, OfNat.ofNat, Nat.notMem_primesBelow
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ #({p ∈ range n | Prime p}) = count Prime n

Tactic:
(count_eq_card_filter_range Prime n).symm

Premises used: Nat.Prime, Nat.count_eq_card_filter_range, Eq.symm
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ #({p ∈ range n | Prime p}) = count Prime n

Tactic:
exact (count_eq_card_filter_range Prime n).symm

Premises used: Nat.Prime, Nat.count_eq_card_filter_range, Eq.symm
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
n : ℕ
⊢ #n.primesLE = π n

Tactic:
simp only [primesLE, primeCounting, primesBelow_card_eq_primeCounting']

Premises used: Nat.primesLE, Nat.primeCounting, Nat.primesBelow_card_eq_primeCounting'
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
rw :
  #({x ∈ Ico 0 k | Prime x} ∪ {x ∈ Ico k (k + n) | Prime x}) ≤
    #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
⊢ π' (k + n) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
rw [primeCounting', count_eq_card_filter_range, range_eq_Ico, range_eq_Ico, ←
        Ico_union_Ico_eq_Ico (zero_le k) le_self_add, filter_union]

Premises used: Nat.zero_le, Nat.count_eq_card_filter_range, Nat.primeCounting', Finset.Ico_union_Ico_eq_Ico, Finset.range_eq_Ico, Finset.filter_union, le_self_add
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ Ico 0 k | Prime x} ∪ {x ∈ Ico k (k + n) | Prime x}) ≤
    #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
apply card_union_le

Premises used: Finset.card_union_le
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
rw : #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ count Prime k + #({p ∈ Ico k (k + n) | Prime p})
rw₁ rw₂ :
  #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤
    #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
⊢ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
rw [primeCounting', count_eq_card_filter_range]

Premises used: Nat.count_eq_card_filter_range, Nat.primeCounting'
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
bc : ∀ (p : ℕ) (hp : p ∈ Ico k (k + n)), Prime p → a.Coprime p
⊢ π' k + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({b ∈ Ico k (k + n) | a.Coprime b})

Tactic:
gcongr with p hp
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
bc : Prime p → p.Coprime a
⊢ Prime p → a.Coprime p

Tactic:
rw [coprime_comm]

Premises used: Nat.coprime_comm
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
⊢ Prime p → p.Coprime a

Tactic:
coprime_of_lt_prime h0 <| h1.trans_le (mem_Ico.1 hp).1

Premises used: And.left, LT.lt.trans_le, Nat.coprime_of_lt_prime, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
⊢ Prime p → p.Coprime a

Tactic:
exact coprime_of_lt_prime h0 <| h1.trans_le (mem_Ico.1 hp).1

Premises used: And.left, LT.lt.trans_le, Nat.coprime_of_lt_prime, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
rw : #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)
⊢ π' k + #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ π' k + φ a * (n / a + 1)

Tactic:
rw [add_le_add_iff_left]

Premises used: add_le_add_iff_left
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)

Tactic:
Ico_filter_coprime_le k n h0

Premises used: Nat.Ico_filter_coprime_le
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)

Tactic:
exact Ico_filter_coprime_le k n h0

Premises used: Nat.Ico_filter_coprime_le
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π' (k + 1 + n) ≤ π' (k + 1) + φ a * (n / a + 1)

Tactic:
primeCounting'_add_le h0 (Order.lt_add_one_iff.mpr h1) n

Premises used: Iff.mpr, Nat.primeCounting'_add_le, Order.lt_add_one_iff
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
h : k + n + 1 = k + 1 + n
⊢ π' (k + n + 1) ≤ π k + φ a * (n / a + 1)

Tactic:
convert! primeCounting'_add_le h0 (Order.lt_add_one_iff.mpr h1) n using 2

Premises used: Iff.mpr, Nat.primeCounting'_add_le, Order.lt_add_one_iff
-- Module: Mathlib.NumberTheory.PrimeCounting
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ k + n + 1 = k + 1 + n

Tactic:
omega
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k n : ℕ
hk0 : k ≠ 0
inl : ∀ (hk0 : Ne (α := ℕ) 1 0), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
inr : ∀ (hk1 : 1 < k), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
rcases (one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)

Premises used: Iff.mpr, LE.le.eq_or_lt, Nat.one_le_iff_ne_zero, rfl
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n : ℕ
hk0 : Ne (α := ℕ) 1 0
inl : ∀ (p : ℕ) (hnp : n + 1 ≤ p) (hp : Prime p), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Tactic:
rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩

Premises used: HAdd.hAdd, OfNat.ofNat, Nat.exists_infinite_primes
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n : ℕ
hk0 : Ne (α := ℕ) 1 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Tactic:
⟨p, hp, hnp, modEq_one⟩

Premises used: Nat.modEq_one, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n : ℕ
hk0 : Ne (α := ℕ) 1 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Tactic:
exact ⟨p, hp, hnp, modEq_one⟩
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
rcases :
  ∀ (k : ℕ) (hk0 : k + 1 ≠ 0) (hk1 : 1 < k + 1),
    let b := (k + 1) * n !;
    1 < (eval (↑b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs
⊢ 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs

Tactic:
rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩

Premises used: LT.lt.le, Iff.mp, le_iff_exists_add', rfl
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 2 ≤ b

Tactic:
have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
hb : 2 ≤ b
⊢ 1 ≤ b - 1

Tactic:
le_tsub_of_add_le_left hb

Premises used: le_tsub_of_add_le_left
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
hb : 2 ≤ b
⊢ b - 1 < (eval (↑b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs

Tactic:
sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'

Premises used: Polynomial.sub_one_lt_natAbs_cyclotomic_eval, LT.lt.ne', Iff.mp, Nat.succ_le_iff