awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e : p = m * k
h_1 : mdvd = ⋯
hm : m ≤ p.sqrt
⊢ False

Tactic:
a m m2 hm mdvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e : p = m * k
h_1 : mdvd = ⋯
hm : m ≤ p.sqrt
⊢ False

Tactic:
exact a m m2 hm mdvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e : p = m * k
h_1 : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ p = k * m

Tactic:
rw [mul_comm] at e

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e : p = m * k
h_1 : mdvd = ⋯
hk : k ≤ p.sqrt
e₁ : p = k * m
⊢ mdvd = ⋯

Tactic:
rw [mul_comm] at e

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h_1 mdvd : m ∣ p
k : ℕ
e : p = m * k
h_2 : mdvd = ⋯
hk : k ≤ p.sqrt
e₁ : p = k * m
h : mdvd = ⋯
⊢ k ≤ p.sqrt

Tactic:
rw [mul_comm] at e

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e_1 : p = m * k
e : p = k * m
h_1 : mdvd = ⋯
hk : k ≤ p.sqrt
rwa : m < k * m
rwa₁ rwa₂ rwa₃ rwa₄ : m < p
⊢ 1 * m < k * m

Tactic:
rwa [one_mul, ← e]

Premises used: one_mul
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
h mdvd : m ∣ p
k : ℕ
e_1 : p = m * k
e : p = k * m
h_1 : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False

Tactic:
exact a k (Nat.lt_of_mul_lt_mul_right (a := m) (by rwa [one_mul, ← e])) hk ⟨m, e⟩

