case zero
m✝ n✝ m n : ℕ
h✝ : m ≤ n
h : m ≤ zero
⊢ m ! ∣ zero !

case succ
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
⊢ m ! ∣ (succ n)!
m✝ n✝ m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !
induction' n with n IH
case succ.inl
m n✝¹ n✝ n : ℕ
h✝ : succ n ≤ n✝
IH : succ n ≤ n → (succ n)! ∣ n !
h : succ n ≤ succ n
⊢ (succ n)! ∣ (succ n)!

case succ.inr
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
hl : m < succ n
⊢ m ! ∣ (succ n)!
case succ
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
⊢ m ! ∣ (succ n)!
obtain rfl | hl := h.eq_or_lt
no goals
case succ.inr
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
hl : m < succ n
⊢ m ! ∣ (succ n)!
exact (IH (le_of_lt_succ hl)).mul_left _
no goals
case zero
m✝ n✝ m n : ℕ
h✝ : m ≤ n
h : m ≤ zero
⊢ m ! ∣ zero !
simp [Nat.eq_zero_of_le_zero h]
no goals
case succ.inl
m n✝¹ n✝ n : ℕ
h✝ : succ n ≤ n✝
IH : succ n ≤ n → (succ n)! ∣ n !
h : succ n ≤ succ n
⊢ (succ n)! ∣ (succ n)!
simp