m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
⊢ FrobeniusNumber (m * n - m - n) {m, n}
simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]
m n : ℕ
cop : coprime m 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)
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
⊢ IsGreatest {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k} (m * n - m - n)
have hmn : m + n ≤ m * n := add_le_mul hm hn
case left
m n : ℕ
cop : coprime m 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 : coprime m 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}
m n : ℕ
cop : coprime m 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)
constructor
case left
m n : ℕ
cop : coprime m 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 left
m n : ℕ
cop : coprime m 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}
push_neg
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False
case left
m n : ℕ
cop : coprime m 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}
intro a b h
case left
m n : ℕ
cop : coprime m 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
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False
apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)
case left
m n : ℕ
cop : coprime m 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
case left
m n : ℕ
cop : coprime m 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
simp only [Nat.sub_sub, smul_eq_mul] at h
case left
m n : ℕ
cop : coprime m 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
case left
m n : ℕ
cop : coprime m 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
zify [hmn] at h ⊢
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h✝ : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0
case left
m n : ℕ
cop : coprime m 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
rw [← sub_eq_zero] at h ⊢
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h✝ : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
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))
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h✝ : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
h : ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n)) = 0
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0
rw [← h]
no goals
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h✝ : ↑a * ↑m + ↑b * ↑n = ↑m * ↑n - (↑m + ↑n)
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))
ring
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : k ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
⊢ k ≤ m * n - m - n
case right
m n : ℕ
cop : coprime m 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}
intro k hk
case right
m n : ℕ
cop : coprime m 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
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : k ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
⊢ k ≤ m * n - m - n
dsimp at hk
case right
m n : ℕ
cop : coprime m 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
case right
m n : ℕ
cop : coprime m 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
contrapose! hk
case right
m n : ℕ
cop : coprime m 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
case right
m n : ℕ
cop : coprime m 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
let x := chineseRemainder cop 0 k
case right
m n : ℕ
cop : coprime m 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
case right
m n : ℕ
cop : coprime m 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
have hx : x.val < m * n := chineseRemainder_lt_mul cop 0 k (ne_bot_of_gt hm) (ne_bot_of_gt hn)
case right
m n : ℕ
cop : coprime m 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

case key
m n : ℕ
cop : coprime m 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
case right
m n : ℕ
cop : coprime m 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
suffices key : x.1 ≤ k
case key
m n : ℕ
cop : coprime m 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
case key
m n : ℕ
cop : coprime m 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
refine' ModEq.le_of_lt_add x.2.2 (lt_of_le_of_lt _ (add_lt_add_right hk n))
case key
m n : ℕ
cop : coprime m 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
case key
m n : ℕ
cop : coprime m 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
rw [Nat.sub_add_cancel (le_tsub_of_add_le_left hmn)]
no goals
case key
m n : ℕ
cop : coprime m 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
exact
  ModEq.le_of_lt_add
    (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub' (dvd_mul_right m n) dvd_rfl)).symm)
    (lt_of_lt_of_le hx le_tsub_add)
case right.intro
m n : ℕ
cop : coprime m 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
case right
m n : ℕ
cop : coprime m 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
obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1
case right.intro.intro
m n : ℕ
cop : coprime m 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
case right.intro
m n : ℕ
cop : coprime m 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
obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2
no goals
case right.intro.intro
m n : ℕ
cop : coprime m 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
exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩
no goals
m n : ℕ
cop : coprime m 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
⊢ a * m + b * n = k
rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]