awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ False
have e₁ : p = k * m
Tactic: rw [mul_comm] at e
Cleared hypotheses: h_1, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ 1 * m < k * m
have rwa : m < k * m
Tactic: rwa [one_mul, ← e]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ¬∃ (m : ℕ), ∃ (n : ℕ), m < p ∧ n < p ∧ m * n = p
have push : Prime p ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p
Tactic: push Not
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p
have simp_rw : (2 ≤ p ∧ ∀ (m : ℕ), m < p → ∀ (x : ℕ), p = m * x → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p
Tactic: simp_rw [prime_def_lt, dvd_def, exists_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
⊢ (2 ≤ p ∧ ∀ (m : ℕ), m < p → ∀ (x : ℕ), p = m * x → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ) (_ : m < p) (_ : n < p), m * n ≠ p
have refine : ∀ (hp : 2 ≤ p) (m : ℕ) (h : m < p), (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (_ : b < p), m * b ≠ p
Tactic: refine and_congr_right fun hp ↦ forall_congr' fun m ↦ (forall_congr' fun h ↦ ?_).trans forall_comm
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (_ : b < p), m * b ≠ p
have simp_rw : (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (b_1 : p = m * b), p ≤ b
Tactic: simp_rw [Ne, forall_comm (β := _ = _), eq_comm, imp_false, not_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ) (b_1 : p = m * b), p ≤ b
have refine : ∀ (n : ℕ) (hp : p = m * n) (hpn : p ≤ n), m = 1
Tactic: refine forall₂_congr fun n hp ↦ ⟨by simp_all, fun hpn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
p : ℕ
hp_1 : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
⊢ m = 1
have this : m ≠ 0 ∧ n ≠ 0
Tactic: have := mul_ne_zero_iff.mp (hp ▸ show p ≠ 0 by lia)
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
⊢ Prime n
have refine : ∀ (m : ℕ) (mlt : m < n) (mdvd : m ∣ n), m = 1
Tactic: refine prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False
have mdvd₁ : n = 0
Tactic: rw [zero_dvd_iff] at mdvd
Cleared hypotheses: mdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1
have hm : m ≠ 0
Tactic: have hm : m ≠ 0 := by
    rintro rfl
    rw [zero_dvd_iff] at mdvd
    exact mlt.ne' mdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n a : ℕ
k : ℕ := a
h : ¬n < k * k
h_1 : ¬k ∣ n
⊢ n.sqrt + 2 - (a + 2) < n.sqrt + 2 - a
have simp_wf : n.sqrt - a < n.sqrt + 2 - a
Tactic: simp_wf
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n a : ℕ
k : ℕ := a
h : ¬n < k * k
h_1 : ¬k ∣ n
⊢ n.sqrt + 2 - (a + 2) < n.sqrt + 2 - a
have decreasing_by : n.sqrt - a < n.sqrt + 2 - a
Tactic: decreasing_by simp_wf; apply minFac_lemma n k; assumption
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
⊢ n.minFacProp (n.minFacAux x)
have rw : n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
Tactic: rw [minFacAux]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n2 : 2 ≤ n
x : ℕ
k : ℕ := x
i : ℕ
e : x = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x ≤ m
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
have pos : ∀ (h : n < k * k), 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
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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))
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
have neg : ∀ (h : ¬n < k * k), 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
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
have pp : 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)⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
have subst : let k := 2 * i + 3;
∀ (a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m) (h : ¬n < k * k), 2 ≤ k
Tactic: subst e
Cleared hypotheses: x, k, e, a, h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
have k2 : 2 ≤ k
Tactic: have k2 : 2 ≤ k := by
      subst e
      apply Nat.le_add_left
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ n.minFacProp (if n < x * x then n else if x ∣ n then x else n.minFacAux (x + 2))
have neg : n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
Tactic: simp only [k, h, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
have pos : ∀ (dk : k ∣ n), n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
Tactic: by_cases dk : k ∣ n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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))
⊢ n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
have neg : ∀ (dk : ¬k ∣ n), n.minFacProp (if x ∣ n then x else n.minFacAux (x + 2))
Tactic: by_cases dk : k ∣ n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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 (if x ∣ n then x else n.minFacAux (x + 2))
have pos : n.minFacProp x
Tactic: simp only [k, dk, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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 (if x ∣ n then x else n.minFacAux (x + 2))
have neg : n.minFacProp (n.minFacAux (x + 2))
Tactic: simp only [k, dk, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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 (n.minFacAux (x + 2))
have neg : ∀ (this : n.sqrt - k < n.sqrt + 2 - k) (m : ℕ) (m2 : 2 ≤ m) (d : m ∣ n), k + 2 ≤ m
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 => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ k + 2 ≤ m
have neg : ∀ (m2 : 2 ≤ x) (d : x ∣ n), k + 2 ≤ x
Tactic: rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml
Cleared hypotheses: m, m2, d
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ k + 2 ≤ m
have neg₁ : ∀ (ml : x < m), k + 2 ≤ m
Tactic: rcases Nat.eq_or_lt_of_le (a m m2 d) with rfl | ml
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ k + 2 ≤ m
have neg : ¬x.succ = m
Tactic: apply (Nat.eq_or_lt_of_le ml).resolve_left
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ False
have d₁ : (2 * i + 3).succ ∣ n
Tactic: rw [← me, e] at d
Cleared hypotheses: d, ml, me
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ False
have d' : 2 * (i + 2) ∣ n
Tactic: have d' : 2 * (i + 2) ∣ n := d
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ False
have this₁ : x ≤ 2
Tactic: have := a _ le_rfl (dvd_of_mul_right_dvd d')
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
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
⊢ False
have this₁ : 2 * i + 3 ≤ 2
Tactic: rw [e] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
⊢ n.minFacProp n.minFac
have pos : ∀ (n0 : n = 0), n.minFacProp n.minFac
Tactic: by_cases n0 : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
pos : ∀ (n0 : n = 0), n.minFacProp n.minFac
⊢ n.minFacProp n.minFac
have neg : ∀ (n0 : ¬n = 0), n.minFacProp n.minFac
Tactic: by_cases n0 : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ 2 ≤ n
have revert : ∀ (n1 : n ≠ 1) (n0 : ¬n = 0), 2 ≤ n
Tactic: revert n0 n1
Cleared hypotheses: n1, n0
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
⊢ ∀ (n1 : n ≠ 1) (n0 : ¬n = 0), 2 ≤ n
have zero : ∀ (n1 : Ne (α := ℕ) 0 1) (n0 : ¬Eq (α := ℕ) 0 0), LE.le (α := ℕ) 2 0
Tactic: rcases n with (_ | _ | _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
zero : ∀ (n1 : Ne (α := ℕ) 0 1) (n0 : ¬Eq (α := ℕ) 0 0), LE.le (α := ℕ) 2 0
⊢ ∀ (n1 : n ≠ 1) (n0 : ¬n = 0), 2 ≤ n
have succ : ∀ (n1 : HAdd.hAdd (α := ℕ) 0 1 ≠ 1) (n0 : ¬HAdd.hAdd (α := ℕ) 0 1 = 0), 2 ≤ HAdd.hAdd (α := ℕ) 0 1
Tactic: rcases n with (_ | _ | _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ ∀ (n1 : n ≠ 1) (n0 : ¬n = 0), 2 ≤ n
have succ₁ : ∀ (n : ℕ) (n1 : n + 1 + 1 ≠ 1) (n0 : ¬n + 1 + 1 = 0), 2 ≤ n + 1 + 1
Tactic: rcases n with (_ | _ | _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ n.minFacProp n.minFac
have n2 : 2 ≤ n
Tactic: have n2 : 2 ≤ n := by
    revert n0 n1
    rcases n with (_ | _ | _) <;> simp [succ_le_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
have pos : ∀ (d2 : 2 ∣ n), n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
Tactic: by_cases d2 : 2 ∣ n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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)
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
have neg : ∀ (d2 : ¬2 ∣ n), n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
Tactic: by_cases d2 : 2 ∣ n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
have pos : n.minFacProp 2
Tactic: simp only [d2, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)
have neg : n.minFacProp (n.minFacAux 3)
Tactic: simp only [d2, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)
have neg : ∀ (m : ℕ) (m2 : 2 ≤ m) (d : m ∣ n), 2 = m → 2 ∣ n
Tactic: refine
      minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
⊢ Prime n.minFac ↔ n ≠ 1
have refine : Prime n.minFac → n ≠ 1
Tactic: refine ⟨?_, minFac_prime⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m
have pos : ∀ {m : ℕ} (n1 : n = 1), 2 ≤ m → m ∣ n → n.minFac ≤ m
Tactic: by_cases n1 : n = 1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : ∀ {m : ℕ} (n1 : n = 1), 2 ≤ m → m ∣ n → n.minFac ≤ m
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m
have neg : ∀ {m : ℕ} (n1 : ¬n = 1), 2 ≤ m → m ∣ n → n.minFac ≤ m
Tactic: by_cases n1 : n = 1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
⊢ 0 < n.minFac
have pos : ∀ (n1 : n = 1), 0 < n.minFac
Tactic: by_cases n1 : n = 1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : ∀ (n1 : n = 1), 0 < n.minFac
⊢ 0 < n.minFac
have neg : ∀ (n1 : ¬n = 1), 0 < n.minFac
Tactic: by_cases n1 : n = 1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < n
have rw : ¬LT.lt (α := ℕ) 0 0
Tactic: rw [h0, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac * 1
⊢ n.minFac ≤ n / n.minFac
have h1₁ : n = n.minFac
Tactic: rw [mul_one] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
have np₁ : 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
Cleared hypotheses: np, h1
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
have rw : minFac 1 ≤ 1 / minFac 1
Tactic: rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = n.minFac
rw : minFac 1 ≤ 1 / minFac 1
⊢ n.minFac ≤ n / n.minFac
have rw₁ : 1 ≤ 1 / 1
Tactic: rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
a : n
| n / n.minFac
have a₁ : n.minFac
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n
have a : n.minFac * (x + 2)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
| n / n.minFac
have a : n.minFac * (x + 2)
Tactic: congr
      rw [hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
a : n.minFac * (x + 2)
| n / n.minFac
have a₁ : n.minFac
Tactic: congr
      rw [hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n / n.minFac
have conv_rhs : n.minFac ≤ n.minFac * (x + 2) / n.minFac
Tactic: conv_rhs =>
      congr
      rw [hx]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac
have rw : n.minFac ≤ x + 2
Tactic: rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
⊢ n.minFac = 1 ↔ n = 1
have mp : n.minFac = 1 → n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
mp : n.minFac = 1 → n = 1
⊢ n.minFac = 1 ↔ n = 1
have mpr : n = 1 → n.minFac = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
h : n.minFac = 1
⊢ n = 1
have mp : ∀ (hn : ¬n = 1), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
⊢ False
have this : Prime n.minFac
Tactic: have := minFac_prime hn
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime n.minFac
⊢ False
have this₁ : Prime 1
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
⊢ n.minFac = 2 ↔ 2 ∣ n
have mp : n.minFac = 2 → 2 ∣ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
mp : n.minFac = 2 → 2 ∣ n
⊢ n.minFac = 2 ↔ 2 ∣ n
have mpr : 2 ∣ n → n.minFac = 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
h : n.minFac = 2
⊢ 2 ∣ n
have mp : n.minFac ∣ n
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
h : 2 ∣ n
⊢ n.minFac = 2
have ub : n.minFac ≤ 2
Tactic: have ub := minFac_le_of_dvd (le_refl 2) h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (hypothesis)
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
⊢ n.minFac = 2
have lb : 0 < n.minFac
Tactic: have lb := minFac_pos n
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
⊢ n.minFac = 2
have mpr : ∀ (h' : n.minFac < 2), False
Tactic: refine ub.eq_or_lt.resolve_right fun h' => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
⊢ False
have mpr : n.minFac = 1
Tactic: suffices n.minFac = 1 by simp_all
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
k : ℕ
⊢ k + 2 ≠ 1
have h : 1 < k + 2
Tactic: apply Nat.ne_of_gt
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
k : ℕ
⊢ 1 < k + 2
have h : 0 < k + 1
Tactic: apply Nat.succ_lt_succ
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ m.gcd n = 1
have by_contra : ∀ (g2 : ¬m.gcd n = 1), False
Tactic: by_contra g2
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
Goal:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
⊢ False
have obtain : ∀ (p : ℕ) (hp : Prime p) (hpdvd : p ∣ m.gcd n), False
Tactic: obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ False
have a : p ∣ m
Tactic: apply H p hp
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ False
have a₁ : p ∣ n
Tactic: apply H p hp
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ p ∣ m
have a : m.gcd n ∣ m
Tactic: apply dvd_trans hpdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Defs (goal)
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
⊢ p ∣ n
have a : m.gcd n ∣ n
Tactic: apply dvd_trans hpdvd
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1
have rw : p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1
Tactic: rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
n p : ℕ
hp : Prime p
h_1 : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1
have rw : n + 1 ∣ n + 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
m n : ℕ
hm : m ≠ 1
⊢ m.Coprime n ! ↔ n < m.minFac
have rw : m.minFac ≤ n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
Tactic: rw [← not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
have mp : m.minFac ≤ n → ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
m n : ℕ
hm : m ≠ 1
mp : m.minFac ≤ n → ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
⊢ m.minFac ≤ n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !
have mpr : (∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
p n : ℕ
hp : Prime p
hn : n < p
⊢ p.Coprime n !
have rwa : ¬p ∣ n !
Tactic: rwa [hp.coprime_iff_not_dvd, hp.dvd_factorial, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
p n : ℕ
hp : Prime p
hn : n < p
rwa : ¬p ∣ n !
⊢ p.Coprime n !
have rwa₁ : ¬p ≤ n
Tactic: rwa [hp.coprime_iff_not_dvd, hp.dvd_factorial, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ p.Coprime (n.descFactorial k)
have rw : p.Coprime (n ! / (n - k)!)
Tactic: rw [Nat.descFactorial_eq_div hk]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Factorial (goal)
Goal:
p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ p.Coprime (n ! / (n - k)!)
have refine : (n - k)! ∣ n !
Tactic: refine (hp.coprime_factorial_of_lt hn).coprime_div_right ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Infinite (goal)
Goal:
⊢ ¬BddAbove (α := ℕ) {p : ℕ | Prime p}
have rw : ∀ (x : ℕ), ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ x < y
Tactic: rw [not_bddAbove_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Infinite (goal)
Goal:
n : ℕ
⊢ ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ n < y
have obtain : ∀ (p : ℕ) (hi : n.succ ≤ p) (hp : Prime p), ∃ (y : ℕ), Membership.mem (γ := Set ℕ) {p : ℕ | Prime p} y ∧ n < y
Tactic: obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