awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
s : Multiset α
⊢ |s.sum| ≤ (map abs s).sum

Tactic:
le_sum_of_subadditive _ abs_zero.le abs_add_le s

Premises used: Multiset.le_sum_of_subadditive
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
m : Multiset α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
l : List α
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).sum

Tactic:
simp [l.apply_prod_le_sum_map _ h_one h_mul]

Premises used: List.apply_prod_le_sum_map
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
m : Multiset α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
h : ∀ (l : List α), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).sum
⊢ f m.prod ≤ (map f m).sum

Tactic:
induction m using Quotient.inductionOn with
  | h l => simp [l.apply_prod_le_sum_map _ h_one h_mul]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
m : Multiset α
f : α → β
h_one : 0 ≤ f 1
h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)
⊢ (map f m).sum ≤ f m.prod

Tactic:
m.apply_prod_le_sum_map (β := βᵒᵈ) f h_one h_mul

Premises used: Multiset.apply_prod_le_sum_map, OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
⊢ LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)

Tactic:
prod_induction f (fun i ↦ 0 ≤ i) (fun _ _ ha hb ↦ mul_nonneg ha hb) zero_le_one h0

Premises used: mul_nonneg, LE.le, zero_le_one, Finset.prod_induction, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ f i
h1 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≤ g i
⊢ LE.le.{u_2} (α := R) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : ∀ i ∈ Finset.cons a s has, 0 ≤ f i
h1 : ∀ i ∈ Finset.cons a s has, f i ≤ g i
cons :
  ∀ (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
⊢ LE.le.{u_2} (α := R) (∏ i ∈ Finset.cons a s has, f i) (∏ i ∈ Finset.cons a s has, g i)

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

Premises used: Finset.forall_mem_cons, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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
⊢ MulPosMono R

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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
cons : LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)
cons₁ : 0 ≤ g a
cons₂ : f a ≤ g a
cons₃ : LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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
⊢ LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)

Tactic:
prod_nonneg h0.2

Premises used: And.right, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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

Tactic:
h0.1.trans h1.1

Premises used: And.left, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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

Tactic:
h1.1

Premises used: And.left
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
ih h0.2 h1.2

Premises used: And.right
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ 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
⊢ LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)

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

Premises used: And.right, And.left, LE.le.trans, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ g i
empty :
  ∀ (h0 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ f i)
    (h1 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)
cons :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i))
    (h0 : ∀ i ∈ Finset.cons a s has, 0 ≤ f i) (h1 : ∀ i ∈ Finset.cons a s has, f i ≤ g i),
    LE.le.{u_2} (α := R) (∏ i ∈ Finset.cons a s has, f i) (∏ i ∈ Finset.cons a s has, g i)
⊢ LE.le.{u_2} (α := R) (∏ 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]

Premises used: Finset.cons, Finset.forall_mem_cons, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, 1)

Tactic:
prod_le_prod h0 h1

Premises used: Finset.prod_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
h : Eq.{u_2 + 1} (α := R) (∏ i ∈ s, 1) 1
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) 1

Tactic:
convert! ← prod_le_prod h0 h1

Premises used: Finset.prod_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ s, 1) 1

Tactic:
Finset.prod_const_one

Premises used: Finset.prod_const_one
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ s, 1) 1

Tactic:
exact Finset.prod_const_one

Premises used: Finset.prod_const_one
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 1 ≤ f i
⊢ ∀ i ∈ s, LE.le.{u_2} (α := R) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 1 ≤ f i
⊢ LE.le.{u_2} (α := R) 1 (∏ i ∈ s, f i)

Tactic:
simpa using prod_le_prod (by simp) hf

Premises used: Finset.prod_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
inr : ∀ (hf : 0 ≤ f i), f i ≤ ∏ i ∈ s, max (f i) 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
rcases lt_or_ge (f i) 0 with hf | hf

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : f i < 0
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
(hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le

Premises used: LT.lt.le, zero_le_one, LT.lt.trans_le, le_sup_of_le_right, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : f i < 0
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le

Premises used: LT.lt.le, zero_le_one, LT.lt.trans_le, le_sup_of_le_right, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
x : ι
h : x ∈ s
h_1 : x ≠ i
⊢ (if i = x then f i else 1) = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
rw : f i = if i = i then f i else 1
⊢ f i = ∏ j ∈ s, if i = j then f i else 1

Tactic:
rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]

