case intro
n k l w✝ : ℕ
hm : n * w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n
m n k l : ℕ
h : n ∣ m
hm : m ≠ 0
⊢ m / (m / n) = n
rcases h with ⟨_, rfl⟩
case intro
n k l w✝ : ℕ
hm : n ≠ 0 ∧ w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n
case intro
n k l w✝ : ℕ
hm : n * w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n
rw [mul_ne_zero_iff] at hm
no goals
case intro
n k l w✝ : ℕ
hm : n ≠ 0 ∧ w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n
rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]