/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl

! This file was ported from Lean 3 source module algebra.big_operators.order
! leanprover-community/mathlib commit 824f9ae93a4f5174d2ea948e2d75843dd83447bb
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.AbsoluteValue
import Mathlib.Algebra.Order.Ring.WithTop
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Fintype.Card

/-!
# Results about big operators with values in an ordered algebraic structure.

Mostly monotonicity results for the `∏` and `∑` operations.

-/

open Function

open BigOperators

variable {ι: Type ?u.26
ι α: Type ?u.114554
α β: Type ?u.75944
β M: Type ?u.111508
M N: Type ?u.38
N G: Type ?u.114566
G k: Type ?u.20
k R: Type ?u.114572
R : Type _: Type (?u.114566+1)
Type _}

namespace Finset

section OrderedCommMonoid

variable [CommMonoid: Type ?u.19646 → Type ?u.19646
CommMonoid M: Type ?u.23981
M] [OrderedCommMonoid: Type ?u.15696 → Type ?u.15696
OrderedCommMonoid N: Type ?u.38
N]

/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
submultiplicative on `{x | p x}`, i.e., `p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be
a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∏ x in s, g x) ≤ ∏ x in s, f (g x)`. -/
@[to_additive le_sum_nonempty_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N)
  (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
    (∀ (x y : M), p x → p y → p (x + y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive_on_pred]
theorem le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N)
  (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
    (∀ (x y : M), p x → p y → p (x * y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative_on_pred (f: M → N
f : M: Type ?u.65
M → N: Type ?u.68
N) (p: M → Prop
p : M: Type ?u.65
M → Prop: Type
Prop)
    (h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
h_mul : ∀ x: ?m.95
x y: ?m.98
y, p: M → Prop
p x: ?m.95
x → p: M → Prop
p y: ?m.98
y → f: M → N
f (x: ?m.95
x * y: ?m.98
y) ≤ f: M → N
f x: ?m.95
x * f: M → N
f y: ?m.98
y) (hp_mul: ∀ (x y : M), p x → p y → p (x * y)
hp_mul : ∀ x: ?m.2274
x y: ?m.2277
y, p: M → Prop
p x: ?m.2274
x → p: M → Prop
p y: ?m.2277
y → p: M → Prop
p (x: ?m.2274
x * y: ?m.2277
y))
    (g: ι → M
g : ι: Type ?u.56
ι → M: Type ?u.65
M) (s: Finset ι
s : Finset: Type ?u.2705 → Type ?u.2705
Finset ι: Type ?u.56
ι) (hs_nonempty: Finset.Nonempty s
hs_nonempty : s: Finset ι
s.Nonempty: {α : Type ?u.2708} → Finset α → Prop
Nonempty) (hs: ∀ (i : ι), i ∈ s → p (g i)
hs : ∀ i: ?m.2716
i ∈ s: Finset ι
s, p: M → Prop
p (g: ι → M
g i: ?m.2716
i)) :
    f: M → N
f (∏ i: ?m.2781
i in s: Finset ι
s, g: ι → M
g i: ?m.2781
i) ≤ ∏ i: ?m.2803
i in s: Finset ι
s, f: M → N
f (g: ι → M
g i: ?m.2803
i) := by
Goals accomplished! 🐙
  ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)refine' le_trans: ∀ {α : Type ?u.2879} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans (Multiset.le_prod_nonempty_of_submultiplicative_on_pred: ∀ {α : Type ?u.3190} {β : Type ?u.3191} [inst : CommMonoid α] [inst_1 : OrderedCommMonoid β] (f : α → β) (p : α → Prop),
  (∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) →
    (∀ (a b : α), p a → p b → p (a * b)) →
      ∀ (s : Multiset α), s ≠ ∅ → (∀ (a : α), a ∈ s → p a) → f (Multiset.prod s) ≤ Multiset.prod (Multiset.map f s)
Multiset.le_prod_nonempty_of_submultiplicative_on_pred f: M → N
f p: M → Prop
p h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
h_mul hp_mul: ∀ (x y : M), p x → p y → p (x * y)
hp_mul _: Multiset ?m.3192
_ _: ?m.3278 ≠ ∅
_ _: ∀ (a : ?m.3192), a ∈ ?m.3278 → p a
_) _: ?m.2883 ≤ ?m.2884
_ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_1Multiset.map (fun i => g i) s.val ≠ ∅
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_2∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_3Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
  ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)·ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_1Multiset.map (fun i => g i) s.val ≠ ∅ ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_1Multiset.map (fun i => g i) s.val ≠ ∅
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_2∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_3Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)simp [hs_nonempty: Finset.Nonempty s
hs_nonempty.ne_empty: ∀ {α : Type ?u.3289} {s : Finset α}, Finset.Nonempty s → s ≠ ∅
ne_empty]
Goals accomplished! 🐙
  ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)·ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_2∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_2∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_3Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)exact Multiset.forall_mem_map_iff: ∀ {α : Type ?u.3527} {β : Type ?u.3528} {f : α → β} {p : β → Prop} {s : Multiset α},
  (∀ (y : β), y ∈ Multiset.map f s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)
Multiset.forall_mem_map_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr hs: ∀ (i : ι), i ∈ s → p (g i)
hs
Goals accomplished! 🐙
  ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)rw [ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_3Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)Multiset.map_map: ∀ {α : Type ?u.3567} {β : Type ?u.3569} {γ : Type ?u.3568} (g : β → γ) (f : α → β) (s : Multiset α),
  Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s
Multiset.map_mapι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_3Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)]ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

refine'_3Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
  ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs_nonempty: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)rfl
