case inl
a b✝ : ℤ
n : ℕ
b c : ℤ
h : 0 * b ∣ c
⊢ b ∣ c / 0

case inr
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
⊢ b ∣ c / a
rcases eq_or_ne a 0 with (rfl | ha)
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ b ∣ a * b * d / a
case inr
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
rcases h with ⟨d, rfl⟩
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ a * b * d / a = b * d
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ b ∣ a * b * d / a
refine' ⟨d, _⟩
no goals
case inr.intro
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
ha : a ≠ 0
d : ℤ
⊢ a * b * d / a = b * d
rw [mul_assoc, Int.mul_ediv_cancel_left _ ha]
no goals
case inl
a b✝ : ℤ
n : ℕ
b c : ℤ
h : 0 * b ∣ c
⊢ b ∣ c / 0
simp only [Int.ediv_zero, dvd_zero]