Premises used: Finset.prod_eq_single_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
⊢ f i = if i = i then f i else 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
⊢ f i = ∏ j ∈ s, if i = j then f i else 1

Tactic:
have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
this : f i = ∏ j ∈ s, if i = j then f i else 1
x : ι
h : x ∈ s
⊢ 0 ≤ if i = x then f i else 1

Tactic:
grind [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
this : f i = ∏ j ∈ s, if i = j then f i else 1
x : ι
h : x ∈ s
⊢ (if i = x then f i else 1) ≤ max (f x) 1

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
this : f i = ∏ j ∈ s, if i = j then f i else 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
inr inr₁ : ∀ (hf : 0 ≤ f i), f i ≤ ∏ i ∈ s, max (f i) 1
inr₂ : ∀ (hf : 0 ≤ f i) (this : f i = ∏ j ∈ s, if i = j then f i else 1), f i ≤ ∏ i ∈ s, max (f i) 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
classical
  rcases lt_or_ge (f i) 0 with hf | hf
  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ MulPosMono R

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ ∀ i ∈ t \ s, 1 ≤ f i

Tactic:
simpa only [mem_sdiff, and_imp]

Premises used: and_imp, Finset.mem_sdiff
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ HMul.hMul (α := R) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = ∏ i ∈ t \ s ∪ s, f i

Tactic:
(prod_union sdiff_disjoint).symm

Premises used: Finset.prod_union, Eq.symm, Finset.sdiff_disjoint
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
rw rw₁ : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t, f i)
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)

Tactic:
rw [sdiff_union_of_subset h]

Premises used: Finset.sdiff_union_of_subset
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ t, f i)

Tactic:
calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]

Premises used: le_mul_of_one_le_left, Finset.prod_union, Finset.prod, SDiff.sdiff, Finset.one_le_prod, Eq.symm, Finset.sdiff_disjoint, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ t, f i)

Tactic:
classical
  calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]

Premises used: le_mul_of_one_le_left, Finset.prod_union, Finset.one_le_prod, Eq.symm, Finset.sdiff_disjoint, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
⊢ MulPosMono R

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
rw rw₁ : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t, f i)
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t \ s ∪ s, f i)

Tactic:
rw [sdiff_union_of_subset h]

Premises used: Finset.sdiff_union_of_subset
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∏ i ∈ t \ s ∪ s, f i = HMul.hMul (α := R) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i)

Tactic:
prod_union sdiff_disjoint

Premises used: Finset.prod_union, Finset.sdiff_disjoint
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∀ i ∈ s, 0 ≤ f i

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∀ i ∈ t \ s, 0 ≤ f i

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∀ i ∈ t \ s, f i ≤ 1

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t \ s ∪ s, f i)
⊢ LE.le.{u_2} (α := R) (∏ i ∈ t, f i) (∏ i ∈ s, f i)

Tactic:
calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))

Premises used: Finset.prod_le_one, Finset.prod_union, Finset.prod, SDiff.sdiff, mul_le_of_le_one_left, Finset.sdiff_disjoint, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t \ s ∪ s, f i)
⊢ LE.le.{u_2} (α := R) (∏ i ∈ t, f i) (∏ i ∈ s, f i)

Tactic:
classical
  calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))

Premises used: Finset.prod_le_one, Finset.prod_union, mul_le_of_le_one_left, Finset.sdiff_disjoint, Finset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
hf : ∀ (x : ι), 1 ≤ f x
⊢ Monotone.{u_1, u_2} (β := R) fun (s : Finset ι) ↦ ∏ x ∈ s, f x

Tactic:
fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le hst
    (fun i _ ↦ zero_le_one.trans (hf i)) (fun x _ _ ↦ hf x)

Premises used: Monotone, zero_le_one, LE.le.trans, Finset.prod_le_prod_of_subset_of_one_le
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
hf0 : ∀ (x : ι), 0 ≤ f x
hf : ∀ (x : ι), f x ≤ 1
x x_1 : Finset ι
hst : x ≤ x_1
⊢ ∀ i ∈ x_1, 0 ≤ f i

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
hf0 : ∀ (x : ι), 0 ≤ f x
hf : ∀ (x : ι), f x ≤ 1
x x_1 : Finset ι
hst : x ≤ x_1
⊢ ∀ i ∈ x_1, i ∉ x → f i ≤ 1

Tactic:
simp [hf]