awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac

Tactic:
simp [n1]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
(minFac_prime n1).pos

Premises used: Nat.Prime.pos, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
exact (minFac_prime n1).pos

Premises used: Nat.Prime.pos, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
H : 0 < n
⊢ n.minFac ≤ n

Tactic:
le_of_dvd H (minFac_dvd n)

Premises used: Nat.minFac_dvd, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m p : ℕ
pp : Prime p
h : Eq (α := ℕ) 1 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p

Tactic:
cases pp.not_dvd_one d

Premises used: Nat.Prime.not_dvd_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m p : ℕ
pp : 1 < p
h : Eq (α := ℕ) 1 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ LT.lt (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m p : ℕ
pp : 1 < p
h : Eq (α := ℕ) 1 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p

Tactic:
cases not_le_of_gt pp (le_of_dvd (by decide) d)

Premises used: not_le_of_gt, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ p.minFac = p

Tactic:
⟨fun pp =>
    ⟨pp.two_le,
      let ⟨f2, fd, _⟩ := minFac_has_prop <| ne_of_gt pp.one_lt
      ((dvd_prime pp).1 fd).resolve_left (ne_of_gt f2)⟩,
    fun ⟨p2, e⟩ => e ▸ minFac_prime (ne_of_gt p2)⟩

Premises used: Nat.Prime, Nat.Prime.one_lt, _private.0.Nat.prime_def_minFac.match_1, Eq.rec, Nat.minFac, Or.resolve_left, Nat.dvd_prime, _private.0.Nat.minFac_prime.match_1, Nat.minFac_has_prop, And.intro, Iff.intro, Iff.mp, Nat.Prime.two_le, Eq, Nat.minFac_prime, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp : Prime p
⊢ p.minFac = p

Tactic:
(prime_def_minFac.1 hp).2

Premises used: And.right, Iff.mp, Nat.prime_def_minFac
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ decidablePrime = decidablePrime'

Tactic:
subsingleton
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
⊢ ¬Prime n ↔ n.minFac < n

Tactic:
(not_congr <| prime_def_minFac.trans <| and_iff_right n2).trans <|
    (lt_iff_le_and_ne.trans <| and_iff_right <| minFac_le <| le_of_succ_le n2).symm

Premises used: lt_iff_le_and_ne, Nat.le_of_succ_le, Nat.minFac_le, and_iff_right, Iff.trans, Iff.symm, Nat.prime_def_minFac, not_congr
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
rw : ¬LT.lt (α := ℕ) 0 0
⊢ ¬0 < n

Tactic:
rw [h0, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬LT.lt (α := ℕ) 0 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac * 1
⊢ n = n.minFac

Tactic:
rw [mul_one] at h1

Premises used: mul_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac
⊢ n < 2

Tactic:
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false,
      not_le] at np

Premises used: not_le, not_and_or, not_true, or_false, eq_self_iff_true, Nat.prime_def_minFac
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac
np₁ : n < 2
⊢ n = n.minFac

Tactic:
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false,
      not_le] at np

Premises used: not_le, not_and_or, not_true, or_false, eq_self_iff_true, Nat.prime_def_minFac
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
rw : minFac 1 ≤ 1 / minFac 1
rw₁ : 1 ≤ 1 / 1
rw₂ rw₃ : LE.le (α := ℕ) 1 1
⊢ n.minFac ≤ n / n.minFac

Tactic:
rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]

Premises used: Nat.succ_le_of_lt, Nat.minFac_one, Nat.div_one, le_antisymm, Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
a : n
a₁ : n.minFac
| n / n.minFac

Tactic:
congr
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
a : n.minFac * (x + 2)
| n

Tactic:
rw [hx]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
a : n.minFac * (x + 2)
a₁ : n.minFac
| n / n.minFac

Tactic:
congr
      rw [hx]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
conv_rhs : n.minFac ≤ n.minFac * (x + 2) / n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
conv_rhs =>
      congr
      rw [hx]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
rw : n.minFac ≤ x + 2
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac

Tactic:
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]

Premises used: Nat.mul_div_cancel_left, Nat.minFac_pos
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
rwa rwa₁ rwa₂ rwa₃ : n = n.minFac * (x + 2)
⊢ n = (x + 2) * n.minFac

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ x + 2

Tactic:
exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩

Premises used: Nat.minFac_le_of_dvd, Nat.le_add_left, Nat.minFac, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
w : 0 < n
h : ¬Prime n
⊢ HPow.hPow (β := ℕ) n.minFac 2 ≤ n

