no goals
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i
classical
  simp_rw [prod_eq_mul_prod_diff_singleton hi]
  refine' le_trans _ (mul_le_mul_right' h2i _)
  rw [right_distrib]
  apply add_le_add <;> apply mul_le_mul_left' <;> apply prod_le_prod' <;>
          simp only [and_imp, mem_sdiff, mem_singleton] <;>
        intros <;>
      apply_assumption <;>
    assumption
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i
simp_rw [prod_eq_mul_prod_diff_singleton hi]
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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_right' h2i _)
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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]
no goals
ι : Type u_1
α : Type ?u.177392
β : Type ?u.177395
M : Type ?u.177398
N : Type ?u.177401
G : Type ?u.177404
k : Type ?u.177407
R : Type u_2
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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
apply add_le_add <;> apply mul_le_mul_left' <;> apply prod_le_prod' <;>
        simp only [and_imp, mem_sdiff, mem_singleton] <;>
      intros <;>
    apply_assumption <;>
  assumption