case mp
n : ℕ
⊢ minFac n = 2 → 2 ∣ n

case mpr
n : ℕ
⊢ 2 ∣ n → minFac n = 2
n : ℕ
⊢ minFac n = 2 ↔ 2 ∣ n
constructor
case mp
n : ℕ
h : minFac n = 2
⊢ 2 ∣ n
case mp
n : ℕ
⊢ minFac n = 2 → 2 ∣ n
intro h
case mp
n : ℕ
h : minFac n = 2
⊢ minFac n ∣ n
case mp
n : ℕ
h : minFac n = 2
⊢ 2 ∣ n
rw [←h]
no goals
case mp
n : ℕ
h : minFac n = 2
⊢ minFac n ∣ n
exact minFac_dvd n
case mpr
n : ℕ
h : 2 ∣ n
⊢ minFac n = 2
case mpr
n : ℕ
⊢ 2 ∣ n → minFac n = 2
intro h
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
⊢ minFac n = 2
case mpr
n : ℕ
h : 2 ∣ n
⊢ minFac n = 2
have ub := minFac_le_of_dvd (le_refl 2) h
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
⊢ minFac n = 2
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
⊢ minFac n = 2
have lb := minFac_pos n
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
⊢ False
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
⊢ minFac n = 2
refine ub.eq_or_lt.resolve_right fun h' => ?_
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : succ 0 = minFac n
⊢ False
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
⊢ False
have := le_antisymm (Nat.succ_le_of_lt lb) (lt_succ_iff.mp h')
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : n = 1
⊢ False
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : succ 0 = minFac n
⊢ False
rw [eq_comm, Nat.minFac_eq_one_iff] at this
case mpr
h : 2 ∣ 1
ub : minFac 1 ≤ 2
lb : 0 < minFac 1
h' : minFac 1 < 2
⊢ False
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : n = 1
⊢ False
subst this
no goals
case mpr
h : 2 ∣ 1
ub : minFac 1 ≤ 2
lb : 0 < minFac 1
h' : minFac 1 < 2
⊢ False
exact not_lt_of_le (le_of_dvd zero_lt_one h) one_lt_two