Goals accomplished! 🐙
#align finset.le_prod_nonempty_of_submultiplicative_on_pred Finset.le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N)
  (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
    (∀ (x y : M), p x → p y → p (x * y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_nonempty_of_submultiplicative_on_pred
#align finset.le_sum_nonempty_of_subadditive_on_pred Finset.le_sum_nonempty_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N)
  (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
    (∀ (x y : M), p x → p y → p (x + y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_nonempty_of_subadditive_on_pred

/-- Let `{x | p x}` be an additive subsemigroup of an additive commutative monoid `M`. Let
`f : M → N` be a map subadditive on `{x | p x}`, i.e., `p x → p y → f (x + y) ≤ f x + f y`. Let
`g i`, `i ∈ s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∑ i in s, g i) ≤ ∑ i in s, f (g i)`. -/
add_decl_doc le_sum_nonempty_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N)
  (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
    (∀ (x y : M), p x → p y → p (x + y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive_on_pred

/-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∏ i in s, g i) ≤ ∏ i in s, f (g i)`. -/
@[to_additive le_sum_nonempty_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N),
  (∀ (x y : M), f (x + y) ≤ f x + f y) →
    ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive]
theorem le_prod_nonempty_of_submultiplicative: ∀ (f : M → N),
  (∀ (x y : M), f (x * y) ≤ f x * f y) →
    ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative (f: M → N
f : M: Type ?u.3862
M → N: Type ?u.3865
N) (h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul : ∀ x: ?m.3888
x y: ?m.3891
y, f: M → N
f (x: ?m.3888
x * y: ?m.3891
y) ≤ f: M → N
f x: ?m.3888
x * f: M → N
f y: ?m.3891
y)
    {s: Finset ι
s : Finset: Type ?u.6060 → Type ?u.6060
Finset ι: Type ?u.3853
ι} (hs: Finset.Nonempty s
hs : s: Finset ι
s.Nonempty: {α : Type ?u.6063} → Finset α → Prop
Nonempty) (g: ι → M
g : ι: Type ?u.3853
ι → M: Type ?u.3862
M) : f: M → N
f (∏ i: ?m.6104
i in s: Finset ι
s, g: ι → M
g i: ?m.6104
i) ≤ ∏ i: ?m.6126
i in s: Finset ι
s, f: M → N
f (g: ι → M
g i: ?m.6126
i) :=
  le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type ?u.6194} {M : Type ?u.6193} {N : Type ?u.6192} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N]
  (f : M → N) (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
    (∀ (x y : M), p x → p y → p (x * y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative_on_pred f: M → N
f (fun _: ?m.6204
_ ↦ True: Prop
True) (fun x: ?m.6209
x y: ?m.6212
y _: ?m.6215
_ _: ?m.6218
_ ↦ h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul x: ?m.6209
x y: ?m.6212
y)
    (fun _: ?m.6288
_ _: ?m.6291
_ _: ?m.6294
_ _: ?m.6297
_ ↦ trivial: True
trivial) g: ι → M
g s: Finset ι
s hs: Finset.Nonempty s
hs fun _: ?m.6314
_ _: ?m.6317
_ ↦ trivial: True
trivial
#align finset.le_prod_nonempty_of_submultiplicative Finset.le_prod_nonempty_of_submultiplicative: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N),
  (∀ (x y : M), f (x * y) ≤ f x * f y) →
    ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_nonempty_of_submultiplicative
#align finset.le_sum_nonempty_of_subadditive Finset.le_sum_nonempty_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N),
  (∀ (x y : M), f (x + y) ≤ f x + f y) →
    ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_nonempty_of_subadditive

/-- If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y` and `g i`, `i ∈ s`, is a
nonempty finite family of elements of `M`, then `f (∑ i in s, g i) ≤ ∑ i in s, f (g i)`. -/
add_decl_doc le_sum_nonempty_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N),
  (∀ (x y : M), f (x + y) ≤ f x + f y) →
    ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive

/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
such that `f 1 = 1` and `f` is submultiplicative on `{x | p x}`, i.e.,
`p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be a finite family of elements of `M` such
that `∀ i ∈ s, p (g i)`. Then `f (∏ i in s, g i) ≤ ∏ i in s, f (g i)`. -/
@[to_additive le_sum_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N)
  (p : M → Prop),
  f 0 = 0 →
    (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
      (∀ (x y : M), p x → p y → p (x + y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive_on_pred]
theorem le_prod_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N)
  (p : M → Prop),
  f 1 = 1 →
    (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
      (∀ (x y : M), p x → p y → p (x * y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_of_submultiplicative_on_pred (f: M → N
f : M: Type ?u.6433
M → N: Type ?u.6436
N) (p: M → Prop
p : M: Type ?u.6433
M → Prop: Type
Prop) (h_one: f 1 = 1
h_one : f: M → N
f 1: ?m.6464
1 = 1: ?m.6944
1)
    (h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
h_mul : ∀ x: ?m.7462
x y: ?m.7465
y, p: M → Prop
p x: ?m.7462
x → p: M → Prop
p y: ?m.7465
y → f: M → N
f (x: ?m.7462
x * y: ?m.7465
y) ≤ f: M → N
f x: ?m.7462
x * f: M → N
f y: ?m.7465
y) (hp_mul: ∀ (x y : M), p x → p y → p (x * y)
hp_mul : ∀ x: ?m.9455
x y: ?m.9458
y, p: M → Prop
p x: ?m.9455
x → p: M → Prop
p y: ?m.9458
y → p: M → Prop
p (x: ?m.9455
x * y: ?m.9458
y))
    (g: ι → M
g : ι: Type ?u.6424
ι → M: Type ?u.6433
M) {s: Finset ι
s : Finset: Type ?u.9886 → Type ?u.9886
Finset ι: Type ?u.6424
ι} (hs: ∀ (i : ι), i ∈ s → p (g i)
hs : ∀ i: ?m.9890
i ∈ s: Finset ι
s, p: M → Prop
p (g: ι → M
g i: ?m.9890
i)) : f: M → N
f (∏ i: ?m.9956
i in s: Finset ι
s, g: ι → M
g i: ?m.9956
i) ≤ ∏ i: ?m.9978
i in s: Finset ι
s, f: M → N
f (g: ι → M
g i: ?m.9978
i) := by
Goals accomplished! 🐙
  ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)rcases eq_empty_or_nonempty: ∀ {α : Type ?u.10054} (s : Finset α), s = ∅ ∨ Finset.Nonempty s
eq_empty_or_nonempty s: Finset ι
s with (rfl | hs_nonempty): s = ∅ ∨ Finset.Nonempty s
(rfl: s = ∅
rflrfl | hs_nonempty: s = ∅ ∨ Finset.Nonempty s
 | hs_nonempty: Finset.Nonempty s
hs_nonempty(rfl | hs_nonempty): s = ∅ ∨ Finset.Nonempty s
)ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

hs: ∀ (i : ι), i ∈ ∅ → p (g i)

inlf (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s

inrf (∏ i in s, g i) ≤ ∏ i in s, f (g i)
  ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)·ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

hs: ∀ (i : ι), i ∈ ∅ → p (g i)

inlf (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i) ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

hs: ∀ (i : ι), i ∈ ∅ → p (g i)

inlf (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s

inrf (∏ i in s, g i) ≤ ∏ i in s, f (g i)simp [h_one: f 1 = 1
h_one]
Goals accomplished! 🐙
  ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)·ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s

inrf (∏ i in s, g i) ≤ ∏ i in s, f (g i) ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

p: M → Prop

h_one: f 1 = 1

h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y

hp_mul: ∀ (x y : M), p x → p y → p (x * y)

g: ι → M

s: Finset ι

hs: ∀ (i : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s

inrf (∏ i in s, g i) ≤ ∏ i in s, f (g i)exact le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type ?u.11062} {M : Type ?u.11061} {N : Type ?u.11060} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N]
  (f : M → N) (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
    (∀ (x y : M), p x → p y → p (x * y)) →
      ∀ (g : ι → M) (s : Finset ι),
        Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative_on_pred f: M → N
f p: M → Prop
p h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
h_mul hp_mul: ∀ (x y : M), p x → p y → p (x * y)
hp_mul g: ι → M
g s: Finset ι
s hs_nonempty: Finset.Nonempty s
hs_nonempty hs: ∀ (i : ι), i ∈ s → p (g i)
hs
Goals accomplished! 🐙
#align finset.le_prod_of_submultiplicative_on_pred Finset.le_prod_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N)
  (p : M → Prop),
  f 1 = 1 →
    (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
      (∀ (x y : M), p x → p y → p (x * y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_of_submultiplicative_on_pred
#align finset.le_sum_of_subadditive_on_pred Finset.le_sum_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N)
  (p : M → Prop),
  f 0 = 0 →
    (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
      (∀ (x y : M), p x → p y → p (x + y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_of_subadditive_on_pred

/-- Let `{x | p x}` be a subsemigroup of a commutative additive monoid `M`. Let `f : M → N` be a map
such that `f 0 = 0` and `f` is subadditive on `{x | p x}`, i.e. `p x → p y → f (x + y) ≤ f x + f y`.
Let `g i`, `i ∈ s`, be a finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∑ x in s, g x) ≤ ∑ x in s, f (g x)`. -/
add_decl_doc le_sum_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N)
  (p : M → Prop),
  f 0 = 0 →
    (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
      (∀ (x y : M), p x → p y → p (x + y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive_on_pred

/-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y`, `f 1 = 1`, and `g i`,
`i ∈ s`, is a finite family of elements of `M`, then `f (∏ i in s, g i) ≤ ∏ i in s, f (g i)`. -/
@[to_additive le_sum_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N),
  f 0 = 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive]
theorem le_prod_of_submultiplicative: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N),
  f 1 = 1 → (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ (s : Finset ι) (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_of_submultiplicative (f: M → N
f : M: Type ?u.11331
M → N: Type ?u.11334
N) (h_one: f 1 = 1
h_one : f: M → N
f 1: ?m.11358
1 = 1: ?m.11838
1)
    (h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul : ∀ x: ?m.12356
x y: ?m.12359
y, f: M → N
f (x: ?m.12356
x * y: ?m.12359
y) ≤ f: M → N
f x: ?m.12356
x * f: M → N
f y: ?m.12359
y) (s: Finset ι
s : Finset: Type ?u.14342 → Type ?u.14342
Finset ι: Type ?u.11322
ι) (g: ι → M
g : ι: Type ?u.11322
ι → M: Type ?u.11331
M) :
    f: M → N
f (∏ i: ?m.14380
i in s: Finset ι
s, g: ι → M
g i: ?m.14380
i) ≤ ∏ i: ?m.14402
i in s: Finset ι
s, f: M → N
f (g: ι → M
g i: ?m.14402
i) := by
Goals accomplished! 🐙
  ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)refine' le_trans: ∀ {α : Type ?u.14470} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans (Multiset.le_prod_of_submultiplicative: ∀ {α : Type ?u.14781} {β : Type ?u.14782} [inst : CommMonoid α] [inst_1 : OrderedCommMonoid β] (f : α → β),
  f 1 = 1 →
    (∀ (a b : α), f (a * b) ≤ f a * f b) → ∀ (s : Multiset α), f (Multiset.prod s) ≤ Multiset.prod (Multiset.map f s)
Multiset.le_prod_of_submultiplicative f: M → N
f h_one: f 1 = 1
h_one h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul _: Multiset ?m.14783
_) _: ?m.14474 ≤ ?m.14475
_ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
  ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)rw [ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)Multiset.map_map: ∀ {α : Type ?u.14834} {β : Type ?u.14836} {γ : Type ?u.14835} (g : β → γ) (f : α → β) (s : Multiset α),
  Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s
Multiset.map_mapι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)]ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
  ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f: M → N

h_one: f 1 = 1

h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y

s: Finset ι

g: ι → M

f (∏ i in s, g i) ≤ ∏ i in s, f (g i)rfl
Goals accomplished! 🐙
#align finset.le_prod_of_submultiplicative Finset.le_prod_of_submultiplicative: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N),
  f 1 = 1 → (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ (s : Finset ι) (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_of_submultiplicative
#align finset.le_sum_of_subadditive Finset.le_sum_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N),
  f 0 = 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_of_subadditive

/-- If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y`, `f 0 = 0`, and `g i`,
`i ∈ s`, is a finite family of elements of `M`, then `f (∑ i in s, g i) ≤ ∑ i in s, f (g i)`. -/
add_decl_doc le_sum_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N),
  f 0 = 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive

variable {f: ι → N
f g: ι → N
g : ι: Type ?u.15056
ι → N: Type ?u.15068
N} {s: Finset ι
s t: Finset ι
t : Finset: Type ?u.19663 → Type ?u.19663
Finset ι: Type ?u.15056
ι}

/-- In an ordered commutative monoid, if each factor `f i` of one finite product is less than or
equal to the corresponding factor `g i` of another finite product, then
`∏ i in s, f i ≤ ∏ i in s, g i`. -/
@[to_additive sum_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∑ i in s, f i ≤ ∑ i in s, g i
sum_le_sum]
theorem prod_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
prod_le_prod' (h: ∀ (i : ι), i ∈ s → f i ≤ g i
h : ∀ i: ?m.15145
i ∈ s: Finset ι
s, f: ι → N
f i: ?m.15145
i ≤ g: ι → N
g i: ?m.15145
i) : (∏ i: ?m.15478
i in s: Finset ι
s, f: ι → N
f i: ?m.15478
i) ≤ ∏ i: ?m.15542
i in s: Finset ι
s, g: ι → N
g i: ?m.15542
i :=
  Multiset.prod_map_le_prod_map: ∀ {ι : Type ?u.15553} {α : Type ?u.15554} [inst : OrderedCommMonoid α] {s : Multiset ι} (f g : ι → α),
  (∀ (i : ι), i ∈ s → f i ≤ g i) → Multiset.prod (Multiset.map f s) ≤ Multiset.prod (Multiset.map g s)
Multiset.prod_map_le_prod_map f: ι → N
f g: ι → N
g h: ∀ (i : ι), i ∈ s → f i ≤ g i
h
#align finset.prod_le_prod' Finset.prod_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
Finset.prod_le_prod'
#align finset.sum_le_sum Finset.sum_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∑ i in s, f i ≤ ∑ i in s, g i
Finset.sum_le_sum

/-- In an ordered additive commutative monoid, if each summand `f i` of one finite sum is less than
or equal to the corresponding summand `g i` of another finite sum, then
`∑ i in s, f i ≤ ∑ i in s, g i`. -/
add_decl_doc sum_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∑ i in s, f i ≤ ∑ i in s, g i
sum_le_sum

@[to_additive sum_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → 0 ≤ ∑ i in s, f i
sum_nonneg]
theorem one_le_prod': (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
one_le_prod' (h: ∀ (i : ι), i ∈ s → 1 ≤ f i
h : ∀ i: ?m.15714
i ∈ s: Finset ι
s, 1: ?m.15750
1 ≤ f: ι → N
f i: ?m.15714
i) : 1: ?m.16526
1 ≤ ∏ i: ?m.16548
i in s: Finset ι
s, f: ι → N
f i: ?m.16548
i :=
  le_trans: ∀ {α : Type ?u.16611} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans (by
Goals accomplished! 🐙 ι: Type u_1

α: Type ?u.15672

β: Type ?u.15675

M: Type ?u.15678

N: Type u_2

G: Type ?u.15684

k: Type ?u.15687

R: Type ?u.15690

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → 1 ≤ f i

1 ≤ ∏ i in s, 1rw [ι: Type u_1

α: Type ?u.15672

β: Type ?u.15675

M: Type ?u.15678

N: Type u_2

G: Type ?u.15684

k: Type ?u.15687

R: Type ?u.15690

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → 1 ≤ f i

1 ≤ ∏ i in s, 1prod_const_one: ∀ {β : Type ?u.16971} {α : Type ?u.16970} {s : Finset α} [inst : CommMonoid β], ∏ _x in s, 1 = 1
prod_const_oneι: Type u_1

α: Type ?u.15672

β: Type ?u.15675

M: Type ?u.15678

N: Type u_2

G: Type ?u.15684

k: Type ?u.15687

R: Type ?u.15690

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → 1 ≤ f i

1 ≤ 1]
Goals accomplished! 🐙) (prod_le_prod': ∀ {ι : Type ?u.16924} {N : Type ?u.16925} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
prod_le_prod' h: ∀ (i : ι), i ∈ s → 1 ≤ f i
h)
#align finset.one_le_prod' Finset.one_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
Finset.one_le_prod'
#align finset.sum_nonneg Finset.sum_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → 0 ≤ ∑ i in s, f i
Finset.sum_nonneg

@[to_additive Finset.sum_nonneg': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), 0 ≤ f i) → 0 ≤ ∑ i in s, f i
Finset.sum_nonneg']
theorem one_le_prod'': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), 1 ≤ f i) → 1 ≤ ∏ i in s, f i
one_le_prod'' (h: ∀ (i : ι), 1 ≤ f i
h : ∀ i: ι
i : ι: Type ?u.17163
ι, 1: ?m.17212
1 ≤ f: ι → N
f i: ι
i) : 1: ?m.17987
1 ≤ ∏ i: ι
i : ι: Type ?u.17163
ι in s: Finset ι
s, f: ι → N
f i: ι
i :=
  Finset.one_le_prod': ∀ {ι : Type ?u.18071} {N : Type ?u.18072} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
Finset.one_le_prod' fun i: ?m.18119
i _: ?m.18122
_ ↦ h: ∀ (i : ι), 1 ≤ f i
h i: ?m.18119
i
#align finset.one_le_prod'' Finset.one_le_prod'': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), 1 ≤ f i) → 1 ≤ ∏ i in s, f i
Finset.one_le_prod''
#align finset.sum_nonneg' Finset.sum_nonneg': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), 0 ≤ f i) → 0 ≤ ∑ i in s, f i
Finset.sum_nonneg'

@[to_additive sum_nonpos: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ 0) → ∑ i in s, f i ≤ 0
sum_nonpos]
theorem prod_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ 1) → ∏ i in s, f i ≤ 1
prod_le_one' (h: ∀ (i : ι), i ∈ s → f i ≤ 1
h : ∀ i: ?m.18224
i ∈ s: Finset ι
s, f: ι → N
f i: ?m.18224
i ≤ 1: ?m.18260
1) : (∏ i: ?m.19037
i in s: Finset ι
s, f: ι → N
f i: ?m.19037
i) ≤ 1: ?m.19089
1 :=
  (prod_le_prod': ∀ {ι : Type ?u.19111} {N : Type ?u.19112} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
prod_le_prod' h: ∀ (i : ι), i ∈ s → f i ≤ 1
h).trans_eq: ∀ {α : Type ?u.19145} [inst : Preorder α] {a b c : α}, a ≤ b → b = c → a ≤ c
trans_eq (by
Goals accomplished! 🐙 ι: Type u_1

α: Type ?u.18182

β: Type ?u.18185

M: Type ?u.18188

N: Type u_2

G: Type ?u.18194

k: Type ?u.18197

R: Type ?u.18200

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → f i ≤ 1

∏ i in s, 1 = 1rw [ι: Type u_1

α: Type ?u.18182

β: Type ?u.18185

M: Type ?u.18188

N: Type u_2

G: Type ?u.18194

k: Type ?u.18197

R: Type ?u.18200

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → f i ≤ 1

∏ i in s, 1 = 1prod_const_one: ∀ {β : Type ?u.19441} {α : Type ?u.19440} {s : Finset α} [inst : CommMonoid β], ∏ _x in s, 1 = 1
prod_const_oneι: Type u_1

α: Type ?u.18182

β: Type ?u.18185

M: Type ?u.18188

N: Type u_2

G: Type ?u.18194

k: Type ?u.18197

R: Type ?u.18200

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → f i ≤ 1

1 = 1]
Goals accomplished! 🐙)
#align finset.prod_le_one' Finset.prod_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ 1) → ∏ i in s, f i ≤ 1
Finset.prod_le_one'
#align finset.sum_nonpos Finset.sum_nonpos: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ 0) → ∑ i in s, f i ≤ 0
Finset.sum_nonpos

@[to_additive sum_le_sum_of_subset_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 0 ≤ f i) → ∑ i in s, f i ≤ ∑ i in t, f i
sum_le_sum_of_subset_of_nonneg]
theorem prod_le_prod_of_subset_of_one_le': s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le' (h: s ⊆ t
h : s: Finset ι
s ⊆ t: Finset ι
t) (hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
hf : ∀ i: ?m.19686
i ∈ t: Finset ι
t, i: ?m.19686
i ∉ s: Finset ι
s → 1: ?m.19733
1 ≤ f: ι → N
f i: ?m.19686
i) :
    (∏ i: ?m.20516
i in s: Finset ι
s, f: ι → N
f i: ?m.20516
i) ≤ ∏ i: ?m.20574
i in t: Finset ι
t, f: ι → N
f i: ?m.20574
i := by
Goals accomplished! 🐙
  ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 iclassical ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 icalc
      (∏ i: ?m.20604
i in s: Finset ι
s, f: ι → N
f i: ?m.20604
i) ≤ (∏ i: ?m.20879
i in t: Finset ι
t \ s: Finset ι
s, f: ι → N
f i: ?m.20879
i) * ∏ i: ?m.20889
i in s: Finset ι
s, f: ι → N
f i: ?m.20889
i :=
        le_mul_of_one_le_left': ∀ {α : Type ?u.22098} [inst : MulOneClass α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 ≤ b → a ≤ b * a
