-- Mathlib/NumberTheory/FrobeniusNumber.lean
theorem frobeniusNumber_pair (cop : Coprime m n) (hm : 1 < m) (hn : 1 < n) :
    FrobeniusNumber (m * n - m - n) {m, n}

Proof state:
case intro
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Tactic:
obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2

Result:
case intro.intro
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a * m + b * n = m * n - (m + n)
⊢ (a + 1) * m + (b + 1) * n = m * n

Tactic:
zify [hmn] at h ⊢

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n = ↑m * ↑n

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k}

Tactic:
intro a b h

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False

Proof state:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)

Tactic:
constructor

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}

case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ upperBounds {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}

Proof state:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Tactic:
obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1

Result:
case intro
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : ¬∃ m_1 n_1, m_1 * m + n_1 * n = k
⊢ k ≤ m * n - m - n

Tactic:
contrapose! hk

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Tactic:
suffices key : x.1 ≤ k by
  obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1
  obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2
  exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ k

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ k

Tactic:
refine ModEq.le_of_lt_add x.2.2 (lt_of_le_of_lt ?_ (add_lt_add_right hk n))

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m - n + n

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ (a + 1) * m + (b + 1) * n = m * n

Tactic:
simp only [Nat.sub_sub, smul_eq_mul] at h

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a * m + b * n = m * n - (m + n)
⊢ (a + 1) * m + (b + 1) * n = m * n

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Tactic:
let x := chineseRemainder cop 0 k

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Proof state:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
⊢ FrobeniusNumber (m * n - m - n) {m, n}

Tactic:
simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]

Result:
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m - n + n

Tactic:
rw [Nat.sub_add_cancel (le_tsub_of_add_le_left hmn)]

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0

Tactic:
rw [← h]

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n))

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}

Tactic:
push_neg

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k}

Proof state:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Tactic:
have hx : x.val < m * n := chineseRemainder_lt_mul cop 0 k (ne_bot_of_gt hm) (ne_bot_of_gt hn)

Result:
case right
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
x : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False

Tactic:
apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)

Result:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ (a + 1) * m + (b + 1) * n = m * n

Proof state:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n))

Tactic:
ring

Result:
no goals