awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
left : prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map f l).prod
right : prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map g l).prod
⊢ 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

Tactic:
constructor
-- 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
left : ∀ (i : α), i ∈ l → min (f i) (g i) ≤ f i
⊢ prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map f l).prod

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
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
l : List α
f g : α → M
right : ∀ (i : α), i ∈ l → min (f i) (g i) ≤ g i
⊢ prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map g l).prod

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
inst_1 : LinearOrder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
l : List α
f g : α → M
i : α
h : i ∈ l
⊢ min (f i) (g i) ≤ f i

Tactic:
apply min_le_left

Premises used: min_le_left
-- 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
i : α
h : i ∈ l
⊢ min (f i) (g i) ≤ g i

Tactic:
apply min_le_right

Premises used: min_le_right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
⊢ Monotone.{0, u_3} (β := M) fun (i : ℕ) ↦ (take i L).prod

Tactic:
monotone_nat_of_le_succ fun n => ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
refine : ∀ (n : ℕ), (take n L).prod ≤ (take (n + 1) L).prod
⊢ Monotone.{0, u_3} (β := M) fun (i : ℕ) ↦ (take i L).prod

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
n : ℕ
inl : ∀ (h : n < L.length), (take n L).prod ≤ (take (n + 1) L).prod
inr : ∀ (h : L.length ≤ n), (take n L).prod ≤ (take (n + 1) L).prod
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
rcases lt_or_ge n L.length with h | h

