n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ minFac n
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3
refine ⟨by norm_num, by norm_num, ?_⟩
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ minFac n
refine (le_minFac'.mpr λ p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2

case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p
rcases hp.eq_or_lt with rfl|h
no goals
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3
norm_num
no goals
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1
norm_num
no goals
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2
simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2
no goals
case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p
exact h