-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_chain {n : ℕ} :
    ∀ {a}, (∀ p, Prime p → p ∣ n → a ≤ p) → List.Chain (· ≤ ·) a (primeFactorsList n)

Proof state:
n k : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList

Tactic:
intro a h

Result:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList

Proof state:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.Chain (fun x1 x2 => x1 ≤ x2) a (primeFactorsList 0)

Tactic:
simp

Result:
no goals

Proof state:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList

Tactic:
have : (k + 2) / m < (k + 2) := factors_lemma

Result:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList

Proof state:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.Chain (fun x1 x2 => x1 ≤ x2) a n.primeFactorsList

Tactic:
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 [primeFactorsList]
    refine List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (primeFactorsList_chain ?_)
    exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.Chain (fun x1 x2 => x1 ≤ x2) a (primeFactorsList 1)

Tactic:
simp

Result:
no goals

Proof state:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList

Tactic:
rw [primeFactorsList]

Result:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)

Proof state:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)

Tactic:
refine List.Chain.cons ((le_minFac.2 h).resolve_left (by simp)) (primeFactorsList_chain ?_)

Result:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p

Proof state:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p

Tactic:
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

Result:
no goals

Proof state:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList

Tactic:
let m := minFac (k + 2)

Result:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
⊢ List.Chain (fun x1 x2 => x1 ≤ x2) a (k + 2).primeFactorsList