awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
conv_lhs :
  HMul.hMul (α := β) (∏ x ∈ disjointed s 0, g x) (∏ k ∈ range n, ∏ x ∈ disjointed s (k + 1), g x) =
    HMul.hMul (α := β) (∏ i ∈ s 0, g i) (∏ i ∈ range n, ∏ j ∈ s (i + 1) \ s i, g j)
⊢ ∏ i ∈ s n, g i = HMul.hMul (α := β) (∏ i ∈ s 0, g i) (∏ i ∈ range n, ∏ j ∈ s (i + 1) \ s i, g j)

Tactic:
conv_lhs => rw [← hs.partialSups_eq, ← disjiUnion_Iic_disjointed, Iic_eq_Icc,
    prod_disjiUnion, Nat.bot_eq_zero, ← Nat.range_succ_eq_Icc_zero, prod_range_succ', mul_comm]

Premises used: Finset.prod_range_succ', Finset.prod_disjiUnion, Finset.Iic_eq_Icc, Monotone.partialSups_eq, Nat.range_succ_eq_Icc_zero, mul_comm, Nat.bot_eq_zero, Finset.disjiUnion_Iic_disjointed
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
refine_1 : disjointed s 0 = s 0
refine_2 : ∀ (k : ℕ), (Iio (k + 1)).sup s = s k
⊢ HMul.hMul (α := β) (∏ x ∈ disjointed s 0, g x) (∏ k ∈ range n, ∏ x ∈ disjointed s (k + 1), g x) =
    HMul.hMul (α := β) (∏ i ∈ s 0, g i) (∏ i ∈ range n, ∏ j ∈ s (i + 1) \ s i, g j)

Tactic:
congrm (∏ x ∈ ?_, g x) * ∏ k ∈ range n, ∏ x ∈ s (k + 1) \ ?_, g x

Premises used: Finset.prod, Finset.range
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
⊢ disjointed s 0 = s 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
refine_2 : (Iic k).sup (s ∘ id) = s k
⊢ (Iio (k + 1)).sup s = s k

Tactic:
change (Iic k).sup (s ∘ id) = s k

Premises used: Function.comp, id, Finset.Iic, Finset.sup
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
refine_2 : s ((Iic k).sup id) = s k
refine_2₁ refine_2₂ : s k = s k
⊢ (Iic k).sup (s ∘ id) = s k

Tactic:
rw [← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic, sup_Iic]

Premises used: Finset.apply_sup_eq_sup_comp_of_nonempty, Finset.sup_Iic, Finset.nonempty_Iic
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
inst_2 : MulLeftMono α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
⊢ 1 ≤ prod ⟦l⟧

Tactic:
simpa using List.one_le_prod_of_one_le hl

Premises used: List.one_le_prod_of_one_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
inst_2 : IsOrderedMonoid α
l : List α
hl : ∀ (x : α), x ∈ ⟦l⟧ → 1 ≤ x
x : α
hx : x ∈ ⟦l⟧
⊢ x ≤ prod ⟦l⟧

Tactic:
simpa using List.single_le_prod hl x hx

Premises used: List.single_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
s : Multiset α
n : α
h : ∀ (x : α), x ∈ s → x ≤ n
h₁ : ∀ (a : List α) (h : ∀ (x : α), x ∈ ⟦a⟧ → x ≤ n), prod ⟦a⟧ ≤ n ^ card ⟦a⟧
⊢ s.prod ≤ n ^ s.card

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
n : α
a : List α
h : ∀ (x : α), x ∈ ⟦a⟧ → x ≤ n
⊢ prod ⟦a⟧ ≤ n ^ card ⟦a⟧

Tactic:
simpa using List.prod_le_pow_card _ _ h

Premises used: List.prod_le_pow_card
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_4
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ a → 1 ≤ x) → a.prod = 1 → ∀ (x : α), x ∈ a → x = 1

