case a.mk
n m x y : ℕ
⊢ (x, y) ∈ filter (fun x => x.fst = m) (antidiagonal n) ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
n m : ℕ
⊢ filter (fun x => x.fst = m) (antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅
ext ⟨x, y⟩
case a.mk
n m x y : ℕ
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
case a.mk
n m x y : ℕ
⊢ (x, y) ∈ filter (fun x => x.fst = m) (antidiagonal n) ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
simp only [mem_filter, Nat.mem_antidiagonal]
case a.mk.inl
n m x y : ℕ
h : m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ {(m, n - m)}

case a.mk.inr
n m x y : ℕ
h : ¬m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
case a.mk
n m x y : ℕ
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ if m ≤ n then {(m, n - m)} else ∅
split_ifs with h
no goals
case a.mk.inl
n m x y : ℕ
h : m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ {(m, n - m)}
simp (config := { contextual := true }) [and_comm, eq_tsub_iff_add_eq_of_le h, add_comm]
case a.mk.inr
n m x y : ℕ
h : n < m
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
case a.mk.inr
n m x y : ℕ
h : ¬m ≤ n
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
rw [not_le] at h
case a.mk.inr
n m x y : ℕ
h : n < m
⊢ x + y = n → ¬x = m
case a.mk.inr
n m x y : ℕ
h : n < m
⊢ x + y = n ∧ x = m ↔ (x, y) ∈ ∅
simp only [not_mem_empty, iff_false_iff, not_and, decide_eq_true_eq]
no goals
case a.mk.inr
n m x y : ℕ
h : n < m
⊢ x + y = n → ¬x = m
exact fun hn => ne_of_lt (lt_of_le_of_lt (le_self_add.trans hn.le) h)