feat(data/dfinsupp): add submodule.bsupr_eq_range_dfinsupp_lsum (#9202)

Also a version for `add_submonoid`. Unfortunately the proofs are almost identical, but that's consistent with the surrounding bits of the file anyway.

The key result is a dfinsupp version of the lemma in #8246,
```lean
x ∈ (⨆ i (H : p i), f i) ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) :=
```
as
```lean
x ∈ (⨆ i (h : p i), S i) ↔ ∃ f : Π₀ i, S i, dfinsupp.lsum ℕ (λ i, (S i).subtype) (f.filter p) = x
```

src/data/dfinsupp.lean

@@ -1180,34 +1180,63 @@ begin
 end
 
 /-- The supremum of a family of commutative additive submonoids is equal to the range of
-`finsupp.sum_add_hom`; that is, every element in the `supr` can be produced from taking a finite
-number of non-zero elements of `p i`, coercing them to `γ`, and summing them. -/
+`dfinsupp.sum_add_hom`; that is, every element in the `supr` can be produced from taking a finite
+number of non-zero elements of `S i`, coercing them to `γ`, and summing them. -/
 lemma _root_.add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom [add_comm_monoid γ]
-  (p : ι → add_submonoid γ) : supr p = (dfinsupp.sum_add_hom (λ i, (p i).subtype)).mrange :=
+  (S : ι → add_submonoid γ) : supr S = (dfinsupp.sum_add_hom (λ i, (S i).subtype)).mrange :=
 begin
   apply le_antisymm,
   { apply supr_le _,
     intros i y hy,
     exact ⟨dfinsupp.single i ⟨y, hy⟩, dfinsupp.sum_add_hom_single _ _ _⟩, },
   { rintros x ⟨v, rfl⟩,
-    exact add_submonoid.dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr p i : p i ≤ _) (v i).prop) }
+    exact add_submonoid.dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr S i : S i ≤ _) (v i).prop) }
+end
+
+/-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
+`dfinsupp.sum_add_hom` composed with `dfinsupp.filter_add_monoid_hom`; that is, every element in the
+bounded `supr` can be produced from taking a finite number of non-zero elements from the `S i` that
+satisfy `p i`, coercing them to `γ`, and summing them. -/
+lemma _root_.add_submonoid.bsupr_eq_mrange_dfinsupp_sum_add_hom (p : ι → Prop)
+  [decidable_pred p] [add_comm_monoid γ] (S : ι → add_submonoid γ) :
+  (⨆ i (h : p i), S i) =
+    ((sum_add_hom (λ i, (S i).subtype)).comp (filter_add_monoid_hom _ p)).mrange :=
+begin
+  apply le_antisymm,
+  { apply bsupr_le _,
+    intros i hi y hy,
+    refine ⟨dfinsupp.single i ⟨y, hy⟩, _⟩,
+    rw [add_monoid_hom.comp_apply, filter_add_monoid_hom_apply, filter_single_pos _ _ hi],
+    exact sum_add_hom_single _ _ _, },
+  { rintros x ⟨v, rfl⟩,
+    refine add_submonoid.dfinsupp_sum_add_hom_mem _ _ _ (λ i hi, _),
+    refine add_submonoid.mem_supr_of_mem i _,
+    by_cases hp : p i,
+    { simp [hp], },
+    { simp [hp] }, }
 end
 
 lemma _root_.add_submonoid.mem_supr_iff_exists_dfinsupp [add_comm_monoid γ]
-  (p : ι → add_submonoid γ) (x : γ) :
-  x ∈ supr p ↔ ∃ f : Π₀ i, p i, dfinsupp.sum_add_hom (λ i, (p i).subtype) f = x :=
-set_like.ext_iff.mp (add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom p) x
+  (S : ι → add_submonoid γ) (x : γ) :
+  x ∈ supr S ↔ ∃ f : Π₀ i, S i, dfinsupp.sum_add_hom (λ i, (S i).subtype) f = x :=
+set_like.ext_iff.mp (add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom S) x
 
 /-- A variant of `add_submonoid.mem_supr_iff_exists_dfinsupp` with the RHS fully unfolded. -/
 lemma _root_.add_submonoid.mem_supr_iff_exists_dfinsupp' [add_comm_monoid γ]