le_mul_of_one_le_left' <| one_le_prod': ∀ {ι : Type ?u.22515} {N : Type ?u.22516} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
one_le_prod' <| ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 iby
Goals accomplished! 🐙 ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 isimpa only [mem_sdiff: ∀ {α : Type ?u.23412} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s \ t ↔ a ∈ s ∧ ¬a ∈ t
mem_sdiff, and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp]
Goals accomplished! 🐙
      _: ?m✝
_ = ∏ i: ?m.22814
i in t: Finset ι
t \ s: Finset ι
s ∪ s: Finset ι
s, f: ι → N
f i: ?m.22814
i := (prod_union: ∀ {β : Type ?u.22819} {α : Type ?u.22818} {s₁ s₂ : Finset α} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α],
  Disjoint s₁ s₂ → ∏ x in s₁ ∪ s₂, f x = (∏ x in s₁, f x) * ∏ x in s₂, f x
prod_union sdiff_disjoint: ∀ {α : Type ?u.22827} [inst : DecidableEq α] {s t : Finset α}, Disjoint (t \ s) s
sdiff_disjoint).symm: ∀ {α : Sort ?u.23090} {a b : α}, a = b → b = a
symm
      _: ?m✝
_ = ∏ i: ?m.23347
i in t: Finset ι
t, f: ι → N
f i: ?m.23347
i := ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 iby
Goals accomplished! 🐙 ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 irw [ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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 isdiff_union_of_subset: ∀ {α : Type ?u.23793} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₁ ⊆ s₂ → s₂ \ s₁ ∪ s₁ = s₂
sdiff_union_of_subset h: s ⊆ t
hι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

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, f i = ∏ i in t, f i]
Goals accomplished! 🐙
#align finset.prod_le_prod_of_subset_of_one_le' Finset.prod_le_prod_of_subset_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
Finset.prod_le_prod_of_subset_of_one_le'
#align finset.sum_le_sum_of_subset_of_nonneg Finset.sum_le_sum_of_subset_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 0 ≤ f i) → ∑ i in s, f i ≤ ∑ i in t, f i
Finset.sum_le_sum_of_subset_of_nonneg