Premises used: lt_or_ge, List.length
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
inl : (take n L).prod ≤ (take n L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L n h
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
rw [prod_take_succ _ _ h]

Premises used: List.prod_take_succ
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L n h

Tactic:
le_self_mul

Premises used: le_self_mul
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L n h

Tactic:
exact le_self_mul

Premises used: le_self_mul
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

Premises used: List.take_of_length_le, Nat.le_succ, le_trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x : M
h₁ : Membership.mem (γ := List M) [] x
⊢ x ≤ prod []

Tactic:
simp at h₁
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x y : M
ys : List M
ih : ∀ (h₁ : x ∈ ys), x ≤ ys.prod
h₁ : x ∈ y :: ys
⊢ x = y ∨ x ∈ ys

Tactic:
simp only [mem_cons] at h₁

Premises used: List.mem_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x y : M
ys : List M
ih : ∀ (h₁ : x ∈ ys), x ≤ ys.prod
h₁ : x = y ∨ x ∈ ys
cons : x ≤ (x :: ys).prod
cons₁ : ∀ (h₁ : x ∈ ys), x ≤ (y :: ys).prod
⊢ x ≤ (y :: ys).prod

Tactic:
rcases h₁ with (rfl | h₁)

Premises used: rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x : M
ys : List M
ih : ∀ (h₁ : x ∈ ys), x ≤ ys.prod
⊢ x ≤ (x :: ys).prod

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x y : M
ys : List M
ih : ∀ (h₁ : x ∈ ys), x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ ys.prod

Tactic:
specialize ih h₁
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
cons : x ≤ y * ys.prod
⊢ x ≤ (y :: ys).prod

Tactic:
simp only [List.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 : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
⊢ x ≤ y * ys.prod

Tactic:
le_mul_left ih

Premises used: le_mul_left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
⊢ x ≤ y * ys.prod

Tactic:
exact le_mul_left ih

Premises used: le_mul_left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
xs : List M
x : M
h₁ : x ∈ xs
nil : ∀ (h₁ : Membership.mem (γ := List M) [] x), x ≤ prod []
cons : ∀ (y : M) (ys : List M) (ih : ∀ (h₁ : x ∈ ys), x ≤ ys.prod) (h₁ : x ∈ y :: ys), x ≤ (y :: ys).prod
⊢ x ≤ xs.prod

Tactic:
induction xs with
  | nil => simp at h₁
  | cons y ys ih =>
    simp only [mem_cons] at h₁
    rcases h₁ with (rfl | h₁)
    · simp
    · specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

Premises used: List.cons, List.mem_cons, List.prod_cons, rfl, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
hpl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a
⊢ f (prod []) ≤ (map f []).prod

Tactic:
simp [h_one]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : ∀ (hpl : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
⊢ ∀ (x : α), x ∈ s → p x

Tactic:
have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : ∀ (hpl : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
⊢ p s.prod

Tactic:
have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : List α
ih : ∀ (hpl : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
cons : f (a * s.prod) ≤ (map f (a :: s)).prod
cons₁ : f (a * s.prod) ≤ (f a :: map f s).prod
cons₂ : f (a * s.prod) ≤ f a * (map f s).prod
cons₃ : f a * f s.prod ≤ f a * (map f s).prod
cons₄ cons₅ : f a * (map f s).prod ≤ f a * (map f s).prod
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod

Tactic:
grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]

Premises used: List.map_cons, List.mem_cons_self, List.prod_cons, List.prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hpl : ∀ (a : α), a ∈ l → p a
nil : ∀ (hpl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a), f (prod []) ≤ (map f []).prod
cons :
  ∀ (a : α) (s : List α) (ih : ∀ (hpl : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod)
    (hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1), f (a :: s).prod ≤ (map f (a :: s)).prod
⊢ f l.prod ≤ (map f l).prod

Tactic:
induction l with
  | nil => simp [h_one]
  | cons a s ih =>
    have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
    have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
    grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]

Premises used: List.map_cons, List.cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ ∀ (a b : α), (fun (x : α) ↦ True) a → (fun (x : α) ↦ True) b → (fun (x : α) ↦ True) (a * b)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ ∀ (a : α), a ∈ l → (fun (x : α) ↦ True) a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
hl_nonempty : Ne.{u_5 + 1} (α := List α) [] []
hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a
⊢ f (prod []) ≤ (map f []).prod

Tactic:
simp at hl_nonempty
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
cons : f (a * l.prod) ≤ f a * (map f l).prod
⊢ f (a :: l).prod ≤ (map f (a :: l)).prod

Tactic:
rw [prod_cons, map_cons, prod_cons]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
pos : ∀ (hl_empty : l = []), f (a * l.prod) ≤ f a * (map f l).prod
neg : ∀ (hl_empty : ¬l = []), f (a * l.prod) ≤ f a * (map f l).prod
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
by_cases hl_empty : l = []
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
simp [hl_empty]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
⊢ ∀ (x : α), x ∈ l → p x

Tactic:
have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
⊢ p l.prod

Tactic:
have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
⊢ p a

Tactic:
have hp_a : p a := hl a mem_cons_self
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
hp_a : p a
neg : f a * f l.prod ≤ f a * (map f l).prod
neg₁ neg₂ : f a * f l.prod ≤ f a * f l.prod
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hl_nonempty : l ≠ []
hl : ∀ (a : α), a ∈ l → p a
nil :
  ∀ (hl_nonempty : Ne.{u_5 + 1} (α := List α) [] []) (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
    f (prod []) ≤ (map f []).prod
cons :
  ∀ (a : α) (l : List α) (ih : ∀ (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a), f l.prod ≤ (map f l).prod)
    (hl_nonempty : a :: l ≠ []) (hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1), f (a :: l).prod ≤ (map f (a :: l)).prod
⊢ f l.prod ≤ (map f l).prod

Tactic:
induction l with
  | nil => simp at hl_nonempty
  | cons a l ih =>
    rw [prod_cons, map_cons, prod_cons]
    by_cases hl_empty : l = []
    · simp [hl_empty]
    have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
    have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
    have hp_a : p a := hl a mem_cons_self
    grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]

Premises used: List.map_cons, List.cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a b : α), (fun (x : α) ↦ True) a → (fun (x : α) ↦ True) b → f (a * b) ≤ f a * f b

Tactic:
simp [h_mul]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a b : α), (fun (x : α) ↦ True) a → (fun (x : α) ↦ True) b → (fun (x : α) ↦ True) (a * b)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a : α), a ∈ l → (fun (x : α) ↦ True) a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : Zero N
inst_2 : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f (sum []) ≤ foldr max 0 (map f [])

Tactic:
simpa using h0
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : Zero N
inst_2 : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr max 0 (map f tl)
cons :
  ∀ (IH : f tl.sum ≤ foldr (fun (x : M) (y : N) ↦ max (f x) y) 0 tl),
    f (hd + tl.sum) ≤ max (f hd) (foldr (fun (x : M) (y : N) ↦ max (f x) y) 0 tl)
⊢ f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))

