awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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
cons :
  ∀ (hl₁ : 1 ≤ head ∧ ∀ (x : M), x ∈ tail → 1 ≤ x), head ≤ head * tail.prod ∧ ∀ (x : M), x ∈ tail → x ≤ head * tail.prod
⊢ ∀ (x : M), x ∈ head :: tail → x ≤ (head :: tail).prod

Tactic:
simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢

Premises used: List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
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
cons : ∀ (x : M), x ∈ tail → x ≤ head * tail.prod
⊢ head ≤ head * tail.prod ∧ ∀ (x : M), x ∈ tail → x ≤ head * tail.prod

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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

Tactic:
le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

Premises used: And.right, List.one_le_prod_of_one_le, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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

Tactic:
exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

Premises used: And.right, List.one_le_prod_of_one_le, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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

Tactic:
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

Premises used: And.right, List.one_le_prod_of_one_le, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
hd : M
tl : List M
ih : ∀ (hl₁ : ∀ (x : M), x ∈ tl → 1 ≤ x) (x : M), x ∈ tl → x ≤ tl.prod
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * tl.prod

Tactic:
fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

Premises used: le_mul_of_one_le_of_le, And.right, And.left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
hd : M
tl : List M
ih : ∀ (hl₁ : ∀ (x : M), x ∈ tl → 1 ≤ x) (x : M), x ∈ tl → x ≤ tl.prod
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * tl.prod

Tactic:
exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

Premises used: le_mul_of_one_le_of_le, And.right, And.left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
M : Type u_3
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
hl₂ : l.prod = 1
x : M
hx : x ∈ l
⊢ x = 1

Tactic:
_root_.le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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 : ℕ
rw₁ : l.length = l.length
⊢ l.prod = 1

Tactic:
rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]

Premises used: Iff.mpr, one_pow, And.intro, List.eq_replicate_iff, List.prod_replicate
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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
⊢ ℕ

Tactic:
exact (length l)

Premises used: List.length
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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.length = l.length

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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 (prod []) ≤ (map f []).sum

Tactic:
simp [h_one]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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
cons : f hd + (map f tl).sum ≤ (map f (hd :: tl)).sum
⊢ f (hd :: tl).prod ≤ (map f (hd :: tl)).sum

Tactic:
grw [prod_cons, h_mul, IH]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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 + (map f tl).sum ≤ (map f (hd :: tl)).sum

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
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
cons : ∀ (hd : α) (tl : List α) (IH : f tl.prod ≤ (map f tl).sum), f (hd :: tl).prod ≤ (map f (hd :: tl)).sum
⊢ f l.prod ≤ (map f l).sum

Tactic:
induction l with
  | nil => simp [h_one]
  | cons hd tl IH => grw [prod_cons, h_mul, IH]; simp

Premises used: List.cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.Order.BigOperators.Group.List
Goal:
α : Type u_5
β : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : Preorder β
inst_3 : AddLeftMono β
l : List α
f : α → β
h_one : 0 ≤ f 1
h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)
⊢ (map f l).sum ≤ f l.prod

Tactic:
apply_prod_le_sum_map (β := βᵒᵈ) l f h_one h_mul

Premises used: List.apply_prod_le_sum_map, OrderDual
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : f b * ∏ x ∈ Ico a b, f x = f b * ∏ x ∈ Ico a b, f x
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ico h, prod_cons]

Premises used: Finset.prod_cons, Finset.Icc_eq_cons_Ico
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Icc a b, f x) (∏ x ∈ Icc a b, f x)
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]

Premises used: Finset.mul_prod_Ico_eq_prod_Icc, mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : f a * ∏ x ∈ Ioc a b, f x = f a * ∏ x ∈ Ioc a b, f x
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ioc h, prod_cons]

Premises used: Finset.Icc_eq_cons_Ioc, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Icc a b, f x) (∏ x ∈ Icc a b, f x)
⊢ (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ioc_eq_prod_Icc h]

