awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : LinearOrder α
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderTop α
inst_4 : LocallyFiniteOrderBot α
f : α → α → M
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Ioi,
      f (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)))
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Iio,
      f (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)))
have e_a : ∀ (a : (_ : α) × α),
  Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio)
      ((fun (i : (_ : α) × α) ↦
          (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) : (_ : α) × α))
        a)
Tactic: refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : LinearOrder α
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderTop α
inst_4 : LocallyFiniteOrderBot α
f : α → α → M
e_a :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Ioi,
      f (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)))
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Iio,
      f (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)))
have e_a₁ : ∀ (a : (_ : α) × α),
  Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio) a →
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi)
      ((fun (i : (_ : α) × α) ↦
          (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) : (_ : α) × α))
        a)
Tactic: refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : LinearOrder α
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderTop α
inst_4 : LocallyFiniteOrderBot α
f : α → α → M
e_a :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
e_a₁ :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Ioi,
      f (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)))
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Iio,
      f (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)))
have e_a₂ : ∀ (a : (_ : α) × α),
  Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
    (fun (i : (_ : α) × α) ↦
          (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) : (_ : α) × α))
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a) =
      a
Tactic: refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : LinearOrder α
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderTop α
inst_4 : LocallyFiniteOrderBot α
f : α → α → M
e_a :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
e_a₁ :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
e_a₂ :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
      (fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          ((fun (i : (_ : α) × α) ↦
              (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
                (_ : α) × α))
            a) =
        a
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Ioi,
      f (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)))
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Iio,
      f (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)))
have e_a₃ : ∀ (a : (_ : α) × α),
  Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio) a →
    (fun (i : (_ : α) × α) ↦
          (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) : (_ : α) × α))
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a) =
      a
Tactic: refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : LinearOrder α
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderTop α
inst_4 : LocallyFiniteOrderBot α
f : α → α → M
e_a :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
e_a₁ :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio) a →
      Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi)
        ((fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          a)
e_a₂ :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
      (fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          ((fun (i : (_ : α) × α) ↦
              (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
                (_ : α) × α))
            a) =
        a
e_a₃ :
  ∀ (a : (_ : α) × α),
    Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Iio) a →
      (fun (i : (_ : α) × α) ↦
            (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
              (_ : α) × α))
          ((fun (i : (_ : α) × α) ↦
              (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
                (_ : α) × α))
            a) =
        a
⊢ Eq.{u_2 + 1} (α := M)
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Ioi,
      f (x.fst (β := fun (i : α) ↦ α)) (x.snd (β := fun (i : α) ↦ α)))
    (∏ x ∈ Finset.sigma (α := fun (a : α) ↦ α) univ Iio,
      f (x.snd (β := fun (i : α) ↦ α)) (x.fst (β := fun (i : α) ↦ α)))
have e_a₄ : ∀ (a : (_ : α) × α),
  Membership.mem (γ := Finset ((_ : α) × α)) (Finset.sigma (α := fun (a : α) ↦ α) univ Ioi) a →
    f (a.fst (β := fun (i : α) ↦ α)) (a.snd (β := fun (i : α) ↦ α)) =
      f
        (Sigma.snd (β := fun (i : α) ↦ α)
          ((fun (i : (_ : α) × α) ↦
              (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
                (_ : α) × α))
            a))
        (Sigma.fst (β := fun (i : α) ↦ α)
          ((fun (i : (_ : α) × α) ↦
              (Sigma.mk (β := fun (i : α) ↦ α) (i.snd (β := fun (i : α) ↦ α)) (i.fst (β := fun (i : α) ↦ α)) :
                (_ : α) × α))
            a))
Tactic: refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ s n, g i
have rw : HMul.hMul (α := β) (∏ x ∈ disjointed s 0, g x) (∏ k ∈ range n, ∏ x ∈ disjointed s (k + 1), g x)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
⊢ ∏ i ∈ s n, g i = HMul.hMul (α := β) (∏ i ∈ s 0, g i) (∏ i ∈ range n, ∏ j ∈ s (i + 1) \ s i, g j)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
⊢ 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)
have refine_1 : disjointed s 0 = s 0
Tactic: congrm (∏ x ∈ ?_, g x) * ∏ k ∈ range n, ∏ x ∈ s (k + 1) \ ?_, g x
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
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
⊢ 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)
have refine_2 : ∀ (k : ℕ), (Iio (k + 1)).sup s = s k
Tactic: congrm (∏ x ∈ ?_, g x) * ∏ k ∈ range n, ∏ x ∈ s (k + 1) \ ?_, g x
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iio (k + 1)).sup s = s k
have refine_2 : (Iic k).sup (s ∘ id) = s k
Tactic: change (Iic k).sup (s ∘ id) = s k
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_3
β : Type u_4
inst : DecidableEq α
inst_1 : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iic k).sup (s ∘ id) = s k
have refine_2 : s ((Iic k).sup id) = s k
Tactic: rw [← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic, sup_Iic]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
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
⊢ (Iic k).sup (s ∘ id) = s k
have refine_2₁ : s k = s k
Tactic: rw [← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic, sup_Iic]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : MulLeftMono α
s : Multiset α
n : α
h : ∀ (x : α), x ∈ s → x ≤ n
⊢ s.prod ≤ n ^ s.card
have h₁ : ∀ (a : List α) (h : ∀ (x : α), x ∈ ⟦a⟧ → x ≤ n), prod ⟦a⟧ ≤ n ^ card ⟦a⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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
have cons : a * as.prod ≤ b * bs.prod
Tactic: rw [prod_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s t : Multiset α
inst_2 : MulLeftMono α
h : Rel (fun (x1 x2 : α) ↦ x1 ≤ x2) s t
⊢ s.prod ≤ t.prod
have zero : LE.le.{u_2} (α := α) (prod 0) (prod 0)
Tactic: induction h with
  | zero => rfl
  | cons rh _ rt =>
    rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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)
