no goals
α : Type u_2
β : Type ?u.380672
ι : Type ?u.380675
G : Type ?u.380678
M✝ : Type ?u.380681
N : Type ?u.380684
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_1
inst✝ : OrderedCommMonoid M
i : α
f : α → M
hf : Set.Finite (mulSupport f)
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j
classical calc
    f i ≤ ∏ j in insert i hf.toFinset, f j :=
      Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
    _ = ∏ᶠ j, f j :=
      (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm
no goals
α : Type u_2
β : Type ?u.380672
ι : Type ?u.380675
G : Type ?u.380678
M✝ : Type ?u.380681
N : Type ?u.380684
inst✝² : CommMonoid M✝
inst✝¹ : CommMonoid N
f✝ g : α → M✝
a b : α
s t : Set α
M : Type u_1
inst✝ : OrderedCommMonoid M
i : α
f : α → M
hf : Set.Finite (mulSupport f)
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j
calc
f i ≤ ∏ j in insert i hf.toFinset, f j :=
Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
_ = ∏ᶠ j, f j :=
(finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm