no goals
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m
by_cases n1 : n = 1 <;> [exact fun m2 _ => n1.symm ▸ le_trans (by decide) m2;
  apply (minFac_has_prop n1).2.2]
no goals
n m✝ : ℕ
n1 : n = 1
m2 : 2 ≤ m✝
x✝ : m✝ ∣ n
⊢ minFac 1 ≤ 2
decide