From e4ab015e67f0ffe7a47ff5ad3d2d2b7eca0a569e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 23 Feb 2024 00:32:13 +0000
Subject: [PATCH] refactor(Data/Finsupp): Make `Finsupp.filter` computable
 (#8979)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs.

This enables some trivial computations on factorizations, eg finding the odd prime factors:
```lean
/-- info: fun₀ | 3 => 2 | 5 => 1 -/
#guard_msgs in
#eval (Nat.factorization 720).filter Odd
```

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238979.20making.20Finsupp.2Efilter.20computable/near/420898226)
---
 Mathlib/Algebra/MonoidAlgebra/Division.lean   |  9 +--
 Mathlib/Data/Finsupp/Basic.lean               | 60 +++++++++----------
 Mathlib/LinearAlgebra/Finsupp.lean            | 12 ++--
 .../MvPolynomial/WeightedHomogeneous.lean     |  7 ++-
 test/finsupp_notation.lean                    | 11 ++++
 5 files changed, 57 insertions(+), 42 deletions(-)

diff --git a/Mathlib/Algebra/MonoidAlgebra/Division.lean b/Mathlib/Algebra/MonoidAlgebra/Division.lean
index 33c503b73cd9fa..903ab4ce3d45ed 100644
--- a/Mathlib/Algebra/MonoidAlgebra/Division.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/Division.lean
@@ -123,6 +123,7 @@ theorem of'_divOf (a : G) : of' k G a /ᵒᶠ a = 1 := by
 
 /-- The remainder upon division by `of' k G g`. -/
 noncomputable def modOf (x : k[G]) (g : G) : k[G] :=
+  letI := Classical.decPred fun g₁ => ∃ g₂, g₁ = g + g₂
   x.filter fun g₁ => ¬∃ g₂, g₁ = g + g₂
 #align add_monoid_algebra.mod_of AddMonoidAlgebra.modOf
 
