no goals
k n m : Nat
H : k ∣ n
⊢ m * n / k = m * (n / k)
match Nat.eq_zero_or_pos k with
| .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
| .inr hpos =>
  have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
  rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
no goals
k n m : Nat
H : k ∣ n
h0 : k = 0
⊢ m * n / k = m * (n / k)
rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
k n m : Nat
H : k ∣ n
hpos : k > 0
h1 : m * n / k = m * (n / k * k) / k
⊢ m * n / k = m * (n / k)
k n m : Nat
H : k ∣ n
hpos : k > 0
⊢ m * n / k = m * (n / k)
have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
no goals
k n m : Nat
H : k ∣ n
hpos : k > 0
h1 : m * n / k = m * (n / k * k) / k
⊢ m * n / k = m * (n / k)
rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
no goals
k n m : Nat
H : k ∣ n
hpos : k > 0
⊢ m * n / k = m * (n / k * k) / k
rw [Nat.div_mul_cancel H]