@[to_additive sum_mono_set_of_nonneg: ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N},
  (∀ (x : ι), 0 ≤ f x) → Monotone fun s => ∑ x in s, f x
sum_mono_set_of_nonneg]
theorem prod_mono_set_of_one_le': (∀ (x : ι), 1 ≤ f x) → Monotone fun s => ∏ x in s, f x
prod_mono_set_of_one_le' (hf: ∀ (x : ι), 1 ≤ f x
hf : ∀ x: ?m.24017
x, 1: ?m.24022
1 ≤ f: ι → N
f x: ?m.24017
x) : Monotone: {α : Type ?u.24796} → {β : Type ?u.24795} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone fun s: ?m.24850
s ↦ ∏ x: ?m.24883
x in s: ?m.24850
s, f: ι → N
f x: ?m.24883
x :=
  fun _: ?m.25180
_ _: ?m.25183
_ hst: ?m.25186
hst ↦ prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.25188} {N : Type ?u.25189} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le' hst: ?m.25186
hst fun x: ?m.25233
x _: ?m.25236
_ _: ?m.25239
_ ↦ hf: ∀ (x : ι), 1 ≤ f x
hf x: ?m.25233
x
#align finset.prod_mono_set_of_one_le' Finset.prod_mono_set_of_one_le': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedCommMonoid N] {f : ι → N},
  (∀ (x : ι), 1 ≤ f x) → Monotone fun s => ∏ x in s, f x
