cases' eq_or_ne (a * b) 0 with H H
case intro.intro
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
case intro.intro.inl
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b = 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b

case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b