case empty
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s → f i ≤ g i
h0 : ∀ (i : ι), i ∈ ∅ → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ ∅ → f i ≤ g i
⊢ ∏ i in ∅, f i ≤ ∏ i in ∅, g i

case insert
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in insert a s, f i ≤ ∏ i in insert a s, g i
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ ∏ i in s, f i ≤ ∏ i in s, g i
induction' s using Finset.induction with a s has ih h
no goals
case empty
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s → f i ≤ g i
h0 : ∀ (i : ι), i ∈ ∅ → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ ∅ → f i ≤ g i
⊢ ∏ i in ∅, f i ≤ ∏ i in ∅, g i
simp
case insert
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ f a * ∏ i in s, f i ≤ g a * ∏ i in s, g i
case insert
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in insert a s, f i ≤ ∏ i in insert a s, g i
simp only [prod_insert has]
case insert.h₁
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ f a ≤ g a

case insert.h₂
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in s, f i ≤ ∏ i in s, g i

case insert.c0
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ 0 ≤ ∏ i in s, f i

case insert.b0
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ 0 ≤ g a
case insert
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ f a * ∏ i in s, f i ≤ g a * ∏ i in s, g i
apply mul_le_mul
no goals
case insert.h₁
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ f a ≤ g a
exact h1 a (mem_insert_self a s)
no goals
case insert.h₂
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in s, f i ≤ ∏ i in s, g i
refine ih (fun x H ↦ h0 _ ?_) (fun x H ↦ h1 _ ?_) <;> exact mem_insert_of_mem H
no goals
case insert.c0
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ 0 ≤ ∏ i in s, f i
apply prod_nonneg fun x H ↦ h0 x (mem_insert_of_mem H)
no goals
case insert.b0
ι : Type u_1
α : Type ?u.149270
β : Type ?u.149273
M : Type ?u.149276
N : Type ?u.149279
G : Type ?u.149282
k : Type ?u.149285
R : Type u_2
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ 0 ≤ g a
apply le_trans (h0 a (mem_insert_self a s)) (h1 a (mem_insert_self a s))