Finset.prod_mono_set_of_one_le'
#align finset.sum_mono_set_of_nonneg Finset.sum_mono_set_of_nonneg: ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N},
  (∀ (x : ι), 0 ≤ f x) → Monotone fun s => ∑ x in s, f x
Finset.sum_mono_set_of_nonneg

@[to_additive sum_le_univ_sum_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι},
  (∀ (x : ι), 0 ≤ f x) → ∑ x in s, f x ≤ ∑ x : ι, f x
sum_le_univ_sum_of_nonneg]
theorem prod_le_univ_prod_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι},
  (∀ (x : ι), 1 ≤ f x) → ∏ x in s, f x ≤ ∏ x : ι, f x
prod_le_univ_prod_of_one_le' [Fintype: Type ?u.25363 → Type ?u.25363
Fintype ι: Type ?u.25319
ι] {s: Finset ι
s : Finset: Type ?u.25366 → Type ?u.25366
Finset ι: Type ?u.25319
ι} (w: ∀ (x : ι), 1 ≤ f x
w : ∀ x: ?m.25370
x, 1: ?m.25375
1 ≤ f: ι → N
f x: ?m.25370
x) :
    (∏ x: ?m.26157
x in s: Finset ι
s, f: ι → N
f x: ?m.26157
x) ≤ ∏ x: ?m.26266
x, f: ι → N
f x: ?m.26266
x :=
  prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.26284} {N : Type ?u.26285} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le' (subset_univ: ∀ {α : Type ?u.26327} [inst : Fintype α] (s : Finset α), s ⊆ univ
subset_univ s: Finset ι
s) fun a: ?m.26336
a _: ?m.26339
_ _: ?m.26342
_ ↦ w: ∀ (x : ι), 1 ≤ f x
w a: ?m.26336
a
#align finset.prod_le_univ_prod_of_one_le' Finset.prod_le_univ_prod_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι},
  (∀ (x : ι), 1 ≤ f x) → ∏ x in s, f x ≤ ∏ x : ι, f x
Finset.prod_le_univ_prod_of_one_le'
#align finset.sum_le_univ_sum_of_nonneg Finset.sum_le_univ_sum_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι},
  (∀ (x : ι), 0 ≤ f x) → ∑ x in s, f x ≤ ∑ x : ι, f x
Finset.sum_le_univ_sum_of_nonneg

-- Porting Note: TODO -- The two next lemmas give the same lemma in additive version
@[to_additive sum_eq_zero_iff_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∑ i in s, f i = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)
sum_eq_zero_iff_of_nonneg]
theorem prod_eq_one_iff_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
prod_eq_one_iff_of_one_le' :
    (∀ i: ?m.26455
i ∈ s: Finset ι
s, 1: ?m.26491
1 ≤ f: ι → N
f i: ?m.26455
i) → ((∏ i: ?m.27270
i in s: Finset ι
s, f: ι → N
f i: ?m.27270
i) = 1: ?m.27322
1 ↔ ∀ i: ?m.27339
i ∈ s: Finset ι
s, f: ι → N
f i: ?m.27339
i = 1: ?m.27371
1) := by
Goals accomplished! 🐙
  ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)classical
    ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)refine Finset.induction_on: ∀ {α : Type ?u.27396} {p : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
  p ∅ → (∀ ⦃a : α⦄ {s : Finset α}, ¬a ∈ s → p s → p (insert a s)) → p s
Finset.induction_on s: Finset ι
s
      (fun _: ?m.27616
_ ↦ ⟨fun _: ?m.27633
_ _: ?m.27636
_ h: ?m.27639
h ↦ False.elim: ∀ {C : Sort ?u.27641}, False → C
False.elim (Finset.not_mem_empty: ∀ {α : Type ?u.27643} (a : α), ¬a ∈ ∅
Finset.not_mem_empty _: ?m.27644
_ h: ?m.27639
h), fun _: ?m.27657
_ ↦ rfl: ∀ {α : Sort ?u.27659} {a : α}, a = a
rfl⟩) ?_: ∀ ⦃a : ι⦄ {s : Finset ι},
  ¬a ∈ s →
    ((∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)) →
      (∀ (i : ι), i ∈ insert a s → 1 ≤ f i) → (∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1)
?_ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

∀ ⦃a : ι⦄ {s : Finset ι},
  ¬a ∈ s →
    ((∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)) →
      (∀ (i : ι), i ∈ insert a s → 1 ≤ f i) → (∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1)
    ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)intro a: ι
