Theorem: dvd_fac (MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
i n : ℕ
ipos : 0 < i
ile : i ≤ n
⊢ i ∣ fac n
Tactic:
induction' n with n ih
State after:
case zero
i : ℕ
ipos : 0 < i
ile : i ≤ 0
⊢ i ∣ fac 0

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

State before:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ fac (n + 1)
Tactic:
rw [fac]
State after:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ (n + 1) * fac n

State before:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ (n + 1) * fac n
Tactic:
rcases Nat.of_le_succ ile with h | h
State after:
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

State before:
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
Tactic:
rw [h]
State after:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ n.succ ∣ (n + 1) * fac n

State before:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = n.succ
⊢ n.succ ∣ (n + 1) * fac n
Tactic:
apply dvd_mul_right
State after:
no goals

State before:
case zero
i : ℕ
ipos : 0 < i
ile : i ≤ 0
⊢ i ∣ fac 0
Tactic:
exact absurd ipos (not_lt_of_ge ile)
State after:
no goals

State before:
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
Tactic:
apply dvd_mul_of_dvd_right (ih h)
State after:
no goals