Premises used: Nat.lt_of_mul_lt_mul_right, Exists.intro
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
push : Prime p ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p
⊢ Prime p ↔ 2 ≤ p ∧ ¬∃ (m : ℕ), ∃ (n : ℕ), m < p ∧ n < p ∧ m * n = p

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
simp_rw :
  (2 ≤ p ∧ ∀ (m : ℕ), m < p → ∀ (x : ℕ), p = m * x → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p

Tactic:
simp_rw [prime_def_lt, dvd_def, exists_imp]

Premises used: dvd_def, Nat.prime_def_lt, exists_imp
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
⊢ (2 ≤ p ∧ ∀ (m : ℕ), m < p → ∀ (x : ℕ), p = m * x → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p

Tactic:
and_congr_right fun hp ↦ forall_congr' fun m ↦ (forall_congr' fun h ↦ ?_).trans forall_comm

Premises used: forall_comm, and_congr_right, forall_congr', Iff.trans
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
refine : ∀ (hp : 2 ≤ p) (m : ℕ) (h : m < p), (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (_ : b < p), m * b ≠ p
⊢ (2 ≤ p ∧ ∀ (m : ℕ), m < p → ∀ (x : ℕ), p = m * x → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p

Tactic:
refine and_congr_right fun hp ↦ forall_congr' fun m ↦ (forall_congr' fun h ↦ ?_).trans forall_comm

Premises used: forall_comm, and_congr_right, forall_congr', Iff.trans
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
simp_rw : (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (b_1 : p = m * b), p ≤ b
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (_ : b < p), m * b ≠ p

Tactic:
simp_rw [Ne, forall_comm (β := _ = _), eq_comm, imp_false, not_lt]

Premises used: imp_false, forall_comm, Ne, eq_comm, not_lt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
⊢ m = 1 → p ≤ n

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
refine : ∀ (n : ℕ) (hp : p = m * n) (hpn : p ≤ n), m = 1
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (b_1 : p = m * b), p ≤ b

Tactic:
refine forall₂_congr fun n hp ↦ ⟨by simp_all, fun hpn ↦ ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
⊢ p ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
⊢ m ≠ 0 ∧ n ≠ 0

Tactic:
have := mul_ne_zero_iff.mp (hp ▸ show p ≠ 0 by lia)
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
this : m ≠ 0 ∧ n ≠ 0
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
this : m ≠ 0 ∧ n ≠ 0
⊢ 0 < m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
this : m ≠ 0 ∧ n ≠ 0
⊢ m = 1

Tactic:
exact (Nat.mul_eq_right (by lia)).mp
    (hp.symm.trans (hpn.antisymm (hp ▸ Nat.le_mul_of_pos_left _ (by lia))))

Premises used: LE.le.antisymm, Eq.rec, Nat.mul_eq_right, Iff.mp, Nat.le_mul_of_pos_left, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
⊢ Prime n

Tactic:
prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩

Premises used: Iff.mpr, And.intro, Nat.prime_def_lt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
refine : ∀ (m : ℕ) (mlt : m < n) (mdvd : m ∣ n), m = 1
⊢ Prime n

Tactic:
refine prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩

Premises used: Iff.mpr, And.intro, Nat.prime_def_lt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ n = 0

Tactic:
rw [zero_dvd_iff] at mdvd

Premises used: zero_dvd_iff
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : n = 0
⊢ False

Tactic:
mlt.ne' mdvd

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : n = 0
⊢ False

Tactic:
exact mlt.ne' mdvd

Premises used: LT.lt.ne'
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m ≠ 0

Tactic:
have hm : m ≠ 0 := by
    rintro rfl
    rw [zero_dvd_iff] at mdvd
    exact mlt.ne' mdvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1

Tactic:
(h m mlt hm).symm.eq_one_of_dvd mdvd

Premises used: Nat.Coprime.symm, Nat.Coprime.eq_one_of_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1

Tactic:
exact (h m mlt hm).symm.eq_one_of_dvd mdvd

Premises used: Nat.Coprime.symm, Nat.Coprime.eq_one_of_dvd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 3

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 5

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 7

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ Prime 11

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p m : ℕ
pp : Prime p
⊢ m ∣ p ↔ m = 1 ∨ m = p

Tactic:
⟨fun d => pp.eq_one_or_self_of_dvd m d, fun h =>
    h.elim (fun e => e.symm ▸ one_dvd _) fun e => e.symm ▸ dvd_rfl⟩

Premises used: Eq.rec, Nat.Prime.eq_one_or_self_of_dvd, one_dvd, Iff.intro, dvd_rfl, Or.elim, Eq.symm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p m : ℕ
pp : Prime p
H : 2 ≤ m
⊢ m ∣ p ↔ m = p

Tactic:
(dvd_prime pp).trans <| or_iff_right_of_imp <| Not.elim <| ne_of_gt H

Premises used: Nat.dvd_prime, Not.elim, Iff.trans, or_iff_right_of_imp, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p q : ℕ
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q

Tactic:
dvd_prime_two_le qp (Prime.two_le pp)

Premises used: Nat.dvd_prime_two_le, Nat.Prime.two_le
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
p : ℕ
pp : Prime p
⊢ ¬p ∣ 1

Tactic:
Irreducible.not_dvd_one pp

Premises used: Irreducible.not_dvd_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n k : ℕ
h : ¬n < k * k
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n a : ℕ
k : ℕ := a
h : ¬n < k * k
h_1 : ¬k ∣ n
simp_wf : n.sqrt - a < n.sqrt + 2 - a
⊢ n.sqrt + 2 - (a + 2) < n.sqrt + 2 - a

Tactic:
simp_wf
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n a : ℕ
k : ℕ := a
h : ¬n < k * k
h_1 : ¬k ∣ n
apply : ¬n < k * k
⊢ n.sqrt - a < n.sqrt + 2 - a

Tactic:
apply minFac_lemma n k

Premises used: Nat.minFac_lemma
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n a : ℕ
k : ℕ := a
h : ¬n < k * k
h_1 : ¬k ∣ n
⊢ ¬n < k * k

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n a : ℕ
k : ℕ := a
h : ¬n < k * k
h_1 : ¬k ∣ n
decreasing_by decreasing_by₁ : n.sqrt - a < n.sqrt + 2 - a
decreasing_by₂ decreasing_by₃ : ¬n < k * k
⊢ n.sqrt + 2 - (a + 2) < n.sqrt + 2 - a

Tactic:
decreasing_by simp_wf; apply minFac_lemma n k; assumption

Premises used: Nat.minFac_lemma
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ minFac 0 = 2

Tactic:
rfl

Premises used: Nat.minFac, rfl, ite
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ minFac 1 = 1

Tactic:
simp [minFac, minFacAux]

Premises used: Nat.minFac, Nat.minFacAux
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ minFac 2 = 2

Tactic:
simp [minFac]

Premises used: Nat.minFac
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
⊢ n.minFac = if 2 ∣ n then 2 else n.minFacAux 3

Tactic:
rfl

Premises used: Nat.minFac, rfl
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
rw : n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
⊢ n.minFacProp (n.minFacAux x)

Tactic:
rw [minFacAux]

Premises used: Nat.minFacAux
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
pos : ∀ (h : n < k * k), n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
neg : ∀ (h : ¬n < k * k), n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))

Tactic:
by_cases h : n < k * k
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : n < k * k
⊢ Prime n

Tactic:
have pp : Prime n :=
        prime_def_le_sqrt.2
          ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : n < k * k
pp : Prime n
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))

Tactic:
simpa only [k, h] using
        ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
