awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : R
s : List R
hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
cons : 0 < a * s.prod
⊢ 0 < (a :: s).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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
a : R
s : List R
hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < a ∧ ∀ (a : R), a ∈ s → 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
a : R
s : List R
hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod
h : 0 < a ∧ ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < a * s.prod

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

Premises used: mul_pos, 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
a : R
s : List R
hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod
h : 0 < a ∧ ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < a * s.prod

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

Premises used: mul_pos, 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
s : List R
h : ∀ (a : R), a ∈ s → 0 < a
nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 < a), LT.lt.{u_1} (α := R) 0 (prod [])
cons :
  ∀ (a : R) (s : List R) (hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod)
    (h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1), 0 < (a :: s).prod
⊢ 0 < s.prod

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

Premises used: forall_eq_or_imp, 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s : List ι
f g : ι → R
hs : Ne.{u_2 + 1} (α := List ι) [] []
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:
contradiction
-- 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
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
simp : 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
⊢ MulPosStrictMono R

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
h₁ : f a < g a
h₂ : (map f s).prod ≤ (map g s).prod
c0 : 0 < (map f s).prod
b0 : 0 ≤ g a
⊢ f a * (map f s).prod < g a * (map g s).prod

Tactic:
apply mul_lt_mul

Premises used: mul_lt_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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
h₁ : 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono 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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
h₂ : ∀ (i : ι), i ∈ s → 0 ≤ f i
h₃ : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
apply prod_map_le_prod_map₀

Premises used: List.prod_map_le_prod_map₀
-- 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
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
h₂ : 0 < f i
⊢ 0 ≤ f i

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- 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
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
h₂ : i ∈ a :: s
⊢ 0 < f i

Tactic:
apply h0
-- 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
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ i ∈ a :: s

Tactic:
simp [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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
h₂ : f i < g i
⊢ f i ≤ g i

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- 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
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
h₂ : i ∈ a :: s
⊢ f i < g i

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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
c0 : ∀ (a : R), a ∈ map f s → 0 < a
⊢ 0 < (map f s).prod

Tactic:
apply prod_pos

Premises used: List.prod_pos
-- 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
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ ∀ (a : R), a ∈ map f s → 0 < a

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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
apply apply₁ : a ∈ a :: s
⊢ 0 ≤ g a

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

Premises used: le_of_lt, LT.lt.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 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s : List ι
hs : s ≠ []
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
match s with
  | [] => contradiction
  | a :: s =>
    simp only [map_cons, prod_cons]
    have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
    apply mul_lt_mul
    · apply h
      simp
    · apply prod_map_le_prod_map₀
      · intro i hi
        apply le_of_lt
        apply h0
        simp [hi]
      · intro i hi
        apply le_of_lt
        apply h
        simp [hi]
    · apply prod_pos
      grind
    · apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 0 ≤ a
a : ∀ (a : List R) (h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 0 ≤ a_1), 0 ≤ prod ⟦a⟧
⊢ 0 ≤ s.prod

Tactic:
cases s using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
a_1 : List R
h : ∀ (a : R), a ∈ ⟦a_1⟧ → 0 ≤ a
a : ∀ (h : ∀ (a : R), a ∈ a_1 → 0 ≤ a), 0 ≤ a_1.prod
⊢ 0 ≤ prod ⟦a_1⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, prod_coe] at *

Premises used: Multiset.mem_coe, Multiset.quot_mk_to_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
a : List R
h : ∀ (a_1 : R), a_1 ∈ a → 0 ≤ a_1
⊢ 0 ≤ a.prod

Tactic:
apply List.prod_nonneg h

Premises used: List.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 1 ≤ a
a : ∀ (a : List R) (h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 1 ≤ a_1), 1 ≤ prod ⟦a⟧
⊢ 1 ≤ s.prod

Tactic:
cases s using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
a_1 : List R
h : ∀ (a : R), a ∈ ⟦a_1⟧ → 1 ≤ a
a : ∀ (h : ∀ (a : R), a ∈ a_1 → 1 ≤ a), 1 ≤ a_1.prod
⊢ 1 ≤ prod ⟦a_1⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, prod_coe] at *

