-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem filter_snd_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
    filter (fun x : A × A ↦ x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅

Proof state:
case h.a
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
x✝ : A × A
⊢ ((fun x => x.2 = m) ∘ Prod.swap) x✝ ↔ x✝.1 = m

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
this : (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m
⊢ map { toFun := Prod.swap, inj' := ⋯ }
      (filter ((fun x => x.2 = m) ∘ ⇑{ toFun := Prod.swap, inj' := ⋯ }) (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅

Tactic:
simp [this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
this : (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m
⊢ filter (fun x => x.2 = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅

Tactic:
rw [← map_swap_antidiagonal, filter_map]

Result:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
this : (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m
⊢ map { toFun := Prod.swap, inj' := ⋯ }
      (filter ((fun x => x.2 = m) ∘ ⇑{ toFun := Prod.swap, inj' := ⋯ }) (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
⊢ filter (fun x => x.2 = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅

Tactic:
have : (fun x : A × A ↦ (x.snd = m)) ∘ Prod.swap = fun x : A × A ↦ x.fst = m := by
  ext; simp

Result:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
this : (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m
⊢ filter (fun x => x.2 = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
⊢ (fun x => x.2 = m) ∘ Prod.swap = fun x => x.1 = m

Tactic:
ext

Result:
case h.a
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
x✝ : A × A
⊢ ((fun x => x.2 = m) ∘ Prod.swap) x✝ ↔ x✝.1 = m