ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ f i * ∏ i in s \ {i}, f i
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i
simp_rw [prod_eq_mul_prod_diff_singleton hi]
case refine_1
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ (g i + h i) * ∏ i in s \ {i}, f i

case refine_2
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ ∏ i in s \ {i}, f i
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ f i * ∏ i in s \ {i}, f i
refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
case refine_1
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ g i * ∏ i in s \ {i}, f i + h i * ∏ i in s \ {i}, f i
case refine_1
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ (g i + h i) * ∏ i in s \ {i}, f i
rw [right_distrib]
case refine_1.refine_2.refine_1
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∏ i in s \ {i}, h i ≤ ∏ i in s \ {i}, f i

case refine_1.refine_2.refine_2
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ h i
case refine_1.refine_2
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ h i * ∏ i in s \ {i}, h i ≤ h i * ∏ i in s \ {i}, f i
refine mul_le_mul_of_nonneg_left ?_ ?_
no goals
case refine_1.refine_2.refine_1
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∏ i in s \ {i}, h i ≤ ∏ i in s \ {i}, f i
refine prod_le_prod ?_ ?_
<;> simp (config := { contextual := true }) [*]
case refine_1.refine_2.refine_2.a
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
case refine_1.refine_2.refine_2
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ h i
try apply_assumption
no goals
case refine_1.refine_2.refine_2.a
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
try assumption
case refine_1.refine_2.refine_2.a
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
case refine_1.refine_2.refine_2
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ h i
apply_assumption
no goals
case refine_1.refine_2.refine_2.a
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
assumption
case refine_2.h0
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → 0 ≤ f i_1
case refine_2
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ ∏ i in s \ {i}, f i
apply prod_nonneg
case refine_2.h0
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s → ¬i_1 = i → 0 ≤ f i_1
case refine_2.h0
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → 0 ≤ f i_1
simp only [and_imp, mem_sdiff, mem_singleton]
case refine_2.h0
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
j : ι
h1j : j ∈ s
h2j : ¬j = i
⊢ 0 ≤ f j
case refine_2.h0
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s → ¬i_1 = i → 0 ≤ f i_1
intro j h1j h2j
no goals
case refine_2.h0
ι : Type u_1
α : Type ?u.156140
β : Type ?u.156143
M : Type ?u.156146
N : Type ?u.156149
G : Type ?u.156152
k : Type ?u.156155
R : Type u_2
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
j : ι
h1j : j ∈ s
h2j : ¬j = i
⊢ 0 ≤ f j
exact le_trans (hg j h1j) (hgf j h1j h2j)