Tactic:
fun l => List.all_one_of_le_one_le_of_prod_eq_one

Premises used: List.all_one_of_le_one_le_of_prod_eq_one
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_4
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : Multiset α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ a → 1 ≤ x) → a.prod = 1 → ∀ (x : α), x ∈ a → x = 1

Tactic:
exact fun l => List.all_one_of_le_one_le_of_prod_eq_one

Premises used: List.all_one_of_le_one_le_of_prod_eq_one
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s t : Multiset α
inst_2 : MulLeftMono α
⊢ LE.le.{u_2} (α := α) (prod 0) (prod 0)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s t : Multiset α
inst_2 : MulLeftMono α
a b : α
as bs : Multiset α
rh : a ≤ b
h : Rel (fun (x1 x2 : α) ↦ x1 ≤ x2) as bs
rt : as.prod ≤ bs.prod
cons : a * as.prod ≤ b * bs.prod
⊢ (a ::ₘ as).prod ≤ (b ::ₘ bs).prod

Tactic:
rw [prod_cons, prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s t : Multiset α
inst_2 : MulLeftMono α
a b : α
as bs : Multiset α
rh : a ≤ b
h : Rel (fun (x1 x2 : α) ↦ x1 ≤ x2) as bs
rt : as.prod ≤ bs.prod
⊢ a * as.prod ≤ b * bs.prod

Tactic:
mul_le_mul' rh rt

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s t : Multiset α
inst_2 : MulLeftMono α
a b : α
as bs : Multiset α
rh : a ≤ b
h : Rel (fun (x1 x2 : α) ↦ x1 ≤ x2) as bs
rt : as.prod ≤ bs.prod
⊢ a * as.prod ≤ b * bs.prod

Tactic:
exact mul_le_mul' rh rt

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s t : Multiset α
inst_2 : MulLeftMono α
h : Rel (fun (x1 x2 : α) ↦ x1 ≤ x2) s t
zero : LE.le.{u_2} (α := α) (prod 0) (prod 0)
cons :
  ∀ {a b : α} {as bs : Multiset α} (rh : a ≤ b),
    Rel (fun (x1 x2 : α) ↦ x1 ≤ x2) as bs → ∀ (rt : as.prod ≤ bs.prod), (a ::ₘ as).prod ≤ (b ::ₘ bs).prod
⊢ s.prod ≤ t.prod

Tactic:
induction h with
  | zero => rfl
  | cons rh _ rt =>
    rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt

Premises used: Multiset.prod_cons, Multiset.cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
s : Multiset ι
f g : ι → α
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
prod_le_prod_of_rel_le <| rel_map.2 <| rel_refl_of_refl_on h

Premises used: Iff.mpr, Multiset.rel_refl_of_refl_on, Multiset.prod_le_prod_of_rel_le, Multiset.rel_map
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
inst_2 : MulLeftMono α
f : α → α
h : ∀ (x : α), x ∈ s → f x ≤ x
⊢ (map f s).prod ≤ s.prod

Tactic:
prod_le_prod_of_rel_le <| rel_map_left.2 <| rel_refl_of_refl_on h

Premises used: Iff.mpr, Multiset.rel_map_left, Multiset.rel_refl_of_refl_on, Multiset.prod_le_prod_of_rel_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
inst_2 : MulLeftMono α
f : α → α
h : ∀ (x : α), x ∈ s → x ≤ f x
⊢ s.prod ≤ (map f s).prod

Tactic:
prod_map_le_prod (α := αᵒᵈ) f h

Premises used: Multiset.prod_map_le_prod, OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
a : α
inst_2 : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
rw : (map (Function.const α a) s).prod ≤ s.prod
⊢ a ^ s.card ≤ s.prod

Tactic:
rw [← Multiset.prod_replicate, ← Multiset.map_const]

Premises used: Multiset.prod_replicate, Multiset.map_const
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
a : α
inst_2 : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ (map (Function.const α a) s).prod ≤ s.prod

Tactic:
prod_map_le_prod _ h

Premises used: Multiset.prod_map_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
a : α
inst_2 : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ (map (Function.const α a) s).prod ≤ s.prod

Tactic:
exact prod_map_le_prod _ h

Premises used: Multiset.prod_map_le_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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 α
hps : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ ∀ (a : α), a ∈ l → p a

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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 α
hps : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_of_submultiplicative_on_pred f p h_one hp_one h_mul hp_mul (by simpa)]