Premises used: Multiset.mem_coe, Multiset.quot_mk_to_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
a : List R
h : ∀ (a_1 : R), a_1 ∈ a → 1 ≤ a_1
⊢ 1 ≤ a.prod

Tactic:
apply List.one_le_prod h

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

Tactic:
cases s using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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_1 : List ι
h0 : ∀ (i : ι), i ∈ ⟦a_1⟧ → 0 ≤ f i
h : ∀ (i : ι), i ∈ ⟦a_1⟧ → f i ≤ g i
a :
  ∀ (h0 : ∀ (i : ι), i ∈ a_1 → 0 ≤ f i) (h : ∀ (i : ι), i ∈ a_1 → f i ≤ g i),
    (List.map f a_1).prod ≤ (List.map g a_1).prod
⊢ (map f ⟦a_1⟧).prod ≤ (map g ⟦a_1⟧).prod

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *

Premises used: Multiset.mem_coe, Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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 : List ι
h0 : ∀ (i : ι), i ∈ a → 0 ≤ f i
h : ∀ (i : ι), i ∈ a → f i ≤ g i
⊢ (List.map f a).prod ≤ (List.map g a).prod

Tactic:
apply List.prod_map_le_prod_map₀ f g h0 h

Premises used: List.prod_map_le_prod_map₀
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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 : Multiset 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 :
  ∀ (a : List L) (hf0 : ∀ (x : L), x ∈ ⟦a⟧ → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R))
    (hf : ∀ (x : L), x ∈ ⟦a⟧ → (f : (a : L) → R) x ≤ r), prod (map (⇑f : (a : L) → R) ⟦a⟧) ≤ r ^ card ⟦a⟧
⊢ prod (map (⇑f : (a : L) → R) t) ≤ r ^ t.card

Tactic:
induction t using Quotient.inductionOn
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
a : List L
hf0 : ∀ (x : L), x ∈ ⟦a⟧ → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R)
hf : ∀ (x : L), x ∈ ⟦a⟧ → (f : (a : L) → R) x ≤ r
⊢ prod (map (⇑f : (a : L) → R) ⟦a⟧) ≤ r ^ card ⟦a⟧

Tactic:
simp_all [List.prod_map_le_pow_length₀]

Premises used: List.prod_map_le_pow_length₀
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ 0 ≤ (map f s).prod

Tactic:
prod_nonneg fun r hr ↦ ?_

Premises used: Multiset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
refine : ∀ (r : R) (hr : r ∈ map f s), 0 ≤ r
⊢ 0 ≤ (map f s).prod

Tactic:
refine prod_nonneg fun r hr ↦ ?_

Premises used: Multiset.prod_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
r : R
hr : r ∈ map f s
obtain : ∀ (a : α) (ha : a ∈ s) (hr : f a ∈ map f s), 0 ≤ f a
⊢ 0 ≤ r

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_map.mp hr

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
a : α
ha : a ∈ s
hr : f a ∈ map f s
⊢ 0 ≤ f a

Tactic:
h a ha
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
a : α
ha : a ∈ s
hr : f a ∈ map f s
⊢ 0 ≤ f a

Tactic:
exact h a ha
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
⊢ 1 ≤ (map f s).prod

Tactic:
one_le_prod fun r hr ↦ ?_

Premises used: Multiset.one_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
refine : ∀ (r : R) (hr : r ∈ map f s), 1 ≤ r
⊢ 1 ≤ (map f s).prod

Tactic:
refine one_le_prod fun r hr ↦ ?_

Premises used: Multiset.one_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
r : R
hr : r ∈ map f s
obtain : ∀ (a : α) (ha : a ∈ s) (hr : f a ∈ map f s), 1 ≤ f a
⊢ 1 ≤ r

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_map.mp hr

Premises used: Multiset.mem_map, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
a : α
ha : a ∈ s
hr : f a ∈ map f s
⊢ 1 ≤ f a