Tactic:
have t : minFac n ≤ n / minFac n := minFac_le_div w h
  calc
    minFac n ^ 2 = minFac n * minFac n := sq (minFac n)
    _ ≤ n / minFac n * minFac n := Nat.mul_le_mul_right (minFac n) t
    _ ≤ n := div_mul_le_self n (minFac n)

Premises used: Trans.trans, Nat.div_mul_le_self, Nat.mul_le_mul_right, Nat.minFac, sq, Nat.minFac_le_div
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
mp : n.minFac = 1 → n = 1
mpr : n = 1 → n.minFac = 1
⊢ n.minFac = 1 ↔ n = 1

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 1
mp : ∀ (hn : ¬n = 1), False
⊢ n = 1

Tactic:
by_contra hn
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
⊢ Prime n.minFac

Tactic:
have := minFac_prime hn
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime n.minFac
⊢ Prime 1

Tactic:
rw [h] at this
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime 1
⊢ False

Tactic:
not_prime_one this

Premises used: Nat.not_prime_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime 1
⊢ False

Tactic:
exact not_prime_one this

Premises used: Nat.not_prime_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
mp : n.minFac = 2 → 2 ∣ n
mpr : 2 ∣ n → n.minFac = 2
⊢ n.minFac = 2 ↔ 2 ∣ n

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 2
mp : n.minFac ∣ n
⊢ 2 ∣ n

Tactic:
rw [← h]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 2
⊢ n.minFac ∣ n

Tactic:
minFac_dvd n

Premises used: Nat.minFac_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : n.minFac = 2
⊢ n.minFac ∣ n

Tactic:
exact minFac_dvd n

Premises used: Nat.minFac_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
⊢ n.minFac ≤ 2

Tactic:
have ub := minFac_le_of_dvd (le_refl 2) h
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
⊢ 0 < n.minFac

Tactic:
have lb := minFac_pos n
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
⊢ n.minFac = 2

Tactic:
ub.eq_or_lt.resolve_right fun h' => ?_

