awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
nil :
  ∀ (hl_nonempty : Ne.{u_5 + 1} (α := List α) [] []) (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
    f (prod []) ≤ (map f []).prod
⊢ f l.prod ≤ (map f l).prod
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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)
⊢ f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))
have 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)
Tactic: simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ f l.sum ≤ foldr max 0 (map f l)
have nil : f (sum []) ≤ foldr max 0 (map f [])
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)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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 [])
⊢ f l.sum ≤ foldr max 0 (map f l)
have 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))
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)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
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 :: b :: l).prod
have hl₂ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
Tactic: simp only [forall_eq_or_imp, List.mem_cons] at hl₁
Cleared hypotheses: hl₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 1 < (a :: b :: l).prod
have rw : 1 < a * (b :: l).prod
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 1 < a * (b :: l).prod
have apply : 1 ≤ (b :: l).prod
Tactic: apply one_lt_mul_of_lt_of_le' hl₁.1
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ 1 ≤ (b :: l).prod
have apply : ∀ (x : M), x ∈ b :: l → 1 < x
Tactic: apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod
have nil : ∀ (hl₁ : ∀ (x : M), Membership.mem (γ := List M) [] x → 1 ≤ x) (x : M), Membership.mem (γ := List M) [] x → x ≤ prod []
Tactic: induction l
Cleared hypotheses: l, hl₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
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 []
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod
have 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
Tactic: induction l
Cleared hypotheses: l, hl₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
head : M
tail : List M
tail_ih : ∀ (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
have cons : ∀ (hl₁ : 1 ≤ head ∧ ∀ (x : M), x ∈ tail → 1 ≤ x), head ≤ head * tail.prod ∧ ∀ (x : M), x ∈ tail → x ≤ head * tail.prod
Tactic: simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢
Cleared hypotheses: hl₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
head : M
tail : List M
tail_ih : ∀ (hl₁ : ∀ (x : M), x ∈ tail → 1 ≤ x) (x : M), x ∈ tail → x ≤ tail.prod
hl₁ : 1 ≤ head ∧ ∀ (x : M), x ∈ tail → 1 ≤ x
⊢ head ≤ head * tail.prod ∧ ∀ (x : M), x ∈ tail → x ≤ head * tail.prod
have constructor : head ≤ head * tail.prod
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
head : M
tail : List M
tail_ih : ∀ (hl₁ : ∀ (x : M), x ∈ tail → 1 ≤ x) (x : M), x ∈ tail → x ≤ tail.prod
hl₁ : 1 ≤ head ∧ ∀ (x : M), x ∈ tail → 1 ≤ x
constructor : head ≤ head * tail.prod
⊢ head ≤ head * tail.prod ∧ ∀ (x : M), x ∈ tail → x ≤ head * tail.prod
have cons : ∀ (x : M), x ∈ tail → x ≤ head * tail.prod
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedMonoid M
inst_3 : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1
have rw : ℕ
Tactic: rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedMonoid M
inst_3 : CanonicallyOrderedMul M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
rw : ℕ
⊢ l.prod = 1
have rw₁ : l.length = l.length
Tactic: rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
hd : α
tl : List α
IH : f tl.prod ≤ (map f tl).sum
⊢ f (hd :: tl).prod ≤ (map f (hd :: tl)).sum
have cons : f hd + (map f tl).sum ≤ (map f (hd :: tl)).sum
Tactic: grw [prod_cons, h_mul, IH]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f l.prod ≤ (map f l).sum
have nil : f (prod []) ≤ (map f []).sum
Tactic: induction l with
  | nil => simp [h_one]
  | cons hd tl IH => grw [prod_cons, h_mul, IH]; simp
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
nil : f (prod []) ≤ (map f []).sum
⊢ f l.prod ≤ (map f l).sum
have cons : ∀ (hd : α) (tl : List α) (IH : f tl.prod ≤ (map f tl).sum), f (hd :: tl).prod ≤ (map f (hd :: tl)).sum
Tactic: induction l with
  | nil => simp [h_one]
  | cons hd tl IH => grw [prod_cons, h_mul, IH]; simp
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
have rw : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ cons b (Ico a b) sorry, f x
Tactic: rw [Icc_eq_cons_Ico h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
rw : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ cons b (Ico a b) ⋯, f x
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
have rw₁ : f b * ∏ x ∈ Ico a b, f x = f b * ∏ x ∈ Ico a b, f x
Tactic: rw [Icc_eq_cons_Ico h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x
have rw : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
Tactic: rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
rw : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Icc a b, f x) (∏ x ∈ Icc a b, f x)
Tactic: rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
have rw : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ cons a (Ioc a b) sorry, f x
Tactic: rw [Icc_eq_cons_Ioc h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
rw : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ cons a (Ioc a b) ⋯, f x
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
have rw₁ : f a * ∏ x ∈ Ioc a b, f x = f a * ∏ x ∈ Ioc a b, f x
Tactic: rw [Icc_eq_cons_Ioc h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x
have rw : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
Tactic: rw [mul_comm, mul_prod_Ioc_eq_prod_Icc h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a ≤ b
rw : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x
⊢ (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Icc a b, f x) (∏ x ∈ Icc a b, f x)
Tactic: rw [mul_comm, mul_prod_Ioc_eq_prod_Icc h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
⊢ f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x
have rw : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ cons a (Ioo a b) sorry, f x
Tactic: rw [Ico_eq_cons_Ioo h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
rw : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ cons a (Ioo a b) ⋯, f x
⊢ f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x
have rw₁ : f a * ∏ x ∈ Ioo a b, f x = f a * ∏ x ∈ Ioo a b, f x
Tactic: rw [Ico_eq_cons_Ioo h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
⊢ (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x
have rw : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x
Tactic: rw [mul_comm, mul_prod_Ioo_eq_prod_Ico h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
rw : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x
⊢ (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Ico a b, f x) (∏ x ∈ Ico a b, f x)
Tactic: rw [mul_comm, mul_prod_Ioo_eq_prod_Ico h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x
have rw : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ cons b (Ioo a b) sorry, f x
Tactic: rw [Ioc_eq_cons_Ioo h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
rw : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ cons b (Ioo a b) ⋯, f x
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x
have rw₁ : f b * ∏ x ∈ Ioo a b, f x = f b * ∏ x ∈ Ioo a b, f x
Tactic: rw [Ioc_eq_cons_Ioo h, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
⊢ (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x
have rw : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x
Tactic: rw [mul_comm, mul_prod_Ioo_eq_prod_Ioc h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
a b : α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
h : a < b
rw : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x
⊢ (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Ioc a b, f x) (∏ x ∈ Ioc a b, f x)
Tactic: rw [mul_comm, mul_prod_Ioo_eq_prod_Ioc h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k
have ha : a ∉ Ico (a + 1) b
Tactic: have ha : a ∉ Ico (a + 1) b := by simp
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k
have rw : Eq.{u_2 + 1} (α := M) (∏ k ∈ Ico a b, f k) (∏ x ∈ insert a (Ico (a + 1) b), f x)
Tactic: rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
rw : Eq.{u_2 + 1} (α := M) (∏ k ∈ Ico a b, f k) (∏ x ∈ insert a (Ico (a + 1) b), f x)
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ k ∈ Ico a b, f k) (∏ x ∈ Ico a b, f x)
Tactic: rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
have rw : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ cons a (Ioi a) sorry, f x
Tactic: rw [Ici_eq_cons_Ioi, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderTop α
a : α
rw : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ cons a (Ioi a) ⋯, f x
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
have rw₁ : f a * ∏ x ∈ Ioi a, f x = f a * ∏ x ∈ Ioi a, f x
Tactic: rw [Ici_eq_cons_Ioi, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderTop α
a : α
⊢ (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x
have rw : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
Tactic: rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderTop α
a : α
rw : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x
⊢ (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Ici a, f x) (∏ x ∈ Ici a, f x)
Tactic: rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
have rw : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ cons a (Iio a) sorry, f x
Tactic: rw [Iic_eq_cons_Iio, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderBot α
a : α
rw : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ cons a (Iio a) ⋯, f x
⊢ f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
have rw₁ : f a * ∏ x ∈ Iio a, f x = f a * ∏ x ∈ Iio a, f x
Tactic: rw [Iic_eq_cons_Iio, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderBot α
a : α
⊢ (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x
have rw : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
Tactic: rw [mul_comm, mul_prod_Iio_eq_prod_Iic]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
f : α → M
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrderBot α
a : α
rw : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x
⊢ (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Iic a, f x) (∏ x ∈ Iic a, f x)
Tactic: rw [mul_comm, mul_prod_Iio_eq_prod_Iic]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
a b : α
inst_1 : LinearOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : AddMonoidWithOne α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
hab : a ≤ b
f : α → M
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x
have rw : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ insert b (Ico a b), f x
Tactic: rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
a b : α
inst_1 : LinearOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : AddMonoidWithOne α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
hab : a ≤ b
f : α → M
rw : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ insert b (Ico a b), f x
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x
have rw₁ : (∏ x ∈ Ico a b, f x) * f b = f b * ∏ x ∈ Ico a b, f x
Tactic: rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite (goal)
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
a b : α
inst_1 : LinearOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : AddMonoidWithOne α
inst_4 : SuccAddOrder α
inst_5 : NoMaxOrder α
hab : a ≤ b
f : α → M
rw : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ insert b (Ico a b), f x
rw₁ : (∏ x ∈ Ico a b, f x) * f b = f b * ∏ x ∈ Ico a b, f x
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x
have rw₂ : f b * ∏ x ∈ Ico a b, f x = f b * ∏ x ∈ Ico a b, f x
Tactic: rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]
-- 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) (∏ i : α, ∏ j ∈ Ioi i, f j i * f i j) (∏ i : α, ∏ j ∈ {i}ᶜ, f j i)
have simp_rw : HMul.hMul (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) (∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1) =
  HMul.hMul (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) (∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x)
Tactic: simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]
-- 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
⊢ HMul.hMul (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) (∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1) =
    HMul.hMul (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) (∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x)
have e_a : Eq.{u_2 + 1} (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1) (∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x)
Tactic: congr 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
⊢ Eq.{u_2 + 1} (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1) (∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x)
have e_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 : α) ↦ α)))
Tactic: rw [prod_sigma', prod_sigma']