awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
x : Multiset α
⊢ Eq.{u_2 + 1} (α := Multiset (Multiset α)) ((Finset.range (x.card + 1)).sup fun (k : ℕ) ↦ powersetCard k x)
    (∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x)

Tactic:
Eq.symm (finsetSum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetCard x h)

Premises used: Iff.mpr, Multiset.pairwise_disjoint_powersetCard, Multiset.finsetSum_eq_sup_iff_disjoint, Eq.symm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
x : Multiset α
⊢ Eq.{u_2 + 1} (α := Multiset (Multiset α)) ((Finset.range (x.card + 1)).sup fun (k : ℕ) ↦ powersetCard k x)
    (∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x)

Tactic:
exact
    Eq.symm (finsetSum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetCard x h)

Premises used: Iff.mpr, Multiset.pairwise_disjoint_powersetCard, Multiset.finsetSum_eq_sup_iff_disjoint, Eq.symm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
⊢ ∀ x ∈ m.toFinset, 1 ≤ count x m

Tactic:
simp [one_le_count_iff_mem]

Premises used: Multiset.one_le_count_iff_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
rw :
  (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
⊢ m.card ≤ m.toFinset.card + 1 ↔ ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
rw [← m.toFinset_sum_count_eq, m.toFinset.card_eq_sum_ones, ← tsub_le_iff_left,
    ← Finset.sum_tsub_distrib _ (by simp [one_le_count_iff_mem]), Finset.sum_le_one_iff]

Premises used: Multiset.toFinset, Finset.card_eq_sum_ones, Multiset.toFinset_sum_count_eq, Finset.sum_le_one_iff, tsub_le_iff_left, Finset.sum_tsub_distrib
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
simp :
  (∀ (x y : α), x ∈ m → y ∈ m → 1 < count x m → 1 < count y m → x = y ∧ count x m = HAdd.hAdd (α := ℕ) 0 2) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
⊢ (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
simp only [← pos_iff_ne_zero, Nat.sub_pos_iff_lt, mem_toFinset, Nat.pred_eq_succ_iff]

Premises used: Nat.sub_pos_iff_lt, Nat.pred_eq_succ_iff, pos_iff_ne_zero, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m → y ∈ m → 1 < count x m → 1 < count y m → x = y ∧ count x m = HAdd.hAdd (α := ℕ) 0 2) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
⟨fun h x y hx hy ↦ h x y (one_le_count_iff_mem.mp hx.le)
    (one_le_count_iff_mem.mp hy.le) hx hy, fun h x y _ _ hx hy ↦ h x y hx hy⟩

Premises used: LT.lt.le, Iff.intro, Iff.mp, Multiset.one_le_count_iff_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m → y ∈ m → 1 < count x m → 1 < count y m → x = y ∧ count x m = HAdd.hAdd (α := ℕ) 0 2) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
exact ⟨fun h x y hx hy ↦ h x y (one_le_count_iff_mem.mp hx.le)
    (one_le_count_iff_mem.mp hy.le) hx hy, fun h x y _ _ hx hy ↦ h x y hx hy⟩
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
⊢ LE.le.{u_3} (α := M) (prod []) (prod [])

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
a b : M
l₁_1 l₂_1 : List M
hab : a ≤ b
ih : Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁_1 l₂_1
ih' : l₁_1.prod ≤ l₂_1.prod
⊢ (a :: l₁_1).prod ≤ (b :: l₂_1).prod

Tactic:
simpa only [prod_cons] using mul_le_mul' hab ih'

Premises used: List.prod_cons, mul_le_mul'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁ l₂
nil : LE.le.{u_3} (α := M) (prod []) (prod [])
cons :
  ∀ {a b : M} {l₁ l₂ : List M} (hab : a ≤ b) (ih : Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁ l₂) (ih' : l₁.prod ≤ l₂.prod),
    (a :: l₁).prod ≤ (b :: l₂).prod
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'

Premises used: List.Forall₂.cons, List.Forall₂.nil, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h₁ : ∀ (a : M), Membership.mem (γ := List M) [] a → 1 ≤ a
⊢ LE.le.{u_3} (α := M) (prod []) (prod [])

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂_1 → 1 ≤ a_1
cons : ∀ (h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x), l₁_1.prod ≤ a * l₂_1.prod
⊢ l₁_1.prod ≤ (a :: l₂_1).prod

Tactic:
simp only [prod_cons, forall_mem_cons] at h₁ ⊢

Premises used: List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x
⊢ l₁_1.prod ≤ a * l₂_1.prod

Tactic:
(ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)

Premises used: le_mul_of_one_le_left', And.right, And.left, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x
⊢ l₁_1.prod ≤ a * l₂_1.prod

Tactic:
exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)

