case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
⊢ b ∣ c / a
rcases eq_or_ne a 0 with (rfl | ha)
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
rcases h with ⟨d, rfl⟩
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a
refine' ⟨d, _⟩
no goals
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d
rw [mul_assoc, mul_div_cancel_left _ ha]
no goals
case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0
simp only [div_zero, dvd_zero]