case mp
n : ℕ
h : factors n = []
⊢ n = 0 ∨ n = 1

case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ factors n = []
n : ℕ
⊢ factors n = [] ↔ n = 0 ∨ n = 1
constructor <;> intro h
case mp.zero
h : factors zero = []
⊢ zero = 0 ∨ zero = 1

case mp.succ.zero
h : factors (succ zero) = []
⊢ succ zero = 0 ∨ succ zero = 1

case mp.succ.succ
n : ℕ
h : factors (succ (succ n)) = []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
case mp
n : ℕ
h : factors n = []
⊢ n = 0 ∨ n = 1
rcases n with (_ | _ | n)
no goals
case mp.zero
h : factors zero = []
⊢ zero = 0 ∨ zero = 1
exact Or.inl rfl
no goals
case mp.succ.zero
h : factors (succ zero) = []
⊢ succ zero = 0 ∨ succ zero = 1
exact Or.inr rfl
case mp.succ.succ
n : ℕ
h :
  (let m := minFac (n + 2);
    let_fun this := (_ : (n + 2) / minFac (n + 2) < n + 2);
    m :: factors ((n + 2) / m)) =
    []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
case mp.succ.succ
n : ℕ
h : factors (succ (succ n)) = []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
rw [factors] at h
no goals
case mp.succ.succ
n : ℕ
h :
  (let m := minFac (n + 2);
    let_fun this := (_ : (n + 2) / minFac (n + 2) < n + 2);
    m :: factors ((n + 2) / m)) =
    []
⊢ succ (succ n) = 0 ∨ succ (succ n) = 1
injection h
case mpr.inl

⊢ factors 0 = []

case mpr.inr

⊢ factors 1 = []
case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ factors n = []
rcases h with (rfl | rfl)
no goals
case mpr.inl

⊢ factors 0 = []
exact factors_zero
no goals
case mpr.inr

⊢ factors 1 = []
exact factors_one