-  (p : ι → add_submonoid γ) [Π i (x : p i), decidable (x ≠ 0)] (x : γ) :
-  x ∈ supr p ↔ ∃ f : Π₀ i, p i, f.sum (λ i xi, ↑xi) = x :=
+  (S : ι → add_submonoid γ) [Π i (x : S i), decidable (x ≠ 0)] (x : γ) :
+  x ∈ supr S ↔ ∃ f : Π₀ i, S i, f.sum (λ i xi, ↑xi) = x :=
 begin
   rw add_submonoid.mem_supr_iff_exists_dfinsupp,
   simp_rw sum_add_hom_apply,
   congr',
 end
 
+lemma _root_.add_submonoid.mem_bsupr_iff_exists_dfinsupp (p : ι → Prop)
+  [decidable_pred p] [add_comm_monoid γ] (S : ι → add_submonoid γ) (x : γ) :
+  x ∈ (⨆ i (h : p i), S i) ↔
+    ∃ f : Π₀ i, S i, dfinsupp.sum_add_hom (λ i, (S i).subtype) (f.filter p) = x :=
+set_like.ext_iff.mp (add_submonoid.bsupr_eq_mrange_dfinsupp_sum_add_hom p S) x
+
 omit dec
 lemma sum_add_hom_comm {ι₁ ι₂ : Sort*} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} {γ : Type*}
   [decidable_eq ι₁] [decidable_eq ι₂] [Π i, add_zero_class (β₁ i)] [Π i, add_zero_class (β₂ i)]

src/linear_algebra/dfinsupp.lean

@@ -207,6 +207,7 @@ end dfinsupp
 include dec_ι
 
 namespace submodule
+open dfinsupp
 
 lemma dfinsupp_sum_mem {β : ι → Type*} [Π i, has_zero (β i)]
   [Π i (x : β i), decidable (x ≠ 0)] (S : submodule R N)
@@ -232,6 +233,29 @@ begin
     exact dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr p i : p i ≤ _) (v i).prop) }
 end
 
+/-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
+`dfinsupp.sum_add_hom` composed with `dfinsupp.filter_add_monoid_hom`; that is, every element in the
+bounded `supr` can be produced from taking a finite number of non-zero elements from the `S i` that
+satisfy `p i`, coercing them to `γ`, and summing them. -/
+lemma bsupr_eq_range_dfinsupp_lsum (p : ι → Prop)
+  [decidable_pred p] (S : ι → submodule R N) :
+  (⨆ i (h : p i), S i) =
+    ((dfinsupp.lsum ℕ (λ i, (S i).subtype)).comp (dfinsupp.filter_linear_map R _ p)).range :=
+begin
+  apply le_antisymm,
+  { apply bsupr_le _,
+    intros i hi y hy,
+    refine ⟨dfinsupp.single i ⟨y, hy⟩, _⟩,
+    rw [linear_map.comp_apply, filter_linear_map_apply, filter_single_pos _ _ hi],
+    exact dfinsupp.sum_add_hom_single _ _ _, },
+  { rintros x ⟨v, rfl⟩,
+    refine dfinsupp_sum_add_hom_mem _ _ _ (λ i hi, _),
+    refine mem_supr_of_mem i _,
+    by_cases hp : p i,
+    { simp [hp], },
+    { simp [hp] }, }
+end
+
 lemma mem_supr_iff_exists_dfinsupp (p : ι → submodule R N) (x : N) :
   x ∈ supr p ↔ ∃ f : Π₀ i, p i, dfinsupp.lsum ℕ (λ i, (p i).subtype) f = x :=
 set_like.ext_iff.mp (supr_eq_range_dfinsupp_lsum p) x
@@ -246,4 +270,10 @@ begin
   congr',
 end
 
+lemma mem_bsupr_iff_exists_dfinsupp (p : ι → Prop) [decidable_pred p] (S : ι → submodule R N)
+  (x : N) :
+  x ∈ (⨆ i (h : p i), S i) ↔
+    ∃ f : Π₀ i, S i, dfinsupp.lsum ℕ (λ i, (S i).subtype) (f.filter p) = x :=
+set_like.ext_iff.mp (bsupr_eq_range_dfinsupp_lsum p S) x
+
 end submodule