no goals
ι : Type u_1
α : Type ?u.20233
β : Type ?u.20236
M : Type ?u.20239
N : Type u_2
G : Type ?u.20245
k : Type ?u.20248
R : Type ?u.20251
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∏ i in s, f i ≤ ∏ i in t, f i
classical calc
    (∏ i in s, f i) ≤ (∏ i in t \ s, f i) * ∏ i in s, f i :=
      le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
    _ = ∏ i in t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
    _ = ∏ i in t, f i := by rw [sdiff_union_of_subset h]
no goals
ι : Type u_1
α : Type ?u.20233
β : Type ?u.20236
M : Type ?u.20239
N : Type u_2
G : Type ?u.20245
k : Type ?u.20248
R : Type ?u.20251
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∏ i in s, f i ≤ ∏ i in t, f i
calc
(∏ i in s, f i) ≤ (∏ i in t \ s, f i) * ∏ i in s, f i :=
le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
_ = ∏ i in t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
_ = ∏ i in t, f i := by rw [sdiff_union_of_subset h]
no goals
ι : Type u_1
α : Type ?u.20233
β : Type ?u.20236
M : Type ?u.20239
N : Type u_2
G : Type ?u.20245
k : Type ?u.20248
R : Type ?u.20251
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∀ (i : ι), i ∈ t \ s → 1 ≤ f i
simpa only [mem_sdiff, and_imp]
no goals
ι : Type u_1
α : Type ?u.20233
β : Type ?u.20236
M : Type ?u.20239
N : Type u_2
G : Type ?u.20245
k : Type ?u.20248
R : Type ?u.20251
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∏ i in t \ s ∪ s, f i = ∏ i in t, f i
rw [sdiff_union_of_subset h]