rcases Nat.of_le_succ ile with h | h
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ (n + 1) * fac n
case succ.inl
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i ≤ n
⊢ i ∣ (n + 1) * fac n

case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ i ∣ (n + 1) * fac n