-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
/-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod'` for
the case of an ordered commutative multiplicative monoid. -/
@[gcongr]
lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
    ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Proof state:
case cons
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i

Tactic:
gcongr

Result:
case cons.c0
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ 0 ≤ ∏ i ∈ s, f i

case cons.b0
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ 0 ≤ g a

case cons.h₁
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ f a ≤ g a

case cons.h₂
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Proof state:
case cons
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›

Result:
case cons
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i

Proof state:
case empty
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ ∅, 0 ≤ f i
h1 : ∀ i ∈ ∅, f i ≤ g i
⊢ ∏ i ∈ ∅, f i ≤ ∏ i ∈ ∅, g i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons a s has ih =>
  simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
  have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
  gcongr
  exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

Result:
no goals

Proof state:
case cons
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : ∀ i ∈ cons a s has, 0 ≤ f i
h1 : ∀ i ∈ cons a s has, f i ≤ g i
⊢ ∏ i ∈ cons a s has, f i ≤ ∏ i ∈ cons a s has, g i

Tactic:
simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢

Result:
case cons
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i

Proof state:
case cons.c0
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ 0 ≤ ∏ i ∈ s, f i

case cons.b0
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ 0 ≤ g a

case cons.h₁
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ f a ≤ g a

case cons.h₂
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f g : ι → R
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]

Result:
no goals