i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

case this
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
i j : ℕ
⊢ i ! * j ! ∣ (i + j)!
suffices : i ! * (i + j - i) ! ∣ (i + j)!
case this
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

case this
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
. rwa [add_tsub_cancel_left i j] at this
no goals
case this
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)
no goals
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!
rwa [add_tsub_cancel_left i j] at this