Premises used: le_mul_of_one_le_left', And.right, And.left, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂_1 → 1 ≤ a_1
cons_cons : ∀ (h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x), a * l₁_1.prod ≤ a * l₂_1.prod
⊢ (a :: l₁_1).prod ≤ (a :: l₂_1).prod

Tactic:
simp only [prod_cons, forall_mem_cons] at h₁ ⊢

Premises used: List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x
cons_cons cons_cons₁ : a * l₂_1.prod ≤ a * l₂_1.prod
⊢ a * l₁_1.prod ≤ a * l₂_1.prod

Tactic:
grw [ih' h₁.2]

Premises used: And.right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
slnil : ∀ (h₁ : ∀ (a : M), Membership.mem (γ := List M) [] a → 1 ≤ a), LE.le.{u_3} (α := M) (prod []) (prod [])
cons :
  ∀ {l₁ l₂ : List M} (a : M),
    l₁ <+ l₂ →
      ∀ (ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a), l₁.prod ≤ l₂.prod) (h₁ : ∀ (a_2 : M), a_2 ∈ a :: l₂ → 1 ≤ a_2),
        l₁.prod ≤ (a :: l₂).prod
cons_cons :
  ∀ {l₁ l₂ : List M} (a : M),
    l₁ <+ l₂ →
      ∀ (ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a), l₁.prod ≤ l₂.prod) (h₁ : ∀ (a_2 : M), a_2 ∈ a :: l₂ → 1 ≤ a_2),
        (a :: l₁).prod ≤ (a :: l₂).prod
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons_cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]

Premises used: List.Sublist.cons_cons, List.Sublist.slnil, List.forall_mem_cons, List.prod_cons, List.Sublist.cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : SublistForall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ l₁.prod ≤ l₂.prod

Tactic:
let ⟨_, hall, hsub⟩ := sublistForall₂_iff.1 h
  hall.prod_le_prod'.trans <| hsub.prod_le_prod' h₁

Premises used: _private.0.List.SublistForall₂.prod_le_prod'.match_1, List.Forall₂.prod_le_prod', LE.le, List.sublistForall₂_iff, Iff.mp, List.Sublist.prod_le_prod', LE.le.trans, List.prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → f i ≤ g i
⊢ Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) (map f l) (map g l)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
h₁ : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i
h₂ : ∃ (i : ι), Membership.mem (γ := List ι) [] i ∧ f i < g i
⊢ (map f []).prod < (map g []).prod

Tactic:
simp at h₂
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1
h₂ : ∃ (i_1 : ι), i_1 ∈ i :: l ∧ f i_1 < g i_1
cons : ∀ (h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x), f i * (map f l).prod < g i * (map g l).prod
⊢ (map f (i :: l)).prod < (map g (i :: l)).prod

Tactic:
simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢

Premises used: List.map_cons, List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₂ : ∃ (i_1 : ι), i_1 ∈ i :: l ∧ f i_1 < g i_1
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
⊢ f i < g i ∨ ∃ (a : ι), a ∈ l ∧ f a < g a

Tactic:
simp only [mem_cons, exists_eq_or_imp] at h₂

Premises used: exists_eq_or_imp, List.mem_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h₂ : f i < g i ∨ ∃ (a : ι), a ∈ l ∧ f a < g a
cons : f i < g i → f i * (map f l).prod < g i * (map g l).prod
cons₁ : (∃ (a : ι), a ∈ l ∧ f a < g a) → f i * (map f l).prod < g i * (map g l).prod
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
cases h₂
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)

Premises used: List.prod_le_prod', And.right, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)

Premises used: List.prod_le_prod', And.right, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h : ∃ (a : ι), a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

Premises used: And.right, And.left, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h : ∃ (a : ι), a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

Premises used: And.right, And.left, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
f g : ι → M
h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i
nil :
  ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i)
    (h₂ : ∃ (i : ι), Membership.mem (γ := List ι) [] i ∧ f i < g i), (map f []).prod < (map g []).prod
cons :
  ∀ (i : ι) (l : List ι)
    (ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod)
    (h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1) (h₂ : ∃ (i_1 : ι), i_1 ∈ i :: l ∧ f i_1 < g i_1),
    (map f (i :: l)).prod < (map g (i :: l)).prod
⊢ (map f l).prod < (map g l).prod

Tactic:
induction l with
  | nil => simp at h₂
  | cons i l ihl =>
    simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
    simp only [mem_cons, exists_eq_or_imp] at h₂
    cases h₂
    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
    · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

Premises used: List.map_cons, List.cons, exists_eq_or_imp, List.forall_mem_cons, List.mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
hlt : ∀ (i : ι), i ∈ l → f i < g i
⊢ (map f l).prod < (map g l).prod

