awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
have cons : 1 ≤ hd * tl.prod
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 1 ≤ l.prod
have nil : ∀ (hl₁ : ∀ (x : M), Membership.mem (γ := List M) [] x → 1 ≤ x), LE.le.{u_3} (α := M) 1 1
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))
Cleared hypotheses: l, hl₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 1 ≤ l.prod
have 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
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))
Cleared hypotheses: l, hl₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ max (map f l).prod (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
have 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)
Tactic: rw [max_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ (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)
have left : (map f l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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)
⊢ (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)
have right : (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ (map f l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
have left : ∀ (i : α), i ∈ l → f i ≤ max (f i) (g i)
Tactic: apply List.prod_le_prod'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ (map g l).prod ≤ prod (map (fun (i : α) ↦ max (f i) (g i)) l)
have right : ∀ (i : α), i ∈ l → g i ≤ max (f i) (g i)
Tactic: apply List.prod_le_prod'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ min (map f l).prod (map g l).prod
have 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
Tactic: rw [le_min_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 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
have left : prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map f l).prod
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 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
have right : prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map g l).prod
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map f l).prod
have left : ∀ (i : α), i ∈ l → min (f i) (g i) ≤ f i
Tactic: apply List.prod_le_prod'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ prod (map (fun (i : α) ↦ min (f i) (g i)) l) ≤ (map g l).prod
have right : ∀ (i : α), i ∈ l → min (f i) (g i) ≤ g i
Tactic: apply List.prod_le_prod'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
have refine : ∀ (n : ℕ), (take n L).prod ≤ (take (n + 1) L).prod
Tactic: refine monotone_nat_of_le_succ fun n => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
L : List M
n : ℕ
⊢ (take n L).prod ≤ (take (n + 1) L).prod
have inl : ∀ (h : n < L.length), (take n L).prod ≤ (take (n + 1) L).prod
Tactic: rcases lt_or_ge n L.length with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ (take n L).prod ≤ (take (n + 1) L).prod
have inr : ∀ (h : L.length ≤ n), (take n L).prod ≤ (take (n + 1) L).prod
Tactic: rcases lt_or_ge n L.length with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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 + 1) L).prod
have inl : (take n L).prod ≤ (take n L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L n h
Tactic: rw [prod_take_succ _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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 :: ys).prod
have h₂ : x = y ∨ x ∈ ys
Tactic: simp only [mem_cons] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ x ≤ (y :: ys).prod
have cons : x ≤ (x :: ys).prod
Tactic: rcases h₁ with (rfl | h₁)
Cleared hypotheses: y, h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ x ≤ (y :: ys).prod
have cons₁ : ∀ (h₁ : x ∈ ys), x ≤ (y :: ys).prod
Tactic: rcases h₁ with (rfl | h₁)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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 ≤ (y :: ys).prod
have ih₁ : x ≤ ys.prod
Tactic: specialize ih h₁
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
have cons : x ≤ y * ys.prod
Tactic: simp only [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
xs : List M
x : M
h₁ : x ∈ xs
⊢ x ≤ xs.prod
have nil : ∀ (h₁ : Membership.mem (γ := List M) [] x), x ≤ 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
Cleared hypotheses: xs, h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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 []
⊢ x ≤ xs.prod
have cons : ∀ (y : M) (ys : List M) (ih : ∀ (h₁ : x ∈ ys), x ≤ ys.prod) (h₁ : x ∈ y :: ys), x ≤ (y :: ys).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
Cleared hypotheses: xs, h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have hpla : ∀ (x : α), x ∈ s → p x
Tactic: have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have hp_prod : p s.prod
Tactic: have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have cons : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have cons₁ : f (a * s.prod) ≤ (f a :: map f s).prod
Tactic: grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have cons₂ : f (a * s.prod) ≤ f a * (map f s).prod
Tactic: grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have cons₃ : f a * f s.prod ≤ f a * (map f s).prod
Tactic: grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
have cons₄ : f a * (map f s).prod ≤ f a * (map f s).prod
Tactic: grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f l.prod ≤ (map f l).prod
have nil : ∀ (hpl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a), f (prod []) ≤ (map f []).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]
Cleared hypotheses: l, hpl
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f l.prod ≤ (map f l).prod
have 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
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]
Cleared hypotheses: l, hpl
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a :: l).prod ≤ (map f (a :: l)).prod
have cons : f (a * l.prod) ≤ f a * (map f l).prod
Tactic: rw [prod_cons, map_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
have pos : ∀ (hl_empty : l = []), f (a * l.prod) ≤ f a * (map f l).prod
Tactic: by_cases hl_empty : l = []
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
have neg : ∀ (hl_empty : ¬l = []), f (a * l.prod) ≤ f a * (map f l).prod
Tactic: by_cases hl_empty : l = []
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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
have hla_restrict : ∀ (x : α), x ∈ l → p x
Tactic: have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
have hp_sup : p l.prod
Tactic: have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
have hp_a : p a
Tactic: have hp_a : p a := hl a mem_cons_self
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
have neg : f a * f l.prod ≤ f a * (map f l).prod
Tactic: grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
have neg₁ : f a * f l.prod ≤ f a * f l.prod
Tactic: grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f l.prod ≤ (map f l).prod
have nil : ∀ (hl_nonempty : Ne.{u_5 + 1} (α := List α) [] []) (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
  f (prod []) ≤ (map f []).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]
Cleared hypotheses: l, hl_nonempty, hl