a s: Finset ι
s ha: ¬a ∈ s
ha ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ih H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
Hι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
    ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)have : ∀ i: ?m.27718
i ∈ s: Finset ι
s, 1: ?m.27753
1 ≤ f: ι → N
f i: ?m.27718
i := fun _: ?m.28523
_ ↦ H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
H _: ι
_ ∘ mem_insert_of_mem: ∀ {α : Type ?u.28542} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ s → a ∈ insert b s
mem_insert_of_memι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
    ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)rw [ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1prod_insert: ∀ {β : Type ?u.28664} {α : Type ?u.28663} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β]
  [inst_1 : DecidableEq α], ¬a ∈ s → ∏ x in insert a s, f x = f a * ∏ x in s, f x
prod_insert ha: ¬a ∈ s
ha,ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

f a * ∏ x in s, f x = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1 ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1mul_eq_one_iff': ∀ {α : Type ?u.28790} [inst : MulOneClass α] [inst_1 : PartialOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
  [inst_3 : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
  1 ≤ a → 1 ≤ b → (a * b = 1 ↔ a = 1 ∧ b = 1)
mul_eq_one_iff' (H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
H _: ι
_ <| mem_insert_self: ∀ {α : Type ?u.29357} [inst : DecidableEq α] (a : α) (s : Finset α), a ∈ insert a s
mem_insert_self _: ?m.29358
_ _: Finset ?m.29358
_) (one_le_prod': ∀ {ι : Type ?u.29444} {N : Type ?u.29445} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
one_le_prod' this: ∀ (i : ι), i ∈ s → 1 ≤ f i
this),ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

f a = 1 ∧ ∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
      ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1forall_mem_insert: ∀ {α : Type ?u.29637} [inst : DecidableEq α] (a : α) (s : Finset α) (p : α → Prop),
  (∀ (x : α), x ∈ insert a s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
forall_mem_insert,ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

f a = 1 ∧ ∏ i in s, f i = 1 ↔ f a = 1 ∧ ∀ (x : ι), x ∈ s → f x = 1 ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ih this: ∀ (i : ι), i ∈ s → 1 ≤ f i
thisι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i

(f a = 1 ∧ ∀ (i : ι), i ∈ s → f i = 1) ↔ f a = 1 ∧ ∀ (x : ι), x ∈ s → f x = 1]
Goals accomplished! 🐙
#align finset.prod_eq_one_iff_of_one_le' Finset.prod_eq_one_iff_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
Finset.prod_eq_one_iff_of_one_le'
#align finset.sum_eq_zero_iff_of_nonneg Finset.sum_eq_zero_iff_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∑ i in s, f i = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)
Finset.sum_eq_zero_iff_of_nonneg

@[to_additive existing sum_eq_zero_iff_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∑ i in s, f i = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)
sum_eq_zero_iff_of_nonneg]
theorem prod_eq_one_iff_of_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ 1) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
prod_eq_one_iff_of_le_one' :
    (∀ i: ?m.30046
i ∈ s: Finset ι
s, f: ι → N
f i: ?m.30046
i ≤ 1: ?m.30082
1) → ((∏ i: ?m.30856
i in s: Finset ι
s, f: ι → N
f i: ?m.30856
i) = 1: ?m.30908
1 ↔ ∀ i: ?m.30925
i ∈ s: Finset ι
s, f: ι → N
f i: ?m.30925
i = 1: ?m.30957
1) :=
  @prod_eq_one_iff_of_one_le': ∀ {ι : Type ?u.30976} {N : Type ?u.30977} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
prod_eq_one_iff_of_one_le' _: Type ?u.30976
_ N: Type ?u.30012
Nᵒᵈ _ _: ?m.30978 → Nᵒᵈ
_ _: Finset ?m.30978
_
#align finset.prod_eq_one_iff_of_le_one' Finset.prod_eq_one_iff_of_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → f i ≤ 1) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
Finset.prod_eq_one_iff_of_le_one'
-- Porting note: there is no align for the additive version since it aligns to the
-- same one as the previous lemma

@[to_additive single_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∑ x in s, f x
single_le_sum]
theorem single_le_prod': (∀ (i : ι), i ∈ s → 1 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∏ x in s, f x
single_le_prod' (hf: ∀ (i : ι), i ∈ s → 1 ≤ f i
hf : ∀ i: ?m.31102
i ∈ s: Finset ι
s, 1: ?m.31138
1 ≤ f: ι → N
f i: ?m.31102
i) {a: ι
a} (h: a ∈ s
h : a: ?m.31912
a ∈ s: Finset ι
s) : f: ι → N
f a: ?m.31912
a ≤ ∏ x: ?m.31950
x in s: Finset ι
s, f: ι → N
f x: ?m.31950
x :=
  calc
    f: ι → N
f a: ι
a = ∏ i: ?m.32047
i in {a: ι
a}, f: ι → N
f i: ?m.32047
i := prod_singleton: ∀ {β : Type ?u.32117} {α : Type ?u.32116} {a : α} {f : α → β} [inst : CommMonoid β], ∏ x in {a}, f x = f a
prod_singleton.symm: ∀ {α : Sort ?u.32145} {a b : α}, a = b → b = a
symm
    _: ?m✝
_ ≤ ∏ i: ?m.32178
i in s: Finset ι
s, f: ι → N
f i: ?m.32178
i :=
      prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.32456} {N : Type ?u.32457} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le' (singleton_subset_iff: ∀ {α : Type ?u.32490} {s : Finset α} {a : α}, {a} ⊆ s ↔ a ∈ s
singleton_subset_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: a ∈ s
h) fun i: ?m.32511
i hi: ?m.32514
hi _: ?m.32517
_ ↦ hf: ∀ (i : ι), i ∈ s → 1 ≤ f i
hf i: ?m.32511
i hi: ?m.32514
hi
#align finset.single_le_prod' Finset.single_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 1 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∏ x in s, f x
Finset.single_le_prod'
#align finset.single_le_sum Finset.single_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
  (∀ (i : ι), i ∈ s → 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∑ x in s, f x
Finset.single_le_sum

@[to_additive sum_le_card_nsmul: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.sum s f ≤ card s • n
sum_le_card_nsmul]
theorem prod_le_pow_card: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.prod s f ≤ n ^ card s
prod_le_pow_card (s: Finset ι
s : Finset: Type ?u.32708 → Type ?u.32708
Finset ι: Type ?u.32664
ι) (f: ι → N
f : ι: Type ?u.32664
ι → N: Type ?u.32676
N) (n: N
n : N: Type ?u.32676
N) (h: ∀ (x : ι), x ∈ s → f x ≤ n
h : ∀ x: ?m.32718
x ∈ s: Finset ι
s, f: ι → N
f x: ?m.32718
x ≤ n: N
n) :
    s: Finset ι
s.prod: {β : Type ?u.33045} → {α : Type ?u.33044} → [inst : CommMonoid β] → Finset α → (α → β) → β
prod f: ι → N
f ≤ n: N
n ^ s: Finset ι
s.card: {α : Type ?u.33113} → Finset α → ℕ
card := by
Goals accomplished! 🐙
  ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

Finset.prod s f ≤ n ^ card srefine' (Multiset.prod_le_pow_card: ∀ {α : Type ?u.51634} [inst : OrderedCommMonoid α] (s : Multiset α) (n : α),
  (∀ (x : α), x ∈ s → x ≤ n) → Multiset.prod s ≤ n ^ ↑Multiset.card s
Multiset.prod_le_pow_card (s: Finset ι
s.val: {α : Type ?u.51637} → Finset α → Multiset α
val.map: {α : Type ?u.51641} → {β : Type ?u.51640} → (α → β) → Multiset α → Multiset β
map f: ι → N
f) n: N
n _: ∀ (x : ?m.51635), x ∈ Multiset.map f s.val → x ≤ n
_).trans: ∀ {α : Type ?u.51661} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans _: ?m.51672 ≤ ?m.51673
_ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_1∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_2n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
  ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