Premises used: Finset.mul_prod_Ioc_eq_prod_Icc, mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : f a * ∏ x ∈ Ioo a b, f x = f a * ∏ x ∈ Ioo a b, f x
⊢ f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

Tactic:
rw [Ico_eq_cons_Ioo h, prod_cons]

Premises used: Finset.prod_cons, Finset.Ico_eq_cons_Ioo
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Ico a b, f x) (∏ x ∈ Ico a b, f x)
⊢ (∏ x ∈ Ioo a b, f x) * f a = ∏ x ∈ Ico a b, f x

Tactic:
rw [mul_comm, mul_prod_Ioo_eq_prod_Ico h]

Premises used: Finset.mul_prod_Ioo_eq_prod_Ico, mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : f b * ∏ x ∈ Ioo a b, f x = f b * ∏ x ∈ Ioo a b, f x
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Tactic:
rw [Ioc_eq_cons_Ioo h, prod_cons]

Premises used: Finset.Ioc_eq_cons_Ioo, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Ioc a b, f x) (∏ x ∈ Ioc a b, f x)
⊢ (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ioo_eq_prod_Ioc h]

Premises used: Finset.mul_prod_Ioo_eq_prod_Ioc, mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ a ∉ Ico (a + 1) b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ a ∉ Ico (a + 1) b

Tactic:
have ha : a ∉ Ico (a + 1) b := by simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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)
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ k ∈ Ico a b, f k) (∏ x ∈ Ico a b, f x)
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]

Premises used: Finset.insert_Ico_add_one_left_eq_Ico, Finset.prod_insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : f a * ∏ x ∈ Ioi a, f x = f a * ∏ x ∈ Ioi a, f x
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Tactic:
rw [Ici_eq_cons_Ioi, prod_cons]

Premises used: Finset.Ici_eq_cons_Ioi, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Ici a, f x) (∏ x ∈ Ici a, f x)
⊢ (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Tactic:
rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]

Premises used: Finset.mul_prod_Ioi_eq_prod_Ici, mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : f a * ∏ x ∈ Iio a, f x = f a * ∏ x ∈ Iio a, f x
⊢ f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x

Tactic:
rw [Iic_eq_cons_Iio, prod_cons]

Premises used: Finset.Iic_eq_cons_Iio, Finset.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ x ∈ Iic a, f x) (∏ x ∈ Iic a, f x)
⊢ (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Tactic:
rw [mul_comm, mul_prod_Iio_eq_prod_Iic]

Premises used: mul_comm, Finset.mul_prod_Iio_eq_prod_Iic
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
rw₂ rw₃ : f b * ∏ x ∈ Ico a b, f x = f b * ∏ x ∈ Ico a b, f x
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

Premises used: Finset.prod_insert, Finset.right_notMem_Ico, Finset.insert_Ico_right_eq_Ico_add_one, mul_comm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
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)
⊢ Eq.{u_2 + 1} (α := M) (∏ i : α, ∏ j ∈ Ioi i, f j i * f i j) (∏ i : α, ∏ j ∈ {i}ᶜ, f j i)

Tactic:
simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]

Premises used: Finset.Ioi_disjUnion_Iio, Finset.prod_mul_distrib, Finset.prod_disjUnion
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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 : Eq.{u_2 + 1} (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1) (∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x)
⊢ 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:
congr 1
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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 :
  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 : α) ↦ α)))
⊢ Eq.{u_2 + 1} (α := M) (∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1) (∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x)

Tactic:
rw [prod_sigma', prod_sigma']

Premises used: Finset.prod_sigma'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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 : α) ↦ α)))

Tactic:
prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Sigma.fst, Sigma.mk, Finset.prod_nbij', Sigma.snd
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
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))
⊢ 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:
refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Finset.prod_nbij'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
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
⊢ ∀ (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:
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 : ℕ
rw : HMul.hMul (α := β) (∏ x ∈ disjointed s 0, g x) (∏ k ∈ range n, ∏ x ∈ disjointed s (k + 1), g x)
| ∏ i ∈ s n, g i

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]

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