Tactic:
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢

Premises used: List.sum_cons, List.foldr_map, List.foldr
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : Zero N
inst_2 : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr (fun (x : M) (y : N) ↦ max (f x) y) 0 tl
⊢ f (hd + tl.sum) ≤ max (f hd) (foldr (fun (x : M) (y : N) ↦ max (f x) y) 0 tl)

Tactic:
(hadd _ _).trans (max_le_max le_rfl IH)

Premises used: le_rfl, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : Zero N
inst_2 : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr (fun (x : M) (y : N) ↦ max (f x) y) 0 tl
⊢ f (hd + tl.sum) ≤ max (f hd) (foldr (fun (x : M) (y : N) ↦ max (f x) y) 0 tl)

Tactic:
exact (hadd _ _).trans (max_le_max le_rfl IH)

Premises used: le_rfl, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : Zero N
inst_2 : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
l : List M
nil : f (sum []) ≤ foldr max 0 (map f [])
cons :
  ∀ (hd : M) (tl : List M) (IH : f tl.sum ≤ foldr max 0 (map f tl)), f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))
⊢ f l.sum ≤ foldr max 0 (map f l)

Tactic:
induction l with
  | nil => simpa using h0
  | cons hd tl IH =>
    simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
    exact (hadd _ _).trans (max_le_max le_rfl IH)

Premises used: List.cons, List.sum_cons, List.foldr_map, List.foldr, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
h_1 : [b] ≠ []
⊢ 1 < [b].prod

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
h : a :: b :: l ≠ []
⊢ 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a

Tactic:
simp only [forall_eq_or_imp, List.mem_cons] at hl₁

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
a b : M
l : List M
h : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
rw : 1 < a * (b :: l).prod
⊢ 1 < (a :: b :: l).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
a b : M
l : List M
h : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
apply : 1 ≤ (b :: l).prod
⊢ 1 < a * (b :: l).prod

Tactic:
apply one_lt_mul_of_lt_of_le' hl₁.1

Premises used: And.left, one_lt_mul_of_lt_of_le'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
a b : M
l : List M
h : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
apply : ∀ (x : M), x ∈ b :: l → 1 < x
⊢ 1 ≤ (b :: l).prod

Tactic:
apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))

Premises used: le_of_lt, List.cons, List.cons_ne_nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
a b : M
l : List M
h : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ ∀ (x : M), x ∈ b :: l → 1 < x

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
nil :
  ∀ (hl₁ : ∀ (x : M), Membership.mem (γ := List M) [] x → 1 ≤ x) (x : M),
    Membership.mem (γ := List M) [] x → x ≤ prod []
cons :
  ∀ (head : M) (tail : List M),
    (∀ (hl₁ : ∀ (x : M), x ∈ tail → 1 ≤ x) (x : M), x ∈ tail → x ≤ tail.prod) →
      ∀ (hl₁ : ∀ (x : M), x ∈ head :: tail → 1 ≤ x) (x : M), x ∈ head :: tail → x ≤ (head :: tail).prod
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod

Tactic:
induction l
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
hl₁ : ∀ (x : M), Membership.mem (γ := List M) [] x → 1 ≤ x
⊢ ∀ (x : M), Membership.mem (γ := List M) [] x → x ≤ prod []

Tactic:
simp