Premises used: List.le_prod_of_submultiplicative_on_pred
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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)
s : Multiset α
hps : ∀ (a : α), a ∈ s → p a
h : ∀ (l : List α) (hps : ∀ (a : α), a ∈ ⟦l⟧ → p a), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_of_submultiplicative_on_pred f p h_one hp_one h_mul hp_mul (by simpa)]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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 α
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_of_submultiplicative f h_one h_mul]

Premises used: List.le_prod_of_submultiplicative
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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
s : Multiset α
h : ∀ (l : List α), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_of_submultiplicative f h_one h_mul]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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 α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ l ≠ []

Tactic:
simpa using hs_nonempty
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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 α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ ∀ (a : α), a ∈ l → p a

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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 α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul
      (by simpa using hs_nonempty) (by simpa)]

Premises used: List.le_prod_nonempty_of_submultiplicative_on_pred
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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)
s : Multiset α
hs_nonempty : s ≠ ∅
hs : ∀ (a : α), a ∈ s → p a
h : ∀ (l : List α) (hs_nonempty : ⟦l⟧ ≠ ∅) (hs : ∀ (a : α), a ∈ ⟦l⟧ → p a), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
induction s using Quotient.inductionOn with
  | h l =>
    simp [l.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul
      (by simpa using hs_nonempty) (by simpa)]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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⟧ ≠ ∅
⊢ l ≠ ∅

Tactic:
simpa using hs_nonempty
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
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⟧ ≠ ∅
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_nonempty_of_submultiplicative f h_mul (by simpa using hs_nonempty)]

