no goals
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors n)
match n with
| 0 => simp
| 1 => simp
| k + 2 =>
    intro a h
    let m := minFac (k + 2)
    have : (k + 2) / m < (k + 2) := factors_lemma
    rw [factors]
    refine' List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (factors_chain _)
    exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
no goals
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors 0)
simp
no goals
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors 1)
simp
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
n k : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
intro a h
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
let m := minFac (k + 2)
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
have : (k + 2) / m < (k + 2) := factors_lemma
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a
    (let m := minFac (k + 2);
    let_fun this := (_ : (k + 2) / minFac (k + 2) < k + 2);
    m :: factors ((k + 2) / m))
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a (factors (k + 2))
rw [factors]
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / minFac (k + 2) → minFac (k + 2) ≤ p
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x x_1 => x ≤ x_1) a
    (let m := minFac (k + 2);
    let_fun this := (_ : (k + 2) / minFac (k + 2) < k + 2);
    m :: factors ((k + 2) / m))
refine' List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (factors_chain _)
no goals
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / minFac (k + 2) → minFac (k + 2) ≤ p
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)
no goals
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1
simp