obtain ⟨d₁, rfl⟩ := (Coprime.dvd_mul_left h'.symm).mp <| Dvd.intro _ h.symm
case intro
a b d : ℕ
h' : Coprime a b
c₁ : ℕ
h : a * d = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ d = m * b
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