@@ -130,14 +131,14 @@ local infixl:70 " %ᵒᶠ " => modOf
 
 @[simp]
 theorem modOf_apply_of_not_exists_add (x : k[G]) (g : G) (g' : G)
-    (h : ¬∃ d, g' = g + d) : (x %ᵒᶠ g) g' = x g' :=
-  Finsupp.filter_apply_pos _ _ h
+    (h : ¬∃ d, g' = g + d) : (x %ᵒᶠ g) g' = x g' := by
+  classical exact Finsupp.filter_apply_pos _ _ h
 #align add_monoid_algebra.mod_of_apply_of_not_exists_add AddMonoidAlgebra.modOf_apply_of_not_exists_add
 
 @[simp]
 theorem modOf_apply_of_exists_add (x : k[G]) (g : G) (g' : G)
-    (h : ∃ d, g' = g + d) : (x %ᵒᶠ g) g' = 0 :=
-  Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]
+    (h : ∃ d, g' = g + d) : (x %ᵒᶠ g) g' = 0 := by
+  classical exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]
 #align add_monoid_algebra.mod_of_apply_of_exists_add AddMonoidAlgebra.modOf_apply_of_exists_add
 
 @[simp]
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
index c4c10ff43f2d2c..2f6ca9b9ed3b39 100644
--- a/Mathlib/Data/Finsupp/Basic.lean
+++ b/Mathlib/Data/Finsupp/Basic.lean
@@ -872,33 +872,27 @@ section Filter
 
 section Zero
 
-variable [Zero M] (p : α → Prop) (f : α →₀ M)
+variable [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M)
 
 /--
 `Finsupp.filter p f` is the finitely supported function that is `f a` if `p a` is true and `0`
 otherwise. -/
-def filter (p : α → Prop) (f : α →₀ M) : α →₀ M
-    where
-  toFun a :=
-    haveI := Classical.decPred p
-    if p a then f a else 0
-  support :=
-    haveI := Classical.decPred p
-    f.support.filter fun a => p a
+def filter (p : α → Prop) [DecidablePred p] (f : α →₀ M) : α →₀ M where
+  toFun a := if p a then f a else 0
+  support := f.support.filter p
   mem_support_toFun a := by
     simp only -- porting note: necessary to beta reduce to activate `split_ifs`
     split_ifs with h <;>
-      · simp only [h, @mem_filter _ _ (Classical.decPred p), mem_support_iff]
-        -- porting note: I needed to provide the instance explicitly
+      · simp only [h, mem_filter, mem_support_iff]
         tauto
 #align finsupp.filter Finsupp.filter
 
-theorem filter_apply (a : α) [D : Decidable (p a)] : f.filter p a = if p a then f a else 0 := by
-  rw [Subsingleton.elim D] <;> rfl
+theorem filter_apply (a : α) : f.filter p a = if p a then f a else 0 := rfl
 #align finsupp.filter_apply Finsupp.filter_apply
 
-theorem filter_eq_indicator : ⇑(f.filter p) = Set.indicator { x | p x } f :=
-  rfl
+theorem filter_eq_indicator : ⇑(f.filter p) = Set.indicator { x | p x } f := by
+  ext
+  simp [filter_apply, Set.indicator_apply]
 #align finsupp.filter_eq_indicator Finsupp.filter_eq_indicator
 
 theorem filter_eq_zero_iff : f.filter p = 0 ↔ ∀ x, p x → f x = 0 := by
@@ -920,8 +914,7 @@ theorem filter_apply_neg {a : α} (h : ¬p a) : f.filter p a = 0 := if_neg h
 #align finsupp.filter_apply_neg Finsupp.filter_apply_neg
 
 @[simp]
-theorem support_filter [D : DecidablePred p] : (f.filter p).support = f.support.filter p := by
-  rw [Subsingleton.elim D] <;> rfl
+theorem support_filter : (f.filter p).support = f.support.filter p := rfl
 #align finsupp.support_filter Finsupp.support_filter
 
 theorem filter_zero : (0 : α →₀ M).filter p = 0 := by
@@ -966,9 +959,11 @@ theorem prod_div_prod_filter [CommGroup G] (g : α → M → G) :
 
 end Zero
 
-theorem filter_pos_add_filter_neg [AddZeroClass M] (f : α →₀ M) (p : α → Prop) :
+theorem filter_pos_add_filter_neg [AddZeroClass M] (f : α →₀ M) (p : α → Prop) [DecidablePred p] :
     (f.filter p + f.filter fun a => ¬p a) = f :=
-  DFunLike.coe_injective <| Set.indicator_self_add_compl { x | p x } f
+  DFunLike.coe_injective <| by
+    simp only [coe_add, filter_eq_indicator]
+    exact Set.indicator_self_add_compl { x | p x } f
 #align finsupp.filter_pos_add_filter_neg Finsupp.filter_pos_add_filter_neg
 
 end Filter
@@ -1086,15 +1081,18 @@ def subtypeDomainAddMonoidHom : (α →₀ M) →+ Subtype p →₀ M
 #align finsupp.subtype_domain_add_monoid_hom Finsupp.subtypeDomainAddMonoidHom
 
 /-- `Finsupp.filter` as an `AddMonoidHom`. -/
-def filterAddHom (p : α → Prop) : (α →₀ M) →+ α →₀ M
+def filterAddHom (p : α → Prop) [DecidablePred p]: (α →₀ M) →+ α →₀ M
     where
   toFun := filter p
   map_zero' := filter_zero p
-  map_add' f g := DFunLike.coe_injective <| Set.indicator_add { x | p x } f g
+  map_add' f g := DFunLike.coe_injective <| by
+    simp only [filter_eq_indicator, coe_add]
+    exact Set.indicator_add { x | p x } f g
 #align finsupp.filter_add_hom Finsupp.filterAddHom
 
 @[simp]
-theorem filter_add {v v' : α →₀ M} : (v + v').filter p = v.filter p + v'.filter p :=
+theorem filter_add [DecidablePred p] {v v' : α →₀ M} :
+    (v + v').filter p = v.filter p + v'.filter p :=
   (filterAddHom p).map_add v v'
 #align finsupp.filter_add Finsupp.filter_add
 
@@ -1114,15 +1112,15 @@ theorem subtypeDomain_finsupp_sum [Zero N] {s : β →₀ N} {h : β → N → 
   subtypeDomain_sum
 #align finsupp.subtype_domain_finsupp_sum Finsupp.subtypeDomain_finsupp_sum
 
-theorem filter_sum (s : Finset ι) (f : ι → α →₀ M) :
+theorem filter_sum [DecidablePred p] (s : Finset ι) (f : ι → α →₀ M) :
     (∑ a in s, f a).filter p = ∑ a in s, filter p (f a) :=
   map_sum (filterAddHom p) f s
 #align finsupp.filter_sum Finsupp.filter_sum
 
-theorem filter_eq_sum (p : α → Prop) [D : DecidablePred p] (f : α →₀ M) :
+theorem filter_eq_sum (p : α → Prop) [DecidablePred p] (f : α →₀ M) :
     f.filter p = ∑ i in f.support.filter p, single i (f i) :=
   (f.filter p).sum_single.symm.trans <|
-    Finset.sum_congr (by rw [Subsingleton.elim D] <;> rfl) fun x hx => by
+    Finset.sum_congr rfl fun x hx => by
       rw [filter_apply_pos _ _ (mem_filter.1 hx).2]
 #align finsupp.filter_eq_sum Finsupp.filter_eq_sum
 
@@ -1163,12 +1161,12 @@ theorem erase_sub (a : α) (f₁ f₂ : α →₀ G) : erase a (f₁ - f₂) = e
 #align finsupp.erase_sub Finsupp.erase_sub
 
 @[simp]
-theorem filter_neg (p : α → Prop) (f : α →₀ G) : filter p (-f) = -filter p f :=
+theorem filter_neg (p : α → Prop) [DecidablePred p] (f : α →₀ G) : filter p (-f) = -filter p f :=
   (filterAddHom p : (_ →₀ G) →+ _).map_neg f
 #align finsupp.filter_neg Finsupp.filter_neg
 
 @[simp]
-theorem filter_sub (p : α → Prop) (f₁ f₂ : α →₀ G) :
+theorem filter_sub (p : α → Prop) [DecidablePred p] (f₁ f₂ : α →₀ G) :
     filter p (f₁ - f₂) = filter p f₁ - filter p f₂ :=
   (filterAddHom p : (_ →₀ G) →+ _).map_sub f₁ f₂
 #align finsupp.filter_sub Finsupp.filter_sub
@@ -1265,7 +1263,7 @@ def finsuppProdEquiv : (α × β →₀ M) ≃ (α →₀ β →₀ M)
       forall₃_true_iff, (single_sum _ _ _).symm, sum_single]
 #align finsupp.finsupp_prod_equiv Finsupp.finsuppProdEquiv
 
-theorem filter_curry (f : α × β →₀ M) (p : α → Prop) :
+theorem filter_curry (f : α × β →₀ M) (p : α → Prop) [DecidablePred p] :
     (f.filter fun a : α × β => p a.1).curry = f.curry.filter p := by
   classical
     rw [Finsupp.curry, Finsupp.curry, Finsupp.sum, Finsupp.sum, filter_sum, support_filter,
@@ -1567,12 +1565,14 @@ theorem support_smul_eq [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulD
 
 section
 
-variable {p : α → Prop}
+variable {p : α → Prop} [DecidablePred p]
 
 @[simp]
 theorem filter_smul {_ : Monoid R} [AddMonoid M] [DistribMulAction R M] {b : R} {v : α →₀ M} :
     (b • v).filter p = b • v.filter p :=
-  DFunLike.coe_injective <| Set.indicator_const_smul { x | p x } b v
+  DFunLike.coe_injective <| by
+    simp only [filter_eq_indicator, coe_smul]
+    exact Set.indicator_const_smul { x | p x } b v
 #align finsupp.filter_smul Finsupp.filter_smul
 
 end
diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean
index d666bfdade0131..57c2935628b310 100644
--- a/Mathlib/LinearAlgebra/Finsupp.lean
+++ b/Mathlib/LinearAlgebra/Finsupp.lean
@@ -344,7 +344,7 @@ theorem supported_eq_span_single (s : Set α) :
 variable (M)
 
 /-- Interpret `Finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/
-def restrictDom (s : Set α) : (α →₀ M) →ₗ[R] supported M R s :=
+def restrictDom (s : Set α) [DecidablePred (· ∈ s)] : (α →₀ M) →ₗ[R] supported M R s :=
   LinearMap.codRestrict _
     { toFun := filter (· ∈ s)
       map_add' := fun _ _ => filter_add
@@ -357,21 +357,21 @@ variable {M R}
 section
 
 @[simp]
-theorem restrictDom_apply (s : Set α) (l : α →₀ M) :
-    ((restrictDom M R s : (α →₀ M) →ₗ[R] supported M R s) l : α →₀ M) = Finsupp.filter (· ∈ s) l :=
-  rfl
+theorem restrictDom_apply (s : Set α) (l : α →₀ M) [DecidablePred (· ∈ s)]:
+    (restrictDom M R s l : α →₀ M) = Finsupp.filter (· ∈ s) l := rfl
 #align finsupp.restrict_dom_apply Finsupp.restrictDom_apply
 
 end
 
-theorem restrictDom_comp_subtype (s : Set α) :
+theorem restrictDom_comp_subtype (s : Set α) [DecidablePred (· ∈ s)] :
     (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id := by
   ext l a
   by_cases h : a ∈ s <;> simp [h]
   exact ((mem_supported' R l.1).1 l.2 a h).symm
 #align finsupp.restrict_dom_comp_subtype Finsupp.restrictDom_comp_subtype
 
-theorem range_restrictDom (s : Set α) : LinearMap.range (restrictDom M R s) = ⊤ :=
+theorem range_restrictDom (s : Set α) [DecidablePred (· ∈ s)] :
+    LinearMap.range (restrictDom M R s) = ⊤ :=
   range_eq_top.2 <|
     Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s)
 #align finsupp.range_restrict_dom Finsupp.range_restrictDom
diff --git a/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean b/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
index 568ffe8f9fb54f..6d6ca55709d8ba 100644
--- a/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
+++ b/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
@@ -326,6 +326,7 @@ variable {R}
   See `sum_weightedHomogeneousComponent` for the statement that `φ` is equal to the sum
   of all its weighted homogeneous components. -/
 def weightedHomogeneousComponent (w : σ → M) (n : M) : MvPolynomial σ R →ₗ[R] MvPolynomial σ R :=
+  letI := Classical.decEq M
   (Submodule.subtype _).comp <| Finsupp.restrictDom _ _ { d | weightedDegree' w d = n }
 #align mv_polynomial.weighted_homogeneous_component MvPolynomial.weightedHomogeneousComponent
 
@@ -336,13 +337,15 @@ variable {w : σ → M} (n : M) (φ ψ : MvPolynomial σ R)
 theorem coeff_weightedHomogeneousComponent [DecidableEq M] (d : σ →₀ ℕ) :
     coeff d (weightedHomogeneousComponent w n φ) =
       if weightedDegree' w d = n then coeff d φ else 0 :=
-  Finsupp.filter_apply (fun d : σ →₀ ℕ => weightedDegree' w d = n) φ d
+  letI := Classical.decEq M
+  Finsupp.filter_apply (fun d : σ →₀ ℕ => weightedDegree' w d = n) φ d |>.trans <| by convert rfl
 #align mv_polynomial.coeff_weighted_homogeneous_component MvPolynomial.coeff_weightedHomogeneousComponent
 
 theorem weightedHomogeneousComponent_apply [DecidableEq M] :
     weightedHomogeneousComponent w n φ =
       ∑ d in φ.support.filter fun d => weightedDegree' w d = n, monomial d (coeff d φ) :=
-  Finsupp.filter_eq_sum (fun d : σ →₀ ℕ => weightedDegree' w d = n) φ
+  letI := Classical.decEq M
+  Finsupp.filter_eq_sum (fun d : σ →₀ ℕ => weightedDegree' w d = n) φ |>.trans <| by convert rfl
 #align mv_polynomial.weighted_homogeneous_component_apply MvPolynomial.weightedHomogeneousComponent_apply
 
 /-- The `n` weighted homogeneous component of a polynomial is weighted homogeneous of
diff --git a/test/finsupp_notation.lean b/test/finsupp_notation.lean
index b529df0a55a231..2289281f1ecf58 100644
--- a/test/finsupp_notation.lean
+++ b/test/finsupp_notation.lean
@@ -1,4 +1,5 @@
 import Mathlib.Data.Finsupp.Notation
+import Mathlib.Data.Nat.Factorization.Basic
 
 example : (fun₀ | 1 => 3) 1 = 3 :=
 by simp
@@ -18,3 +19,13 @@ info:
   guard <|
     reprStr (Finsupp.mk {1, 2} (fun | 1 | 2 => 3 | _ => 0) (fun x => by aesop))
       = "fun₀ | 1 => 3 | 2 => 3"
+
+/-! ## (computable) number theory examples-/
+
+/-- info: fun₀ | 2 => 2 | 7 => 1 -/
+#guard_msgs in
+#eval Nat.factorization 28
+
+/-- info: fun₀ | 3 => 2 | 5 => 1 -/
+#guard_msgs in
+#eval (Nat.factorization 720).filter Odd