no goals
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors n → Prime p
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
    intro p h
    let m := minFac (k + 2)
    have : (k + 2) / m < (k + 2) := factors_lemma
    have h₁ : p = m ∨ p ∈ factors ((k + 2) / m) :=
      List.mem_cons.1 (by rwa [factors] at h)
    exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_factors
no goals
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors 0 → Prime p
simp
no goals
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors 1 → Prime p
simp
n k p : ℕ
h : p ∈ factors (k + 2)
⊢ Prime p
n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ factors (k + 2) → Prime p
intro p h
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
⊢ Prime p
n k p : ℕ
h : p ∈ factors (k + 2)
⊢ Prime p
let m := minFac (k + 2)
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ Prime p
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
⊢ Prime p
have : (k + 2) / m < (k + 2) := factors_lemma
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
⊢ Prime p
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ Prime p
have h₁ : p = m ∨ p ∈ factors ((k + 2) / m) :=
  List.mem_cons.1 (by rwa [factors] at h)
no goals
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
⊢ Prime p
exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_factors
no goals
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ p ∈ m :: factors ((k + 2) / m)
rwa [factors] at h
no goals
n k p : ℕ
h : p ∈ factors (k + 2)
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ factors ((k + 2) / m)
h₂ : p = m
⊢ k + 2 ≠ 1
simp