case inl
m n l : ℕ
hnl : l ∣ n
hmk : 0 ∣ m
⊢ m * n / (0 * l) = m / 0 * (n / l)

case inr
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
hk0 : k > 0
⊢ m * n / (k * l) = m / k * (n / l)
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
⊢ m * n / (k * l) = m / k * (n / l)
rcases k.eq_zero_or_pos with (rfl | hk0)
case inr.inl
m n k : ℕ
hmk : k ∣ m
hk0 : k > 0
hnl : 0 ∣ n
⊢ m * n / (k * 0) = m / k * (n / 0)

case inr.inr
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
hk0 : k > 0
hl0 : l > 0
⊢ m * n / (k * l) = m / k * (n / l)
case inr
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
hk0 : k > 0
⊢ m * n / (k * l) = m / k * (n / l)
rcases l.eq_zero_or_pos with (rfl | hl0)
case inr.inr.intro
n k l : ℕ
hnl : l ∣ n
hk0 : k > 0
hl0 : l > 0
w✝ : ℕ
⊢ k * w✝ * n / (k * l) = k * w✝ / k * (n / l)
case inr.inr
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
hk0 : k > 0
hl0 : l > 0
⊢ m * n / (k * l) = m / k * (n / l)
obtain ⟨_, rfl⟩ := hmk
case inr.inr.intro.intro
k l : ℕ
hk0 : k > 0
hl0 : l > 0
w✝¹ w✝ : ℕ
⊢ k * w✝¹ * (l * w✝) / (k * l) = k * w✝¹ / k * (l * w✝ / l)
case inr.inr.intro
n k l : ℕ
hnl : l ∣ n
hk0 : k > 0
hl0 : l > 0
w✝ : ℕ
⊢ k * w✝ * n / (k * l) = k * w✝ / k * (n / l)
obtain ⟨_, rfl⟩ := hnl
no goals
case inr.inr.intro.intro
k l : ℕ
hk0 : k > 0
hl0 : l > 0
w✝¹ w✝ : ℕ
⊢ k * w✝¹ * (l * w✝) / (k * l) = k * w✝¹ / k * (l * w✝ / l)
rw [mul_mul_mul_comm, Nat.mul_div_cancel_left _ hk0, Nat.mul_div_cancel_left _ hl0,
  Nat.mul_div_cancel_left _ (mul_pos hk0 hl0)]
no goals
case inl
m n l : ℕ
hnl : l ∣ n
hmk : 0 ∣ m
⊢ m * n / (0 * l) = m / 0 * (n / l)
simp
no goals
case inr.inl
m n k : ℕ
hmk : k ∣ m
hk0 : k > 0
hnl : 0 ∣ n
⊢ m * n / (k * 0) = m / k * (n / 0)
simp