awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 < f i
⊢ LT.lt.{u_2} (α := R) 0 (∏ i ∈ s, f i)

Tactic:
prod_induction f (fun x ↦ 0 < x) (fun _ _ ha hb ↦ mul_pos ha hb) zero_lt_one h0

Premises used: Finset.prod_induction, zero_lt_one, mul_pos, LT.lt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
obtain : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
obtain ⟨i, hi, hilt⟩ := hlt
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
rw : f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]

Premises used: Finset.prod_insert, Finset.notMem_erase, Finset.insert_erase
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
⊢ MulPosStrictMono R

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x

Tactic:
mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_

Premises used: mul_lt_mul_of_pos_of_nonneg'
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
refine_1 : LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
refine_2 : LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
refine_3 : 0 ≤ g i
⊢ f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x

Tactic:
refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_

Premises used: mul_lt_mul_of_pos_of_nonneg'
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)

Tactic:
prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)

Premises used: Finset.prod_le_prod, le_of_lt, Finset.mem_of_mem_erase
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)

Tactic:
exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)

Premises used: Finset.prod_le_prod, le_of_lt, Finset.mem_of_mem_erase
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)

Tactic:
prod_pos fun j hj => hf j (mem_of_mem_erase hj)

Premises used: Finset.mem_of_mem_erase, Finset.prod_pos
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)

Tactic:
exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)

Premises used: Finset.mem_of_mem_erase, Finset.prod_pos
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i

Tactic:
(hf i hi).le.trans hilt.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i

Tactic:
exact (hf i hi).le.trans hilt.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
obtain : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
obtain₁ : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
obtain₂ :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R),
    f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
refine_1 :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R),
    LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
refine_2 :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
refine_3 : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), 0 ≤ g i
refine_2₁ :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
refine_3₁ refine_3₂ : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), 0 ≤ g i
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
classical
  obtain ⟨i, hi, hilt⟩ := hlt
  rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
  · exact (hf i hi).le.trans hilt.le

Premises used: Finset.prod_insert, Finset.notMem_erase
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
apply : ∃ i ∈ s, f i < g i
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)

Premises used: le_of_lt, Finset.prod_lt_prod
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
obtain : ∀ (i : ι) (hi : i ∈ s), ∃ i ∈ s, f i < g i
⊢ ∃ i ∈ s, f i < g i

Tactic:
obtain ⟨i, hi⟩ := h_ne
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i ∈ s, f i < g i

Tactic:
⟨i, hi, hfg i hi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i ∈ s, f i < g i

Tactic:
exact ⟨i, hi, hfg i hi⟩
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 ≤ a
⊢ LE.le.{u_1} (α := R) 0 (prod [])

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
cons : 0 ≤ head * tail.prod
⊢ 0 ≤ (head :: tail).prod

Tactic:
simp only [prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ head ∧ ∀ (a : R), a ∈ tail → 0 ≤ a

Tactic:
simp only [mem_cons, forall_eq_or_imp] at h

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod
h : 0 ≤ head ∧ ∀ (a : R), a ∈ tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod

Tactic:
mul_nonneg h.1 (hind h.2)

Premises used: mul_nonneg, And.right, And.left
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod
h : 0 ≤ head ∧ ∀ (a : R), a ∈ tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod

Tactic:
exact mul_nonneg h.1 (hind h.2)

Premises used: mul_nonneg, And.right, And.left
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 0 ≤ a
nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 ≤ a), LE.le.{u_1} (α := R) 0 (prod [])
cons :
  ∀ (head : R) (tail : List R) (hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod)
    (h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a), 0 ≤ (head :: tail).prod
⊢ 0 ≤ s.prod

Tactic:
induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)

Premises used: List.head, forall_eq_or_imp, List.tail, List.cons, List.mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
h : ∀ (a : R), Membership.mem (γ := List R) [] a → 1 ≤ a
⊢ LE.le.{u_1} (α := R) 1 (prod [])

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
cons : 1 ≤ head * tail.prod
⊢ 1 ≤ (head :: tail).prod

