m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False
m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n
intro h
case intro
m n b : ℕ
cop : coprime m n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False
m n a b : ℕ
cop : coprime m n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False
obtain ⟨x, rfl⟩ : n ∣ a :=
  cop.symm.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
      ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
case intro
m n b : ℕ
cop : coprime m n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False
obtain ⟨y, rfl⟩ : m ∣ b :=
  cop.dvd_of_dvd_mul_right
    ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
      ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
refine' mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) _)
no goals
case intro.intro
m n : ℕ
cop : coprime m n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n
rw [← mul_assoc, ← h, add_mul, add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]