feat(Topology/Algebra/InfiniteSum/Order): Add tprod_subtype_le (#12600)

We add a lemma that says the tprod/tsum over a subtype is less than the full sum. Needed for #12456

Author: CBirkbeck

Mathlib/Topology/Algebra/InfiniteSum/Order.lean

@@ -81,6 +81,15 @@ theorem tprod_le_tprod_of_inj {g : κ → α} (e : ι → κ) (he : Injective e)
   hasProd_le_inj _ he hs h hf.hasProd hg.hasProd
 #align tsum_le_tsum_of_inj tsum_le_tsum_of_inj
 
+@[to_additive]
+lemma tprod_subtype_le {κ γ : Type*} [OrderedCommGroup γ] [UniformSpace γ] [UniformGroup γ]
+    [OrderClosedTopology γ] [ CompleteSpace γ] (f : κ → γ) (β : Set κ) (h : ∀ a : κ, 1 ≤ f a)
+    (hf : Multipliable f) : (∏' (b : β), f b) ≤ (∏' (a : κ), f a) := by
+  apply tprod_le_tprod_of_inj _ (Subtype.coe_injective) (by simp only [Subtype.range_coe_subtype,
+    Set.setOf_mem_eq, h, implies_true]) (by simp only [le_refl,
+    Subtype.forall, implies_true]) (by apply hf.subtype)
+  apply hf
+
 @[to_additive]
 theorem prod_le_hasProd (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : HasProd f a) :
     ∏ i ∈ s, f i ≤ a :=