rcases mul_eq_zero.mp H with rfl | rfl
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.inl.inl
b c₁ d₁ : ℕ
h' : Coprime 0 b
h : 0 * (b * d₁) = b * (0 * c₁)
H : 0 * b = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ b * d₁ = m * b

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