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