Finset.prod s f ≤ n ^ card s·ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_1∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_1∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_2n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card ssimpa using h: ∀ (x : ι), x ∈ s → f x ≤ n
h
Goals accomplished! 🐙
  ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

Finset.prod s f ≤ n ^ card s·ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_2n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_2n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card ssimpι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_2n ^ ↑Multiset.card s.val ≤ n ^ card s
    ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n

refine'_2n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card srfl
Goals accomplished! 🐙
#align finset.prod_le_pow_card Finset.prod_le_pow_card: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.prod s f ≤ n ^ card s
Finset.prod_le_pow_card
#align finset.sum_le_card_nsmul Finset.sum_le_card_nsmul: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.sum s f ≤ card s • n
Finset.sum_le_card_nsmul

@[to_additive card_nsmul_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → n ≤ f x) → card s • n ≤ Finset.sum s f
card_nsmul_le_sum]
theorem pow_card_le_prod: ∀ (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → n ≤ f x) → n ^ card s ≤ Finset.prod s f
pow_card_le_prod (s: Finset ι
s : Finset: Type ?u.56335 → Type ?u.56335
Finset ι: Type ?u.56291
ι) (f: ι → N
f : ι: Type ?u.56291
ι → N: Type ?u.56303
N) (n: N
n : N: Type ?u.56303
N) (h: ∀ (x : ι), x ∈ s → n ≤ f x
h : ∀ x: ?m.56345
x ∈ s: Finset ι
s, n: N
n ≤ f: ι → N
f x: ?m.56345
x) :
    n: N
n ^ s: Finset ι
s.card: {α : Type ?u.56674} → Finset α → ℕ
card ≤ s: Finset ι
s.prod: {β : Type ?u.56679} → {α : Type ?u.56678} → [inst : CommMonoid β] → Finset α → (α → β) → β
prod f: ι → N
f := @Finset.prod_le_pow_card: ∀ {ι : Type ?u.75259} {N : Type ?u.75260} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.prod s f ≤ n ^ card s
Finset.prod_le_pow_card _: Type ?u.75259
_ N: Type ?u.56303
Nᵒᵈ _ _: Finset ?m.75261
_ _: ?m.75261 → Nᵒᵈ
_ _: Nᵒᵈ
_ h: ∀ (x : ι), x ∈ s → n ≤ f x
h
#align finset.pow_card_le_prod Finset.pow_card_le_prod: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → n ≤ f x) → n ^ card s ≤ Finset.prod s f
Finset.pow_card_le_prod
#align finset.card_nsmul_le_sum Finset.card_nsmul_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → n ≤ f x) → card s • n ≤ Finset.sum s f
Finset.card_nsmul_le_sum

theorem card_biUnion_le_card_mul: ∀ [inst : DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ),
  (∀ (a : ι), a ∈ s → card (f a) ≤ n) → card (Finset.biUnion s f) ≤ card s * n
card_biUnion_le_card_mul [DecidableEq: Sort ?u.75423 → Sort (max1?u.75423)
DecidableEq β: Type ?u.75385
β] (s: Finset ι
s : Finset: Type ?u.75432 → Type ?u.75432
Finset ι: Type ?u.75379
ι) (f: ι → Finset β
f : ι: Type ?u.75379
ι → Finset: Type ?u.75437 → Type ?u.75437
Finset β: Type ?u.75385
β) (n: ℕ
n : ℕ: Type
ℕ)
    (h: ∀ (a : ι), a ∈ s → card (f a) ≤ n
h : ∀ a: ?m.75443
a ∈ s: Finset ι
s, (f: ι → Finset β
f a: ?m.75443
a).card: {α : Type ?u.75478} → Finset α → ℕ
card ≤ n: ℕ
n) : (s: Finset ι
s.biUnion: {α : Type ?u.75494} → {β : Type ?u.75493} → [inst : DecidableEq β] → Finset α → (α → Finset β) → Finset β
biUnion f: ι → Finset β
f).card: {α : Type ?u.75547} → Finset α → ℕ
card ≤ s: Finset ι
s.card: {α : Type ?u.75554} → Finset α → ℕ
card * n: ℕ
n :=
  card_biUnion_le: ∀ {β : Type ?u.75623} {α : Type ?u.75622} [inst : DecidableEq β] {s : Finset α} {t : α → Finset β},
  card (Finset.biUnion s t) ≤ ∑ a in s, card (t a)
