n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) ↔ x.fst + x.snd = n
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
rw [antidiagonal, mem_map]
case mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) → x.fst + x.snd = n

case mpr
n : ℕ
x : ℕ × ℕ
⊢ x.fst + x.snd = n → ∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) ↔ x.fst + x.snd = n
constructor
case mp.intro.intro
n i : ℕ
hi : i ∈ range (n + 1)
⊢ (i, n - i).fst + (i, n - i).snd = n
case mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x) → x.fst + x.snd = n
rintro ⟨i, hi, rfl⟩
case mp.intro.intro
n i : ℕ
hi : i ≤ n
⊢ (i, n - i).fst + (i, n - i).snd = n
case mp.intro.intro
n i : ℕ
hi : i ∈ range (n + 1)
⊢ (i, n - i).fst + (i, n - i).snd = n
rw [mem_range, lt_succ_iff] at hi
no goals
case mp.intro.intro
n i : ℕ
hi : i ≤ n
⊢ (i, n - i).fst + (i, n - i).snd = n
exact add_tsub_cancel_of_le hi
case mpr
x : ℕ × ℕ
⊢ ∃ a, a ∈ range (x.fst + x.snd + 1) ∧ (a, x.fst + x.snd - a) = x
case mpr
n : ℕ
x : ℕ × ℕ
⊢ x.fst + x.snd = n → ∃ a, a ∈ range (n + 1) ∧ (a, n - a) = x
rintro rfl
case mpr.refine'_1
x : ℕ × ℕ
⊢ x.fst ∈ range (x.fst + x.snd + 1)

case mpr.refine'_2
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst) = x
case mpr
x : ℕ × ℕ
⊢ ∃ a, a ∈ range (x.fst + x.snd + 1) ∧ (a, x.fst + x.snd - a) = x
refine' ⟨x.fst, _, _⟩
case mpr.refine'_1
x : ℕ × ℕ
⊢ 0 < x.snd + 1
case mpr.refine'_1
x : ℕ × ℕ
⊢ x.fst ∈ range (x.fst + x.snd + 1)
rw [mem_range, add_assoc, lt_add_iff_pos_right]
no goals
case mpr.refine'_1
x : ℕ × ℕ
⊢ 0 < x.snd + 1
exact zero_lt_succ _
no goals
case mpr.refine'_2
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst) = x
exact Prod.ext rfl (by simp only [add_tsub_cancel_left])
no goals
x : ℕ × ℕ
⊢ (x.fst, x.fst + x.snd - x.fst).snd = x.snd
simp only [add_tsub_cancel_left]