⊢ s.prod ≤ t.prod
have 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
Tactic: induction h with
  | zero => rfl
  | cons rh _ rt =>
    rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
s : Multiset α
a : α
inst_2 : MulLeftMono α
h : ∀ (x : α), x ∈ s → a ≤ x
⊢ a ^ s.card ≤ s.prod
have rw : (map (Function.const α a) s).prod ≤ s.prod
Tactic: rw [← Multiset.prod_replicate, ← Multiset.map_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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
⊢ f s.prod ≤ (map f s).prod
have h : ∀ (l : List α) (hps : ∀ (a : α), a ∈ ⟦l⟧ → p a), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).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)]
Cleared hypotheses: s, hps
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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 α
⊢ f s.prod ≤ (map f s).prod
have h : ∀ (l : List α), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod
Tactic: induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_of_submultiplicative f h_one h_mul]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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
⊢ f s.prod ≤ (map f s).prod
have h : ∀ (l : List α) (hs_nonempty : ⟦l⟧ ≠ ∅) (hs : ∀ (a : α), a ∈ ⟦l⟧ → p a), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).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)]
Cleared hypotheses: s, hs_nonempty, hs
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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 ≠ ∅
⊢ f s.prod ≤ (map f s).prod
have h : ∀ (l : List α) (hs_nonempty : ⟦l⟧ ≠ ∅), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).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)]
Cleared hypotheses: s, hs_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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
⊢ (map f s).prod < (map g s).prod
have 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
Tactic: obtain ⟨l⟩ := s
Cleared hypotheses: hle, hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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
⊢ (map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod <
    (map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)).prod
have mk : (List.map f l).prod < (List.map g l).prod
Tactic: simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
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
⊢ (map f s).prod < (map g s).prod
have obtain : ∀ (i : ι) (hi : i ∈ s), (map f s).prod < (map g s).prod
Tactic: obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_2
inst : CommMonoid α
m : Multiset α
a : α
ha : a ∈ m
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
⊢ a ≤ m.prod
have obtain : ∀ (t : Multiset α) (ha : a ∈ a ::ₘ t), a ≤ (a ::ₘ t).prod
Tactic: obtain ⟨t, rfl⟩ := exists_cons_of_mem ha
Cleared hypotheses: m, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_2
inst : CommMonoid α
a : α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
t : Multiset α
ha : a ∈ a ::ₘ t
⊢ a ≤ (a ::ₘ t).prod
have rw : a ≤ a * t.prod
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_4
inst : LinearOrder α
inst_1 : OrderBot α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
⊢ fold max ⊥ l ≤ n
have h₁ : ∀ (a : List α) (h : ∀ (x : α), x ∈ ⟦a⟧ → x ≤ n), fold max ⊥ ⟦a⟧ ≤ n
Tactic: induction l using Quotient.inductionOn
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
⊢ max (map f s).prod (map g s).prod ≤ prod (map (fun (i : ι) ↦ max (f i) (g i)) s)
have 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))
Tactic: obtain ⟨l⟩ := s
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
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))
have mk : max (List.map f l).prod (List.map g l).prod ≤ List.prod (List.map (fun (i : ι) ↦ max (f i) (g i)) l)
Tactic: simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
⊢ prod (map (fun (i : ι) ↦ min (f i) (g i)) s) ≤ min (map f s).prod (map g s).prod
have 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
Tactic: obtain ⟨l⟩ := s
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
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
have mk : List.prod (List.map (fun (i : ι) ↦ min (f i) (g i)) l) ≤ min (List.map f l).prod (List.map g l).prod
Tactic: simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Multiset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : AddCommMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
m : Multiset α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f m.prod ≤ (map f m).sum
have h : ∀ (l : List α), f (prod ⟦l⟧) ≤ (map f ⟦l⟧).sum
Tactic: induction m using Quotient.inductionOn with
  | h l => simp [l.apply_prod_le_sum_map _ h_one h_mul]