Tactic:
(prod_lt_prod' f g fun i hi => (hlt i hi).le) <|
    (exists_mem_of_ne_nil l hl).imp fun i hi => ⟨hi, hlt i hi⟩

Premises used: LT.lt.le, List.prod_lt_prod', Exists.imp, List.exists_mem_of_ne_nil, And.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List M
n : M
h : ∀ (x : M), x ∈ l → x ≤ n
⊢ l.prod ≤ n ^ l.length

Tactic:
simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h

Premises used: List.map_id', List.map_const', List.prod_le_prod', List.prod_replicate
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List M
n : M
h : ∀ (x : M), x ∈ l → n ≤ x
⊢ n ^ l.length ≤ l.prod

Tactic:
@prod_le_pow_card Mᵒᵈ _ _ _ _ l n h

Premises used: OrderDual, List.prod_le_pow_card
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List ι
f g : ι → M
h : (map f l).prod < (map g l).prod
contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ l), g i ≤ f i), (map g l).prod ≤ (map f l).prod
⊢ ∃ (i : ι), i ∈ l ∧ f i < g i

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι) (_ : i ∈ l), g i ≤ f i
⊢ (map g l).prod ≤ (map f l).prod

Tactic:
prod_le_prod' h

Premises used: List.prod_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι) (_ : i ∈ l), g i ≤ f i
⊢ (map g l).prod ≤ (map f l).prod

Tactic:
exact prod_le_prod' h

Premises used: List.prod_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : (map f l).prod ≤ (map g l).prod
contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ l), g x < f x), (map g l).prod < (map f l).prod
⊢ ∃ (x : ι), x ∈ l ∧ f x ≤ g x

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι) (_ : x ∈ l), g x < f x
⊢ (map g l).prod < (map f l).prod

Tactic:
prod_lt_prod_of_ne_nil hl _ _ h

Premises used: List.prod_lt_prod_of_ne_nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι) (_ : x ∈ l), g x < f x
⊢ (map g l).prod < (map f l).prod

Tactic:
exact prod_lt_prod_of_ne_nil hl _ _ h

Premises used: List.prod_lt_prod_of_ne_nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
hl₁ : ∀ (x : M), Membership.mem (γ := List M) [] x → 1 ≤ x
⊢ LE.le.{u_3} (α := M) 1 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
hd : M
tl : List M
ih : ∀ (hl₁ : ∀ (x : M), x ∈ tl → 1 ≤ x), 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
cons : 1 ≤ hd * tl.prod
⊢ 1 ≤ (hd :: tl).prod

Tactic:
rw [prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
hd : M
tl : List M
ih : ∀ (hl₁ : ∀ (x : M), x ∈ tl → 1 ≤ x), 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod

Tactic:
one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

Premises used: List.mem_cons_of_mem, one_le_mul, List.mem_cons_self
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
hd : M
tl : List M
ih : ∀ (hl₁ : ∀ (x : M), x ∈ tl → 1 ≤ x), 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod

Tactic:
exact one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

Premises used: List.mem_cons_of_mem, one_le_mul, List.mem_cons_self
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftMono M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
nil : ∀ (hl₁ : ∀ (x : M), Membership.mem (γ := List M) [] x → 1 ≤ x), LE.le.{u_3} (α := M) 1 1
cons :
  ∀ (hd : M) (tl : List M) (ih : ∀ (hl₁ : ∀ (x : M), x ∈ tl → 1 ≤ x), 1 ≤ tl.prod)
    (hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x), 1 ≤ (hd :: tl).prod
⊢ 1 ≤ l.prod

Tactic:
induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [prod_cons]
    exact one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

Premises used: List.cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
l : List α
f g : α → M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
rw :
  (map f l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l) ∧
    (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
⊢ max (map f l).prod (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)

Tactic:
rw [max_le_iff]

Premises used: max_le_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
l : List α
f g : α → M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
left : (map f l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
right : (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
⊢ (map f l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l) ∧
    (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
l : List α
f g : α → M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
left : ∀ (i : α), i ∈ l → f i ≤ max (f i) (g i)
⊢ (map f l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)

Tactic:
apply List.prod_le_prod'

Premises used: List.prod_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
l : List α
f g : α → M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
right : ∀ (i : α), i ∈ l → g i ≤ max (f i) (g i)
⊢ (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)

Tactic:
apply List.prod_le_prod'

Premises used: List.prod_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
l : List α
f g : α → M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
i : α
h : i ∈ l
⊢ f i ≤ max (f i) (g i)

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
l : List α
f g : α → M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
i : α
h : i ∈ l
⊢ g i ≤ max (f i) (g i)

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
l : List α
f g : α → M
rw :
  prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map f l).prod ∧
    prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map g l).prod
⊢ prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ min (map f l).prod (map g l).prod

Tactic:
rw [le_min_iff]

Premises used: le_min_iff