awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ 0 ≤ f i

Tactic:
hf i hi
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ 0 ≤ f i

Tactic:
exact hf i hi
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ≤ ∑ i ∈ s, f i

Tactic:
single_le_sum hf hi

Premises used: Finset.single_le_sum
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ≤ ∑ i ∈ s, f i

Tactic:
exact single_le_sum hf hi

Premises used: Finset.single_le_sum
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i

Tactic:
simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]

Premises used: Finset.prod_eq_mul_prod_diff_singleton_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i

Tactic:
le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)

Premises used: mul_le_mul_of_nonneg_right, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
refine_2 : LE.le.{u_2} (α := R) 0 (∏ i ∈ s \ {i}, f i)
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i

Tactic:
refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)

Premises used: mul_le_mul_of_nonneg_right, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i

Tactic:
rw [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : 0 ≤ g i
refine_1₁ : ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1
refine_1₂ : ∀ (j : ι) (hj : j ∈ s \ {i}), g j ≤ f j
refine_1₃ : 0 ≤ h i
refine_1₄ : ∀ i_1 ∈ s \ {i}, 0 ≤ h i_1
refine_1₅ : ∀ i_1 ∈ s \ {i}, h i_1 ≤ f i_1
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
gcongr with j hj
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 0 ≤ g i

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 0 ≤ h i

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s \ {i}, 0 ≤ h i_1

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
i_1 : ι
h_1 : i_1 ∈ s \ {i}
⊢ h i_1 ≤ f i_1

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_2 : ∀ i_1 ∈ s \ {i}, 0 ≤ f i_1
⊢ LE.le.{u_2} (α := R) 0 (∏ i ∈ s \ {i}, f i)

Tactic:
apply prod_nonneg

Premises used: Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_2 : ∀ i_1 ∈ s, ¬i_1 = i → 0 ≤ f i_1
⊢ ∀ i_1 ∈ s \ {i}, 0 ≤ f i_1

Tactic:
simp only [and_imp, mem_sdiff, mem_singleton]

Premises used: Finset.mem_singleton, and_imp, Finset.mem_sdiff
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s, ¬i_1 = i → 0 ≤ f i_1

Tactic:
fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

Premises used: le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s, ¬i_1 = i → 0 ≤ f i_1

Tactic:
exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

Premises used: le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
refine_2 refine_2₁ : LE.le.{u_2} (α := R) 0 (∏ i ∈ s \ {i}, f i)
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i

Tactic:
classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

Premises used: Finset.mem_singleton, and_imp, Finset.mem_sdiff, mul_le_mul_of_nonneg_right, right_distrib, Finset.prod_nonneg, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
⊢ (Multiset.map f (Multiset.map (fun (i : ι) ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
simp [Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
apply : ∀ (a : M), Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a → p a
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
apply le_trans (Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg f p h_nonneg h_one
    h_mul hp_mul _ ?_) (by simp [Multiset.map_map])

Premises used: Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
a : M
ha : Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a
obtain :
  ∀ (i : ι) (hi : i ∈ s.val) (ha : Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) (g i)),
    p (g i)
⊢ p a

Tactic:
obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp ha

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
i : ι
hi : i ∈ s.val
ha : Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) (g i)
⊢ p (g i)

Tactic:
hps i hi
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
i : ι
hi : i ∈ s.val
ha : Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) (g i)
⊢ p (g i)

Tactic:
exact hps i hi
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map f (Multiset.map (fun (i : ι) ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
simp [Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f : ι → R
rw : (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0
⊢ Eq.{u_2 + 1} (α := R) (∑ i ∈ s, f i * f i) 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]

Premises used: mul_self_nonneg, Finset.sum_eq_zero_iff_of_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
s : Finset ι
f : ι → R
⊢ Eq.{u_2 + 1} (α := R) |∏ x ∈ s, f x| (∏ x ∈ s, |f x|)

Tactic:
map_prod absHom _ _

Premises used: abs, map_prod, absHom
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_4
f : ι → ℕ+
s : Finset ι
⊢ (↑(∏ i ∈ s, f i) : ℕ) = ∏ i ∈ s, (↑(f i) : ℕ)

Tactic:
map_prod PNat.coeMonoidHom _ _

Premises used: PNat.val, PNat.coeMonoidHom, map_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f : ι → R
s : Finset ι
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
⊢ LT.lt.{u_2} (α := R) 0 (∏ i ∈ s, f i) ↔ ∀ i ∈ s, 0 < f i

Tactic:
CanonicallyOrderedAdd.multiset_prod_pos.trans Multiset.forall_mem_map_iff

Premises used: CanonicallyOrderedAdd.multiset_prod_pos, Finset.prod, Iff.trans, Multiset.forall_mem_map_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i

Tactic:
simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]

Premises used: Finset.prod_eq_mul_prod_diff_singleton_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
grw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i

Tactic:
grw [← h2i, right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
h₁ : ∀ (j : ι) (hj : j ∈ s \ {i}), g j ≤ f j
h₂ : ∀ (j : ι) (hj : j ∈ s \ {i}), h j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
gcongr with j hj j hj
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ g j ≤ f j

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
j : ι
hj : j ∈ s \ {i}
⊢ h j ≤ f j

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
simp_rw₁ : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i

Tactic:
classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  grw [← h2i, right_distrib]
  gcongr with j hj j hj <;> simp_all

Premises used: right_distrib
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
inl :
  ∀ (h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0),
    HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
inr :
  ∀ (h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)),
    HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
obtain h | h := (sum_nonneg hg).eq_or_lt'

Premises used: Finset.sum_nonneg, LE.le.eq_or_lt'
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0
i : ι
hi : i ∈ s
⊢ r i = 0

Tactic:
simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Iff.mp
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ i ∈ s, r i) 0

Tactic:
have ht' : ∑ i ∈ s, r i = 0 := sum_eq_zero fun i hi ↦ by
      simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0
ht' : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, r i) 0
inl : HPow.hPow (α := R) (β := ℕ) 0 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) 0
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
rw [h, ht']
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0
ht' : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, r i) 0
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h

Premises used: le_of_add_le_add_left, le_of_mul_le_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
inr :
  (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
refine le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h

Premises used: le_of_add_le_add_left, le_of_mul_le_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
simp_rw :
  (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
    2 * ((∑ i ∈ s, r i) * HMul.hMul (α := R) (∑ i ∈ s, g i) (∑ i ∈ s, r i))
⊢ (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j

Tactic:
simp_rw [mul_assoc, ← mul_sum, ← sum_mul]

Premises used: Finset.mul_sum, mul_assoc, Finset.sum_mul
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
    2 * ((∑ i ∈ s, r i) * HMul.hMul (α := R) (∑ i ∈ s, g i) (∑ i ∈ s, r i))

Tactic:
ring