feat(Data/Finset/Filter): tag Finset.filter_congr as congr (#38695)

Tag `Finset.filter_congr` as `@[congr]`.

This should force simp to eta-expand any `Fintype` instances if necessary after using the simp lemma `Fintype.card_ofFinset`.

`theorem card_ofFinset {p : Set α} (s : Finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : @Fintype.card p (ofFinset s H) = #s` rewrites any `@Fintype.card p (Fintype.ofFinset s H)` in the goal to `Finset.card s`, where the finset `s` comes from the matched `Fintype` instance in the goal. This means the syntactic form of the goal will depend on the `Fintype` instance, and `Finset.filter_congr` should help normalize things after it. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20SimpleGraph.20.2F.20Finset.20membership.20diamond/with/591592061).

Author: SnirBroshi

Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean

@@ -131,7 +131,7 @@ lemma schwartz_zippel_sup_sum :
                 {x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0}) := by
             rw [← filter_filter, filter_piFinset_eq_map_consEquiv S (fun r ↦ eval r pₖ ≠ 0),
               filter_map, card_map, product_eq_biUnion_right, filter_biUnion]
-            simp [Function.comp_def, filter_image]
+            simp [filter_image]
             rfl
           _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0,
                 #(image (fun x₀ ↦ (x₀, xₜ)) {x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0}) :=

Mathlib/Algebra/Order/Antidiag/Prod.lean

@@ -167,10 +167,8 @@ theorem filter_fst_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable
 
 theorem filter_snd_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
     {x ∈ antidiagonal n | x.snd = m} = if m ≤ n then {(n - m, m)} else ∅ := by
-  have : (fun x : A × A ↦ (x.snd = m)) ∘ Prod.swap = fun x : A × A ↦ x.fst = m := by
-    ext; simp
   rw [← map_swap_antidiagonal, filter_map]
-  simp [this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
+  simp [filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
 
 end OrderedSub
 

Mathlib/Combinatorics/Additive/Energy.lean

@@ -167,7 +167,7 @@ variable [CommMonoid α]
 
 @[to_additive] lemma mulEnergy_comm (s t : Finset α) : Eₘ[s, t] = Eₘ[t, s] := by
   rw [mulEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]
-  simp [-Finset.card_map, mulEnergy, mul_comm, map_eq_image, Function.comp_def]
+  simp [mulEnergy, mul_comm, map_eq_image]
 
 end CommMonoid
 

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -348,8 +348,10 @@ section Finite
 
 variable [Fintype V]
 
-instance neighborSetFintype [DecidableRel G.Adj] (v : V) : Fintype (G.neighborSet v) :=
-  Subtype.fintype (· ∈ G.neighborSet v)
+/-- `Fintype` for `neighborSet` -/
+@[deprecated inferInstance (since := "2026-04-29")]
+abbrev neighborSetFintype [DecidableRel G.Adj] (v : V) : Fintype (G.neighborSet v) :=
+  inferInstance
 
 theorem neighborFinset_eq_filter {v : V} [DecidableRel G.Adj] :
     G.neighborFinset v = ({w | G.Adj v w} : Finset _) := by ext; simp

Mathlib/Data/Finset/Filter.lean

@@ -172,6 +172,7 @@ theorem filter_false_of_mem (h : ∀ x ∈ s, ¬p x) : s.filter p = ∅ := filte
 theorem filter_const (p : Prop) [Decidable p] (s : Finset α) :
     (s.filter fun _a => p) = if p then s else ∅ := by split_ifs <;> simp [*]
 
+@[congr]
 theorem filter_congr {s : Finset α} (H : ∀ x ∈ s, p x ↔ q x) : filter p s = filter q s :=
   eq_of_veq <| Multiset.filter_congr H
 

Mathlib/Data/Finset/Image.lean

@@ -176,7 +176,7 @@ theorem filter_map {p : β → Prop} [DecidablePred p] :
 lemma map_filter' (p : α → Prop) [DecidablePred p] (f : α ↪ β) (s : Finset α)
     [DecidablePred (∃ a, p a ∧ f a = ·)] :
     (s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b := by
-  simp [Function.comp_def, filter_map, f.injective.eq_iff]
+  simp [filter_map]
 
 lemma filter_attach' [DecidableEq α] (s : Finset α) (p : s → Prop) [DecidablePred p] :
     s.attach.filter p =

Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

@@ -219,7 +219,7 @@ theorem MultilinearMap.domCoprod_alternization [DecidableEq ιa] [DecidableEq ι
       simp [QuotientGroup.leftRel_apply, f, Quotient.eq]
     _ = ∑ τ ∈ {τ | τ⁻¹ ∈ f.range}, sign (σ * τ) • domDomCongr (σ * τ) (a.domCoprod b) := by
       conv_lhs => rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]
-      simp [Function.comp_def, -MonoidHom.mem_range]
+      simp [-MonoidHom.mem_range]
     _ = ∑ τ, sign (σ * f τ) • domDomCongr (σ * f τ) (a.domCoprod b) := by
       simp_rw [f, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
         Finset.sum_image sumCongrHom_injective.injOn]