Premises used: List.le_prod_nonempty_of_submultiplicative
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
inst_2 : Preorder β
inst_3 : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
h : ∀ (l : List α) (hs_nonempty : ⟦l⟧ ≠ ∅), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_nonempty_of_submultiplicative f h_mul (by simpa using hs_nonempty)]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hle : ∀ (i : ι), i ∈ s → f i ≤ g i
hlt : ∃ (i : ι), i ∈ s ∧ f i < g i
mk :
  ∀ (l : List ι)
    (hle :
      ∀ (i : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → f i ≤ g i)
    (hlt :
      ∃ (i : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i ∧ f i < g i),
    (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod <
      (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
⊢ (map f s).prod < (map g s).prod

Tactic:
obtain ⟨l⟩ := s
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
l : List ι
hle :
  ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → f i ≤ g i
hlt :
  ∃ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i ∧ f i < g i
mk : (List.map f l).prod < (List.map g l).prod
⊢ (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod <
    (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod

Tactic:
simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]

Premises used: Multiset.map_coe, Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
l : List ι
hle :
  ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → f i ≤ g i
hlt :
  ∃ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i ∧ f i < g i
⊢ (List.map f l).prod < (List.map g l).prod

Tactic:
List.prod_lt_prod' f g hle hlt

Premises used: List.prod_lt_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
l : List ι
hle :
  ∀ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i → f i ≤ g i
hlt :
  ∃ (i : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l) i ∧ f i < g i
⊢ (List.map f l).prod < (List.map g l).prod

Tactic:
exact List.prod_lt_prod' f g hle hlt

Premises used: List.prod_lt_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ (i : ι), i ∈ s → f i < g i
obtain : ∀ (i : ι) (hi : i ∈ s), (map f s).prod < (map g s).prod
⊢ (map f s).prod < (map g s).prod

Tactic:
obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs

Premises used: Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ (map f s).prod < (map g s).prod

Tactic:
prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩

Premises used: Multiset.prod_lt_prod', le_of_lt, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ (map f s).prod < (map g s).prod

Tactic:
exact prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩

Premises used: Multiset.prod_lt_prod', le_of_lt, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
m : Multiset α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
inst_3 : IsOrderedMonoid α
l : List α
⊢ prod ⟦l⟧ = 1 ↔ ∀ (x : α), x ∈ ⟦l⟧ → x = 1

Tactic:
simpa using List.prod_eq_one_iff

Premises used: List.prod_eq_one_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
m : Multiset α
a : α
ha : a ∈ m
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
obtain : ∀ (t : Multiset α) (ha : a ∈ a ::ₘ t), a ≤ (a ::ₘ t).prod
⊢ a ≤ m.prod

Tactic:
obtain ⟨t, rfl⟩ := exists_cons_of_mem ha

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
a : α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
rw : a ≤ a * t.prod
⊢ a ≤ (a ::ₘ t).prod

Tactic:
rw [prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
a : α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ a * t.prod

Tactic:
_root_.le_mul_right (le_refl a)

Premises used: le_refl, le_mul_right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_2
inst : CommMonoid α
a : α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ a * t.prod

Tactic:
exact _root_.le_mul_right (le_refl a)

Premises used: le_refl, le_mul_right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_4
inst : LinearOrder α
inst_1 : OrderBot α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
h₁ : ∀ (a : List α) (h : ∀ (x : α), x ∈ ⟦a⟧ → x ≤ n), fold max ⊥ ⟦a⟧ ≤ n
⊢ fold max ⊥ l ≤ n

Tactic:
induction l using Quotient.inductionOn
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
α : Type u_4
inst : LinearOrder α
inst_1 : OrderBot α
n : α
a : List α
h : ∀ (x : α), x ∈ ⟦a⟧ → x ≤ n
⊢ fold max ⊥ ⟦a⟧ ≤ n

Tactic:
simpa using List.max_le_of_forall_le _ _ h

Premises used: List.max_le_of_forall_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
mk :
  ∀ (l : List ι),
    max (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
        (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod ≤
      prod (map (fun (i : ι) ↦ max (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))
⊢ max (map f s).prod (map g s).prod ≤ prod (map (fun (i : ι) ↦ max (f i) (g i)) s)

Tactic:
obtain ⟨l⟩ := s
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
mk : max (List.map f l).prod (List.map g l).prod ≤ List.prod (List.map (fun (i : ι) ↦ max (f i) (g i)) l)
⊢ max (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
      (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod ≤
    prod (map (fun (i : ι) ↦ max (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))

Tactic:
simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]

Premises used: Multiset.map_coe, Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (List.map f l).prod (List.map g l).prod ≤ List.prod (List.map (fun (i : ι) ↦ max (f i) (g i)) l)

Tactic:
apply List.max_prod_le

Premises used: List.max_prod_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
mk :
  ∀ (l : List ι),
    prod (map (fun (i : ι) ↦ min (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)) ≤
      min (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
        (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
⊢ prod (map (fun (i : ι) ↦ min (f i) (g i)) s) ≤ min (map f s).prod (map g s).prod

Tactic:
obtain ⟨l⟩ := s
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
mk : List.prod (List.map (fun (i : ι) ↦ min (f i) (g i)) l) ≤ min (List.map f l).prod (List.map g l).prod
⊢ prod (map (fun (i : ι) ↦ min (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)) ≤
    min (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
      (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod

Tactic:
simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]

Premises used: Multiset.map_coe, Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ List.prod (List.map (fun (i : ι) ↦ min (f i) (g i)) l) ≤ min (List.map f l).prod (List.map g l).prod

Tactic:
apply List.prod_min_le

Premises used: List.prod_min_le