Theorem: IMOSL.IMO2021N2.good_cond1 (IMOSLLean4/IMO2021/N2/N2.lean)

State before:
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
rcases (x a).eq_or_eq_not (x b) with h6 | h6
State after:
case inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2

case inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2

State before:
case inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
rcases (x c).eq_or_eq_not (x b) with h7 | h7
State after:
case inr.inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2

case inr.inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2

State before:
case inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
exact ⟨a, b, h, h0, h1.le.trans h2, h6, k, h3⟩
State after:
no goals

State before:
case inr.inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
exact ⟨b, c, h.trans h0.le, h1, h2, h7.symm, m, h5⟩
State after:
no goals

State before:
case inr.inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
exact ⟨a, c, h, h0.trans h1, h2, h6.trans h7.symm, l, h4⟩
State after:
no goals