n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
n m : ℕ
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
have : (fun x : ℕ × ℕ ↦ (x.snd = m)) ∘ Prod.swap = fun x : ℕ × ℕ ↦ x.fst = m := by
  ext ; simp
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ filter (fun x => x.snd = m)
      (map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ filter (fun x => x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
rw [← map_swap_antidiagonal]
no goals
n m : ℕ
this : (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
⊢ filter (fun x => x.snd = m)
      (map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅
simp [filter_map, this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
case h.a
n m : ℕ
x✝ : ℕ × ℕ
⊢ ((fun x => x.snd = m) ∘ Prod.swap) x✝ ↔ x✝.fst = m
n m : ℕ
⊢ (fun x => x.snd = m) ∘ Prod.swap = fun x => x.fst = m
ext
no goals
case h.a
n m : ℕ
x✝ : ℕ × ℕ
⊢ ((fun x => x.snd = m) ∘ Prod.swap) x✝ ↔ x✝.fst = m
simp