Tactic:
simp only [prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
⊢ 1 ≤ head ∧ ∀ (a : R), a ∈ tail → 1 ≤ a

Tactic:
simp only [mem_cons, forall_eq_or_imp] at h

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod
h : 1 ≤ head ∧ ∀ (a : R), a ∈ tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod

Tactic:
one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

Premises used: And.right, And.left, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod
h : 1 ≤ head ∧ ∀ (a : R), a ∈ tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod

Tactic:
exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

Premises used: And.right, And.left, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 1 ≤ a
nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 1 ≤ a), LE.le.{u_1} (α := R) 1 (prod [])
cons :
  ∀ (head : R) (tail : List R) (hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod)
    (h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a), 1 ≤ (head :: tail).prod
⊢ 1 ≤ s.prod

Tactic:
induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

Premises used: List.head, forall_eq_or_imp, List.tail, List.cons, List.mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
h0 : ∀ (i : ι), Membership.mem (γ := List ι) [] i → 0 ≤ f i
h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i
⊢ (map f []).prod ≤ (map g []).prod

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
cons : f a * (map f s).prod ≤ g a * (map g s).prod
⊢ (map f (a :: s)).prod ≤ (map g (a :: s)).prod

Tactic:
simp only [map_cons, prod_cons]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
⊢ MulPosMono R

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
cons : f a ≤ g a
cons₁ : (map f s).prod ≤ (map g s).prod
cons₂ : 0 ≤ (map f s).prod
cons₃ : 0 ≤ g a
⊢ f a * (map f s).prod ≤ g a * (map g s).prod

Tactic:
apply mul_le_mul

Premises used: mul_le_mul
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
cons : a ∈ a :: s
⊢ f a ≤ g a

Tactic:
apply h
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ (map f s).prod

Tactic:
grind [prod_nonneg]

Premises used: List.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
apply apply₁ : a ∈ a :: s
⊢ 0 ≤ g a

Tactic:
apply (h0 _ _).trans (h _ _)

Premises used: LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ a ∈ a :: s

Tactic:
simp only [mem_cons, true_or]

Premises used: true_or, List.mem_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
s : List ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
nil :
  ∀ (h0 : ∀ (i : ι), Membership.mem (γ := List ι) [] i → 0 ≤ f i)
    (h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i), (map f []).prod ≤ (map g []).prod
cons :
  ∀ (a : ι) (s : List ι)
    (hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod)
    (h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i),
    (map f (a :: s)).prod ≤ (map g (a :: s)).prod
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
induction s with
  | nil => simp
  | cons a s hind =>
    simp only [map_cons, prod_cons]
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    apply mul_le_mul
    · apply h
      simp
    · grind
    · grind [prod_nonneg]
    · apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]

Premises used: List.map_cons, true_or, List.cons, mul_le_mul, LE.le.trans, List.mem_cons, List.prod_cons, List.nil, List.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
F : Type u_2
L : Type u_3
inst_4 : FunLike F L R
f : F
r : R
t : List L
hf0 : ∀ (x : L), x ∈ t → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R)
hf : ∀ (x : L), x ∈ t → (f : (a : L) → R) x ≤ r
⊢ prod (map (⇑f : (a : L) → R) t) ≤ (map (Function.const L r) t).prod

Tactic:
prod_map_le_prod_map₀ f (Function.const L r) hf0 hf

Premises used: Function.const, List.prod_map_le_prod_map₀, DFunLike.coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
F : Type u_2
L : Type u_3
inst_4 : FunLike F L R
f : F
r : R
t : List L
hf0 : ∀ (x : L), x ∈ t → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R)
hf : ∀ (x : L), x ∈ t → (f : (a : L) → R) x ≤ r
h : r ^ t.length = (map (Function.const L r) t).prod
⊢ prod (map (⇑f : (a : L) → R) t) ≤ r ^ t.length

Tactic:
convert! prod_map_le_prod_map₀ f (Function.const L r) hf0 hf

Premises used: Function.const, List.prod_map_le_prod_map₀, DFunLike.coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
F : Type u_2
L : Type u_3
inst_4 : FunLike F L R
f : F
r : R
t : List L
hf0 : ∀ (x : L), x ∈ t → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R)
hf : ∀ (x : L), x ∈ t → (f : (a : L) → R) x ≤ r
⊢ r ^ t.length = (map (Function.const L r) t).prod

Tactic:
simp [map_const, prod_replicate]

Premises used: List.map_const, List.prod_replicate
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 < a
⊢ LT.lt.{u_1} (α := R) 0 (prod [])

Tactic:
simp