Tactic:
h a ha
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
a : α
ha : a ∈ s
hr : f a ∈ map f s
⊢ 1 ≤ f a

Tactic:
exact h a ha
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
s : Multiset R
h : ∀ (a : R), a ∈ s → 0 < a
a : ∀ (a : List R) (h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 0 < a_1), 0 < prod ⟦a⟧
⊢ 0 < s.prod

Tactic:
cases s using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
a_1 : List R
h : ∀ (a : R), a ∈ ⟦a_1⟧ → 0 < a
a : ∀ (h : ∀ (a : R), a ∈ a_1 → 0 < a), 0 < a_1.prod
⊢ 0 < prod ⟦a_1⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, prod_coe] at *

Premises used: Multiset.mem_coe, Multiset.quot_mk_to_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
a : List R
h : ∀ (a_1 : R), a_1 ∈ a → 0 < a_1
⊢ 0 < a.prod

Tactic:
apply List.prod_pos h

Premises used: List.prod_pos
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
ι : Type u_3
s : Multiset ι
hs : s ≠ 0
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
a :
  ∀ (a : List ι) (hs : ⟦a⟧ ≠ 0) (h0 : ∀ (i : ι), i ∈ ⟦a⟧ → 0 < f i) (h : ∀ (i : ι), i ∈ ⟦a⟧ → f i < g i),
    (map f ⟦a⟧).prod < (map g ⟦a⟧).prod
⊢ (map f s).prod < (map g s).prod

Tactic:
cases s using Quotient.ind

Premises used: Quotient.ind
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
ι : Type u_3
f g : ι → R
a_1 : List ι
hs : ⟦a_1⟧ ≠ 0
h0 : ∀ (i : ι), i ∈ ⟦a_1⟧ → 0 < f i
h : ∀ (i : ι), i ∈ ⟦a_1⟧ → f i < g i
a :
  ∀ (hs : ¬a_1 = []) (h0 : ∀ (i : ι), i ∈ a_1 → 0 < f i) (h : ∀ (i : ι), i ∈ a_1 → f i < g i),
    (List.map f a_1).prod < (List.map g a_1).prod
⊢ (map f ⟦a_1⟧).prod < (map g ⟦a_1⟧).prod

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *

Premises used: Multiset.mem_coe, Multiset.coe_eq_zero, Multiset.quot_mk_to_coe, ne_eq, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
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
ι : Type u_3
f g : ι → R
a : List ι
hs : ¬a = []
h0 : ∀ (i : ι), i ∈ a → 0 < f i
h : ∀ (i : ι), i ∈ a → f i < g i
⊢ (List.map f a).prod < (List.map g a).prod

Tactic:
apply List.prod_map_lt_prod_map hs f g h0 h

Premises used: List.prod_map_lt_prod_map
-- 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
simp : LE.le.{u_2} (α := R) (∑ x ∈ s, f x * f x) (∑ i ∈ s, ∑ j ∈ s, f i * f j)
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2 ≤ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2

Tactic:
simp only [sq, sum_mul_sum]

Premises used: sq, Finset.sum_mul_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
⊢ LE.le.{u_2} (α := R) (∑ x ∈ s, f x * f x) (∑ i ∈ s, ∑ j ∈ s, f i * f j)

Tactic:
sum_le_sum fun i hi ↦ ?_

Premises used: Finset.sum_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
refine : ∀ (i : ι) (hi : i ∈ s), f i * f i ≤ ∑ j ∈ s, f i * f j
⊢ LE.le.{u_2} (α := R) (∑ x ∈ s, f x * f x) (∑ i ∈ s, ∑ j ∈ s, f i * f j)

Tactic:
refine sum_le_sum fun i hi ↦ ?_

Premises used: Finset.sum_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
rw : f i * f i ≤ f i * ∑ i ∈ s, f i
⊢ f i * f i ≤ ∑ j ∈ s, f i * f j

Tactic:
rw [← mul_sum]

Premises used: Finset.mul_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
ha : 0 ≤ f i
hbc : f i ≤ ∑ i ∈ s, f i
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i

Tactic:
gcongr