case intro
b c : ℕ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
a b : ℕ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b
rcases h with ⟨c, rfl⟩
no goals
case intro
b c : ℕ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
simp only [mul_comm b, Nat.mul_div_assoc c (dvd_refl b), Nat.cast_mul, mul_div_assoc,
  coe_nat_div_self]