card_biUnion_le.trans: ∀ {α : Type ?u.75707} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| sum_le_card_nsmul: ∀ {ι : Type ?u.75839} {N : Type ?u.75840} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
  (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.sum s f ≤ card s • n
sum_le_card_nsmul _: Finset ?m.75841
_ _: ?m.75841 → ?m.75842
_ _: ?m.75842
_ h: ∀ (a : ι), a ∈ s → card (f a) ≤ n
h
#align finset.card_bUnion_le_card_mul Finset.card_biUnion_le_card_mul: ∀ {ι : Type u_2} {β : Type u_1} [inst : DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ),
  (∀ (a : ι), a ∈ s → card (f a) ≤ n) → card (Finset.biUnion s f) ≤ card s * n
Finset.card_biUnion_le_card_mul

variable {ι': Type ?u.78690
ι' : Type _: Type (?u.76038+1)
Type _} [DecidableEq: Sort ?u.78693 → Sort (max1?u.78693)
DecidableEq ι': Type ?u.75982
ι']

-- Porting note: Mathport warning: expanding binder collection (y «expr ∉ » t)
@[to_additive sum_fiberwise_le_sum_of_sum_fiber_nonneg: ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι']
  {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → 0 ≤ ∑ x in filter (fun x => g x = y) s, f x) →
    ∑ y in t, ∑ x in filter (fun x => g x = y) s, f x ≤ ∑ x in s, f x
sum_fiberwise_le_sum_of_sum_fiber_nonneg]
theorem prod_fiberwise_le_prod_of_one_le_prod_fiber': ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι']
  {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x) →
    ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x ≤ ∏ x in s, f x
prod_fiberwise_le_prod_of_one_le_prod_fiber' {t: Finset ι'
t : Finset: Type ?u.76050 → Type ?u.76050
Finset ι': Type ?u.76038
ι'} {g: ι → ι'
g : ι: Type ?u.75994
ι → ι': Type ?u.76038
ι'} {f: ι → N
f : ι: Type ?u.75994
ι → N: Type ?u.76006
N}
    (h: ∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x
h : ∀ (y: ?m.76062
y) (_: ¬y ∈ t
_ : y: ?m.76062
y ∉ t: Finset ι'
t), (1: ?m.76087
1 : N: Type ?u.76006
N) ≤ ∏ x: ?m.76637
x in s: Finset ι
s.filter: {α : Type ?u.76593} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun x: ?m.76602
x ↦ g: ι → ι'
g x: ?m.76602
x = y: ?m.76062
y, f: ι → N
f x: ?m.76637
x) :
    (∏ y: ?m.76951
y in t: Finset ι'
t, ∏ x: ?m.77018
x in s: Finset ι
s.filter: {α : Type ?u.76981} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun x: ?m.76990
x ↦ g: ι → ι'
g x: ?m.76990
x = y: ?m.76951
y, f: ι → N
f x: ?m.77018
x) ≤ ∏ x: ?m.77030
x in s: Finset ι
s, f: ι → N
f x: ?m.77030
x :=
  calc
    (∏ y: ?m.77056
y in t: Finset ι'
t, ∏ x: ?m.77128
x in s: Finset ι
s.filter: {α : Type ?u.77086} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun x: ?m.77095
x ↦ g: ι → ι'
g x: ?m.77095
x = y: ?m.77056
y, f: ι → N
f x: ?m.77128
x) ≤
        ∏ y: ?m.77368
y in t: Finset ι'
t ∪ s: Finset ι
s.image: {α : Type ?u.77215} → {β : Type ?u.77214} → [inst : DecidableEq β] → (α → β) → Finset α → Finset β
image g: ι → ι'
g, ∏ x: ?m.77435
x in s: Finset ι
s.filter: {α : Type ?u.77398} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun x: ?m.77407
x ↦ g: ι → ι'
g x: ?m.77407
x = y: ?m.77368
y, f: ι → N
f x: ?m.77435
x :=
      prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.77715} {N : Type ?u.77716} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι},
  s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le' (subset_union_left: ∀ {α : Type ?u.77756} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ⊆ s₁ ∪ s₂
subset_union_left _: Finset ?m.77757
_ _: Finset ?m.77757
_) fun y: ?m.77868
y _: ?m.77871
_ ↦ h: ∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x
h y: ?m.77868
y
    _: ?m✝
_ = ∏ x: ?m.77894
x in s: Finset ι
s, f: ι → N
f x: ?m.77894
x :=
      prod_fiberwise_of_maps_to: ∀ {β : Type ?u.77900} {α : Type ?u.77899} {γ : Type ?u.77898} [inst : CommMonoid β] [inst_1 : DecidableEq γ]
  {s : Finset α} {t : Finset γ} {g : α → γ},
  (∀ (x : α), x ∈ s → g x ∈ t) → ∀ (f : α → β), ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x = ∏ x in s, f x
prod_fiberwise_of_maps_to (fun _: ?m.77910
_ hx: ?m.77913
hx ↦ mem_union: ∀ {α : Type ?u.77915} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
mem_union.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr <| mem_image_of_mem: ∀ {α : Type ?u.78018} {β : Type ?u.78019} [inst : DecidableEq β] {s : Finset α} (f : α → β) {a : α},
  a ∈ s → f a ∈ image f s
mem_image_of_mem _: ?m.78020 → ?m.78021
_ hx: ?m.77913
hx) _: ?m.77902 → ?m.77901
_
#align finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber': ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι']
  {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x) →
    ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x ≤ ∏ x in s, f x
Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'
#align finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg: ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι']
  {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → 0 ≤ ∑ x in filter (fun x => g x = y) s, f x) →
    ∑ y in t, ∑ x in filter (fun x => g x = y) s, f x ≤ ∑ x in s, f x
Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg

-- Porting note: Mathport warning: expanding binder collection (y «expr ∉ » t)
@[to_additive sum_le_sum_fiberwise_of_sum_fiber_nonpos: ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι']
  {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → ∑ x in filter (fun x => g x = y) s, f x ≤ 0) →
    ∑ x in s, f x ≤ ∑ y in t, ∑ x in filter (fun x => g x = y) s, f x
sum_le_sum_fiberwise_of_sum_fiber_nonpos]
theorem prod_le_prod_fiberwise_of_prod_fiber_le_one': ∀ {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → ∏ x in filter (fun x => g x = y) s, f x ≤ 1) →
    ∏ x in s, f x ≤ ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x
prod_le_prod_fiberwise_of_prod_fiber_le_one' {t: Finset ι'
t : Finset: Type ?u.78702 → Type ?u.78702
Finset ι': Type ?u.78690
ι'} {g: ι → ι'
g : ι: Type ?u.78646
ι → ι': Type ?u.78690
ι'} {f: ι → N
f : ι: Type ?u.78646
ι → N: Type ?u.78658
N}
    (h: ∀ (y : ι'), ¬y ∈ t → ∏ x in filter (fun x => g x = y) s, f x ≤ 1
h : ∀ (y: ?m.78714
y) (_: ¬y ∈ t
_ : y: ?m.78714
y ∉ t: Finset ι'
t), (∏ x: ?m.78786
x in s: Finset ι
s.filter: {α : Type ?u.78742} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun x: ?m.78751
x ↦ g: ι → ι'
g x: ?m.78751
x = y: ?m.78714
y, f: ι → N
f x: ?m.78786
x) ≤ 1: ?m.78855
1) :
    (∏ x: ?m.79615
x in s: Finset ι
s, f: ι → N
f x: ?m.79615
x) ≤ ∏ y: ?m.79625
y in t: Finset ι'
t, ∏ x: ?m.79692
x in s: Finset ι
s.filter: {α : Type ?u.79655} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter fun x: ?m.79664
x ↦ g: ι → ι'
g x: ?m.79664
x = y: ?m.79625
y, f: ι → N
f x: ?m.79692
x :=
  @prod_fiberwise_le_prod_of_one_le_prod_fiber': ∀ {ι : Type ?u.79712} {N : Type ?u.79711} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type ?u.79710}
  [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x) →
    ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x ≤ ∏ x in s, f x
prod_fiberwise_le_prod_of_one_le_prod_fiber' _: Type ?u.79712
_ N: Type ?u.78658
Nᵒᵈ _ _: Finset ?m.79713
_ _: Type ?u.79710
_ _ _: Finset ?m.79717
_ _: ?m.79713 → ?m.79717
_ _: ?m.79713 → Nᵒᵈ
_ h: ∀ (y : ι'), ¬y ∈ t → ∏ x in filter (fun x => g x = y) s, f x ≤ 1
h
#align finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one': ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι']
  {t : Finset ι'} {g : ι → ι'} {f :