subst :
  let k := 2 * i + 3;
  ∀ (a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m) (h : ¬n < k * k), 2 ≤ k
⊢ 2 ≤ k

Tactic:
subst e
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
i : ℕ
k : ℕ := 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < k * k
⊢ 2 ≤ k

Tactic:
apply Nat.le_add_left

Premises used: Nat.le_add_left
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
⊢ 2 ≤ k

Tactic:
have k2 : 2 ≤ k := by
      subst e
      apply Nat.le_add_left
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
neg : n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))

Tactic:
simp only [k, h, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
pos : ∀ (dk : k ∣ n), n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
neg : ∀ (dk : ¬k ∣ n), n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
⊢ n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))

Tactic:
by_cases dk : k ∣ n
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
pos : n.minFacProp x
⊢ n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))

Tactic:
simp only [k, dk, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
neg : n.minFacProp (n.minFacAux (x + 2))
⊢ n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))

Tactic:
simp only [k, dk, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp x

Tactic:
⟨k2, dk, a⟩

Premises used: _private.0.Nat.minFacProp, And.intro
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp x

Tactic:
exact ⟨k2, dk, a⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3

Tactic:
simp [k, e, Nat.left_distrib, add_right_comm]

Premises used: add_right_comm, Nat.left_distrib
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
neg : ∀ (this : n.sqrt - k < n.sqrt + 2 - k) (m : ℕ) (m2 : 2 ≤ m) (d : m ∣ n), k + 2 ≤ m
⊢ n.minFacProp (n.minFacAux (x + 2))

Tactic:
refine
        have := minFac_lemma n k h
        minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [k, e, Nat.left_distrib, add_right_comm])
          fun m m2 d => ?_

Premises used: Nat.minFac_lemma, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
neg : ∀ (m2 : 2 ≤ x) (d : x ∣ n), k + 2 ≤ x
neg₁ : ∀ (ml : x < m), k + 2 ≤ m
⊢ k + 2 ≤ m

Tactic:
rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml

Premises used: Nat.eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m2 : 2 ≤ x
d : x ∣ n
⊢ k + 2 ≤ x

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x < m
neg : ¬x.succ = m
⊢ k + 2 ≤ m

Tactic:
apply (Nat.eq_or_lt_of_le ml).resolve_left

Premises used: Or.resolve_left, Nat.eq_or_lt_of_le
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x < m
me : x.succ = m
⊢ (2 * i + 3).succ ∣ n

Tactic:
rw [← me, e] at d
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x < m
me : x.succ = m
d₁ : (2 * i + 3).succ ∣ n
⊢ x < m

Tactic:
rw [← me, e] at d
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x < m
me : x.succ = m
d₁ : (2 * i + 3).succ ∣ n
ml₁ : x < m
⊢ x.succ = m

Tactic:
rw [← me, e] at d
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x < m
me : x.succ = m
⊢ 2 * (i + 2) ∣ n

Tactic:
have d' : 2 * (i + 2) ∣ n := d
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x < m
me : x.succ = m
d' : 2 * (i + 2) ∣ n
⊢ x ≤ 2