Premises used: LE.le.eq_or_lt, Or.resolve_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
mpr : ∀ (h' : n.minFac < 2), False
⊢ n.minFac = 2

Tactic:
refine ub.eq_or_lt.resolve_right fun h' => ?_

Premises used: LE.le.eq_or_lt, Or.resolve_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : n.minFac = 1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
mpr : n.minFac = 1
⊢ False

Tactic:
suffices n.minFac = 1 by simp_all
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
⊢ n.minFac = 1

Tactic:
(le_antisymm (Nat.succ_le_of_lt lb) (Nat.lt_succ_iff.mp h')).symm

Premises used: Nat.succ_le_of_lt, le_antisymm, Nat.lt_succ_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
⊢ n.minFac = 1

Tactic:
exact (le_antisymm (Nat.succ_le_of_lt lb) (Nat.lt_succ_iff.mp h')).symm

Premises used: Nat.succ_le_of_lt, le_antisymm, Nat.lt_succ_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
k : ℕ
h : 1 < k + 2
⊢ k + 2 ≠ 1

Tactic:
apply Nat.ne_of_gt

Premises used: Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
k : ℕ
h : 0 < k + 1
⊢ 1 < k + 2

Tactic:
apply Nat.succ_lt_succ

Premises used: Nat.succ_lt_succ
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
k : ℕ
⊢ 0 < k + 1

Tactic:
apply Nat.zero_lt_succ

Premises used: Nat.zero_lt_succ
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
hn : n ≠ 1
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ n

Tactic:
⟨minFac n, minFac_prime hn, minFac_dvd _⟩

Premises used: Nat.minFac, Nat.minFac_dvd, And.intro, Exists.intro, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
by_contra : ∀ (g2 : ¬m.gcd n = 1), False
⊢ m.gcd n = 1

Tactic:
by_contra g2
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
obtain : ∀ (p : ℕ) (hp : Prime p) (hpdvd : p ∣ m.gcd n), False
⊢ False

Tactic:
obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2

Premises used: Nat.exists_prime_and_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
a : p ∣ m
a₁ : p ∣ n
⊢ False

Tactic:
apply H p hp
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
a : m.gcd n ∣ m
⊢ p ∣ m

Tactic:
apply dvd_trans hpdvd

Premises used: dvd_trans
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
a : m.gcd n ∣ n
⊢ p ∣ n

Tactic:
apply dvd_trans hpdvd

Premises used: dvd_trans
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m

Tactic:
gcd_dvd_left _ _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m

Tactic:
exact gcd_dvd_left _ _

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Tactic:
gcd_dvd_right _ _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Tactic:
exact gcd_dvd_right _ _

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p n : ℕ
pp : Prime p
co : p.Coprime n
d : p ∣ n
⊢ p ∣ n * 1

Tactic:
simp [d]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p m n : ℕ
pp : Prime p
⊢ p ∣ m * n ↔ p ∣ m ∨ p ∣ n

Tactic:
⟨fun H => or_iff_not_imp_left.2 fun h => (pp.coprime_iff_not_dvd.2 h).dvd_of_dvd_mul_left H,
    Or.rec (fun h : p ∣ m => h.mul_right _) fun h : p ∣ n => h.mul_left _⟩

Premises used: Iff.mpr, Or.rec, Classical.or_iff_not_imp_left, Iff.intro, Nat.Coprime.dvd_of_dvd_mul_left, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ Prime p ↔ _root_.Prime p

Tactic:
⟨fun h => ⟨h.ne_zero, h.not_isUnit, fun _ _ => h.dvd_mul.mp⟩, Prime.irreducible⟩

Premises used: Prime.irreducible, Irreducible.not_isUnit, Nat.Prime.ne_zero, And.intro, Iff.intro, Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ Irreducible p ↔ _root_.Prime p

Tactic:
prime_iff

Premises used: Nat.Prime, Nat.prime_iff
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Function.Injective (α := { p : ℕ // Prime p }) (Subtype.val (p := fun (p : ℕ) ↦ Prime p))

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p q : Primes
⊢ (↑p : ℕ) = (↑q : ℕ) ↔ p = q

Tactic:
Subtype.ext_iff.symm

Premises used: Nat.Primes, Subtype.ext_iff, Iff.symm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
⊢ Fact (Prime 2)

Tactic:
⟨prime_two⟩

Premises used: Nat.prime_two, Fact.mk
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
⊢ Fact (Prime 3)

Tactic:
⟨prime_three⟩

Premises used: Fact.mk, Nat.prime_three
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
n p : ℕ
hp : Prime p
rw : p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1

Tactic:
rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]

Premises used: Nat.factorial_succ, Nat.Prime.dvd_mul
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
n p : ℕ
hp : Prime p
h_1 : p ≤ n + 1
h : p = n + 1
rw rw₁ : n + 1 ∣ n + 1
⊢ p ∣ n + 1

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
n p : ℕ
hp : Prime p
⊢ p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1

Tactic:
exact
      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
m n : ℕ
hm : m ≠ 1
rw : m.minFac ≤ n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
⊢ m.Coprime n ! ↔ n < m.minFac

Tactic:
rw [← not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd]

Premises used: not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
m n : ℕ
hm : m ≠ 1
mp : m.minFac ≤ n → ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
mpr : (∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n
⊢ m.minFac ≤ n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
m n : ℕ
hm : m ≠ 1
h : m.minFac ≤ n
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩

Premises used: Nat.dvd_factorial, Nat.minFac, Nat.minFac_dvd, And.intro, Exists.intro, Nat.minFac_pos, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
m n : ℕ
hm : m ≠ 1
h : m.minFac ≤ n
⊢ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
m n : ℕ
hm : m ≠ 1
p : ℕ
hp : Prime p
hdvd : p ∣ m
hdvd' : p ∣ n !
⊢ m.minFac ≤ n

Tactic:
le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

Premises used: Nat.Prime.dvd_factorial, Nat.minFac_le_of_dvd, Iff.mp, Nat.Prime.two_le, le_trans
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
m n : ℕ
hm : m ≠ 1
p : ℕ
hp : Prime p
hdvd : p ∣ m
hdvd' : p ∣ n !
⊢ m.minFac ≤ n

Tactic:
exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

Premises used: Nat.Prime.dvd_factorial, Nat.minFac_le_of_dvd, Iff.mp, Nat.Prime.two_le, le_trans
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
p n : ℕ
hp : Prime p
hn : n < p
rwa : ¬p ∣ n !
rwa₁ : ¬p ≤ n
rwa₂ rwa₃ rwa₄ rwa₅ : n < p
⊢ p.Coprime n !

Tactic:
rwa [hp.coprime_iff_not_dvd, hp.dvd_factorial, not_le]

Premises used: not_le, Nat.Prime.dvd_factorial, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
rw : p.Coprime (n ! / (n - k)!)
⊢ p.Coprime (n.descFactorial k)

Tactic:
rw [Nat.descFactorial_eq_div hk]

Premises used: Nat.descFactorial_eq_div
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ p.Coprime (n ! / (n - k)!)

Tactic:
(hp.coprime_factorial_of_lt hn).coprime_div_right ?_

Premises used: Nat.Prime.coprime_factorial_of_lt, Nat.Coprime.coprime_div_right
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
refine : (n - k)! ∣ n !
⊢ p.Coprime (n ! / (n - k)!)

Tactic:
refine (hp.coprime_factorial_of_lt hn).coprime_div_right ?_

Premises used: Nat.Prime.coprime_factorial_of_lt, Nat.Coprime.coprime_div_right
-- Module: Mathlib.Data.Nat.Prime.Factorial
Goal:
p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ (n - k)! ∣ n !

Tactic:
simp [Nat.factorial_dvd_factorial]

Premises used: Nat.factorial_dvd_factorial
-- Module: Mathlib.Data.Nat.Prime.Infinite
Goal:
n : ℕ
⊢ ∃ (p : ℕ), n ≤ p ∧ Prime p

Tactic:
let p := minFac (n ! + 1)
  have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _
  have pp : Prime p := minFac_prime f1
  have np : n ≤ p :=
    le_of_not_ge fun h =>
      have h₁ : p ∣ n ! := dvd_factorial (minFac_pos _) h
      have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
      pp.not_dvd_one h₂
  ⟨p, np, pp⟩

Premises used: Iff.mpr, Nat.dvd_factorial, Nat.succ_lt_succ, Nat.minFac, Nat.minFac_dvd, le_of_not_ge, HAdd.hAdd, Nat.factorial, And.intro, Exists.intro, Nat.Prime.not_dvd_one, Nat.minFac_pos, Nat.dvd_add_iff_right, OfNat.ofNat, Nat.factorial_pos, Nat.minFac_prime, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Infinite
Goal:
rw : ∀ (x : ℕ), ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ x < y
⊢ ¬BddAbove (α := ℕ) {p : ℕ | Prime p}

Tactic:
rw [not_bddAbove_iff]

Premises used: not_bddAbove_iff
-- Module: Mathlib.Data.Nat.Prime.Infinite
Goal:
n : ℕ
obtain : ∀ (p : ℕ) (hi : n.succ ≤ p) (hp : Prime p), ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ n < y
⊢ ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ n < y

Tactic:
obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ

Premises used: Nat.succ, Nat.exists_infinite_primes
-- Module: Mathlib.Data.Nat.Prime.Infinite
Goal:
n p : ℕ
hi : n.succ ≤ p
hp : Prime p
⊢ ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ n < y

Tactic:
⟨p, hp, hi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Prime.Infinite
Goal:
n p : ℕ
hi : n.succ ≤ p
hp : Prime p
⊢ ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ n < y

Tactic:
exact ⟨p, hp, hi⟩
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p : ℕ
hp : Prime p
a b : ℤ
h : (↑p : ℤ) ∣ a * b
⊢ p ∣ a.natAbs ∨ p ∣ b.natAbs

Tactic:
rw [← Int.dvd_natAbs, Int.natCast_dvd_natCast, Int.natAbs_mul, hp.dvd_mul] at h

Premises used: Int.dvd_natAbs, Int.natAbs_mul, Nat.Prime.dvd_mul, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
rwa : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑a.natAbs : ℤ) ∨ (↑p : ℤ) ∣ b
rwa₁ : p ∣ a.natAbs ∨ (↑p : ℤ) ∣ b
rwa₂ : p ∣ a.natAbs ∨ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b.natAbs : ℤ)
rwa₃ rwa₄ rwa₅ rwa₆ : p ∣ a.natAbs ∨ p ∣ b.natAbs
⊢ (↑p : ℤ) ∣ a ∨ (↑p : ℤ) ∣ b

Tactic:
rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]

Premises used: Int.dvd_natAbs, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p : ℕ
hp : _root_.Prime (M := ℤ) (↑p : ℤ)
h : p = 1
⊢ False

Tactic:
simp [h] at hp
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p : ℕ
hp : _root_.Prime (M := ℤ) (↑p : ℤ)
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
simpa only [Int.natCast_dvd_natCast, (Int.natCast_mul _ _).symm] using hp.2.2 a b

Premises used: Nat.cast, Int.natCast_mul, And.right, Eq.symm, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q

Tactic:
have H := dvd_antisymm (Prime.dvd_of_dvd_pow hp <| h ▸ dvd_pow_self p (succ_ne_zero m))
    (Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
H : p = q
⊢ p = q ∧ m = n

Tactic:
⟨H, succ_inj.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩

Premises used: Nat.succ_inj, Eq.rec, Nat.pow_right_injective, And.intro, Iff.mp, Nat.Prime.two_le, Eq.symm
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
H : p = q
⊢ p = q ∧ m = n

Tactic:
exact ⟨H, succ_inj.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p q m n : ℕ
hp : Prime p
hq : Prime q
hm : m ≠ 0
hn : n ≠ 0
h : p ^ m = q ^ n
obtain : ∀ (m : ℕ) (hm : m + 1 ≠ 0) (h : p ^ (m + 1) = q ^ n), p = q ∧ m + 1 = n
⊢ p = q ∧ m = n

Tactic:
obtain ⟨m, rfl⟩ := exists_eq_add_one_of_ne_zero hm

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p q n : ℕ
hp : Prime p
hq : Prime q
hn : n ≠ 0
m : ℕ
hm : m + 1 ≠ 0
h : p ^ (m + 1) = q ^ n
obtain : ∀ (n : ℕ) (hn : n + 1 ≠ 0) (h : p ^ (m + 1) = q ^ (n + 1)), p = q ∧ m + 1 = n + 1
⊢ p = q ∧ m + 1 = n

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_add_one_of_ne_zero hn

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
p q : ℕ
hp : Prime p
hq : Prime q
m : ℕ
hm : m + 1 ≠ 0
n : ℕ
hn : n + 1 ≠ 0
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m + 1 = n + 1

Tactic:
simpa using hp.pow_inj hq h

Premises used: Nat.Prime.pow_inj
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
n : ℕ
⊢ Prime (M := ℤ) (OfNat.ofNat n) ↔ Nat.Prime (OfNat.ofNat n)

Tactic:
Nat.prime_iff_prime_int.symm

Premises used: Nat.prime_iff_prime_int, Iff.symm
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
⊢ Prime (M := ℤ) 2

Tactic:
prime_ofNat_iff.mpr Nat.prime_two

Premises used: Iff.mpr, Nat.prime_two, Int.prime_ofNat_iff
-- Module: Mathlib.Data.Nat.Prime.Int
Goal:
⊢ Prime (M := ℤ) 3

Tactic:
prime_ofNat_iff.mpr Nat.prime_three

Premises used: Iff.mpr, Int.prime_ofNat_iff, Nat.prime_three
-- Module: Mathlib.Data.Nat.Prime.Nth
Goal:
⊢ nth Prime 0 = 2

Tactic:
nth_count prime_two

Premises used: cond, List.countP.go, Nat.prime_two, Nat.count, Nat.nth_count
-- Module: Mathlib.Data.Nat.Prime.Nth
Goal:
⊢ nth Prime 1 = 3

Tactic:
nth_count prime_three

Premises used: cond, List.countP.go, Nat.prime_three, Nat.count, Nat.nth_count
-- Module: Mathlib.Data.Nat.Prime.Nth
Goal:
⊢ nth Prime 2 = 5

Tactic:
nth_count prime_five

Premises used: cond, Nat.prime_five, List.countP.go, Nat.count, Nat.nth_count
-- Module: Mathlib.Data.Nat.Prime.Nth
Goal:
⊢ nth Prime 3 = 7

Tactic:
nth_count prime_seven

Premises used: cond, Nat.prime_seven, List.countP.go, Nat.count, Nat.nth_count
-- Module: Mathlib.Data.Nat.Prime.Nth
Goal:
⊢ nth Prime 4 = 11

Tactic:
nth_count prime_eleven

Premises used: cond, Nat.prime_eleven, List.countP.go, Nat.count, Nat.nth_count
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
⊢ Set.Infinite (α := ℕ) {p : ℕ | Prime p}

Tactic:
Set.infinite_of_not_bddAbove not_bddAbove_setOf_prime

Premises used: Set.infinite_of_not_bddAbove, Nat.not_bddAbove_setOf_prime
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b k m n p : ℕ
⊢ Infinite Primes

Tactic:
infinite_setOf_prime.to_subtype

Premises used: Nat.Prime, Nat.infinite_setOf_prime, Set.Mem, setOf, Nat.Primes, Set.Infinite.to_subtype
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b k m n p : ℕ
⊢ Countable Primes

Tactic:
⟨⟨coeNat.coe, coe_nat_injective⟩⟩

Premises used: Nat.Primes.coe_nat_injective, Countable.mk, Exists.intro, Coe.coe
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
⊢ n.primeFactorsList.toFinset = n.primeFactors

Tactic:
rfl

Premises used: Nat.primeFactors, rfl
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
simp_rw : p ∈ n.primeFactorsList.toFinset ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
simp_rw₁ : p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']

Premises used: List.mem_toFinset, Nat.toFinset_factors, Nat.mem_primeFactorsList'
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
hn : n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n

Tactic:
simp [hn]