Tactic:
have := a _ le_rfl (dvd_of_mul_right_dvd d')
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this_1 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x < m
me : x.succ = m
d' : 2 * (i + 2) ∣ n
this : x ≤ 2
⊢ 2 * i + 3 ≤ 2

Tactic:
rw [e] at this
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this_1 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x < m
me : x.succ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this_1 : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x < m
me : x.succ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False

Tactic:
exact absurd this (by contradiction)

Premises used: absurd
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
pos : ∀ (n0 : n = 0), n.minFacProp n.minFac
neg : ∀ (n0 : ¬n = 0), n.minFacProp n.minFac
⊢ n.minFacProp n.minFac

Tactic:
by_cases n0 : n = 0
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ n.minFacProp n.minFac

Tactic:
simp [n0, minFacProp]

Premises used: _private.0.Nat.minFacProp
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
revert : ∀ (n1 : n ≠ 1) (n0 : ¬n = 0), 2 ≤ n
⊢ 2 ≤ n

Tactic:
revert n0 n1
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
zero : ∀ (n1 : Ne (α := ℕ) 0 1) (n0 : ¬Eq (α := ℕ) 0 0), LE.le (α := ℕ) 2 0
succ : ∀ (n1 : HAdd.hAdd (α := ℕ) 0 1 ≠ 1) (n0 : ¬HAdd.hAdd (α := ℕ) 0 1 = 0), 2 ≤ HAdd.hAdd (α := ℕ) 0 1
succ₁ : ∀ (n : ℕ) (n1 : n + 1 + 1 ≠ 1) (n0 : ¬n + 1 + 1 = 0), 2 ≤ n + 1 + 1
⊢ ∀ (n1 : n ≠ 1) (n0 : ¬n = 0), 2 ≤ n

Tactic:
rcases n with (_ | _ | _)
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ ∀ (n1 : Ne (α := ℕ) 0 1) (n0 : ¬Eq (α := ℕ) 0 0), LE.le (α := ℕ) 2 0

Tactic:
simp [succ_le_succ]

Premises used: Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
⊢ ∀ (n1 : HAdd.hAdd (α := ℕ) 0 1 ≠ 1) (n0 : ¬HAdd.hAdd (α := ℕ) 0 1 = 0), 2 ≤ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp [succ_le_succ]

Premises used: Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
⊢ ∀ (n1 : n + 1 + 1 ≠ 1) (n0 : ¬n + 1 + 1 = 0), 2 ≤ n + 1 + 1

Tactic:
simp [succ_le_succ]

Premises used: Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ 2 ≤ n

Tactic:
have n2 : 2 ≤ n := by
    revert n0 n1
    rcases n with (_ | _ | _) <;> simp [succ_le_succ]
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
pos : ∀ (d2 : 2 ∣ n), n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
neg : ∀ (d2 : ¬2 ∣ n), n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

Tactic:
by_cases d2 : 2 ∣ n
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
pos : n.minFacProp 2
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

Tactic:
simp only [d2, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
neg : n.minFacProp (n.minFacAux 3)
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

Tactic:
simp only [d2, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp 2

Tactic:
⟨le_rfl, d2, fun k k2 _ => k2⟩

Premises used: le_rfl, _private.0.Nat.minFacProp, And.intro
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp 2

Tactic:
exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)

Tactic:
minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)

Premises used: Nat.minFacAux_has_prop, mt, Or.resolve_left, Nat.eq_or_lt_of_le, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
neg : ∀ (m : ℕ) (m2 : 2 ≤ m) (d : m ∣ n), 2 = m → 2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)

Tactic:
refine
      minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)

Premises used: Nat.minFacAux_has_prop, mt, Or.resolve_left, Nat.eq_or_lt_of_le, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n

Tactic:
fun e => e.symm ▸ d

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n

Tactic:
exact fun e => e.symm ▸ d
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
n1 : n = 1
⊢ n.minFac ∣ n

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

Tactic:
let ⟨f2, fd, a⟩ := minFac_has_prop n1
  prime_def_lt'.2 ⟨f2, fun m m2 l d => not_le_of_gt l (a m m2 (d.trans fd))⟩

Premises used: Iff.mpr, Nat.Prime, Nat.prime_def_lt', Nat.minFac, _private.0.Nat.minFac_prime.match_1, Nat.minFac_has_prop, And.intro, not_le_of_gt, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
⊢ Prime n.minFac ↔ n ≠ 1

Tactic:
⟨?_, minFac_prime⟩

Premises used: Iff.intro, Nat.minFac_prime
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
refine : Prime n.minFac → n ≠ 1
⊢ Prime n.minFac ↔ n ≠ 1

Tactic:
refine ⟨?_, minFac_prime⟩
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
h : Prime (minFac 1)
⊢ False

Tactic:
simp only [minFac_one, not_prime_one] at h

Premises used: Nat.not_prime_one, Nat.minFac_one
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : ∀ {m : ℕ} (n1 : n = 1), 2 ≤ m → m ∣ n → n.minFac ≤ m
neg : ∀ {m : ℕ} (n1 : ¬n = 1), 2 ≤ m → m ∣ n → n.minFac ≤ m
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m

Tactic:
by_cases n1 : n = 1
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n m : ℕ
n1 : n = 1
m2 : 2 ≤ m
h : m ∣ n
⊢ minFac 1 ≤ 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n m : ℕ
n1 : n = 1
⊢ 2 ≤ m → m ∣ n → n.minFac ≤ m

Tactic:
exact fun m2 _ => n1.symm ▸ le_trans (by simp) m2
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n m : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m → m ∣ n → n.minFac ≤ m

Tactic:
apply (minFac_has_prop n1).2.2

Premises used: And.right, Nat.minFac_has_prop
-- Module: Mathlib.Data.Nat.Prime.Defs
Goal:
n : ℕ
pos : ∀ (n1 : n = 1), 0 < n.minFac
neg : ∀ (n1 : ¬n = 1), 0 < n.minFac
⊢ 0 < n.minFac

Tactic:
by_cases n1 : n = 1