awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : ¬a' = a
neg : 1 * f a ^ count a as = f a ^ (count a as + 0)
neg₁ : f a ^ count a as = f a ^ (count a as + 0)
neg₂ neg₃ : f a ^ count a as = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
rw [hf a' ha' mem_cons_self, one_mul, add_zero]

Premises used: List.mem_cons_self, add_zero, one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
l : List α
a : α
f : α → M
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
nil :
  ∀ (a : α) (hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1),
    (map f []).prod = f a ^ count a []
cons :
  ∀ (a' : α) (as : List α)
    (h : ∀ (a : α) (hf : ∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1), (map f as).prod = f a ^ count a as) (a : α)
    (hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1), (map f (a' :: as)).prod = f a ^ count a (a' :: as)
⊢ (map f l).prod = f a ^ count a l

Tactic:
induction l generalizing a with
  | nil => rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
  | cons a' as h =>
    specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
    rw [List.map_cons, List.prod_cons, count_cons, h]
    simp only [beq_iff_eq]
    split_ifs with ha'
    · rw [ha', _root_.pow_succ']
    · rw [hf a' ha' mem_cons_self, one_mul, add_zero]

Premises used: List.map_cons, beq_iff_eq, List.count_cons, pow_zero, List.cons, List.count_nil, List.prod_nil, add_zero, List.prod_cons, pow_succ', one_mul, List.map_nil, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
inst_1 : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
rw rw₁ : l.prod = l.prod
⊢ l.prod = (map id l).prod

Tactic:
rw [map_id]

Premises used: List.map_id
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
a : M
i : ℕ
hlen : i ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'
induction :
  ∀ {l : List M} (hlen : 0 ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take 0 l → Commute a a'),
    (l.insertIdx 0 a).prod = a * l.prod
succ :
  ∀ (n : ℕ),
    (∀ {l : List M} (hlen : n ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take n l → Commute a a'),
        (l.insertIdx n a).prod = a * l.prod) →
      ∀ {l : List M} (hlen : n + 1 ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take (n + 1) l → Commute a a'),
        (l.insertIdx (n + 1) a).prod = a * l.prod
⊢ (l.insertIdx i a).prod = a * l.prod

Tactic:
induction i generalizing l
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
l : List M
hlen : 0 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take 0 l → Commute a a'
⊢ (l.insertIdx 0 a).prod = a * l.prod

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
l : List M
hlen : 0 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take 0 l → Commute a a'
⊢ (l.insertIdx 0 a).prod = a * l.prod

Tactic:
case zero => rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
i : ℕ
ih :
  ∀ {l : List M} (hlen : i ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'),
    (l.insertIdx i a).prod = a * l.prod
l : List M
hlen : i + 1 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) l → Commute a a'
obtain :
  ∀ (hd : M) (tl : List M) (hlen : i + 1 ≤ (hd :: tl).length)
    (hcomm : ∀ (a' : M), a' ∈ take (i + 1) (hd :: tl) → Commute a a'),
    ((hd :: tl).insertIdx (i + 1) a).prod = a * (hd :: tl).prod
⊢ (l.insertIdx (i + 1) a).prod = a * l.prod

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_length_pos (Nat.zero_lt_of_lt hlen)

Premises used: List.exists_cons_of_length_pos, Nat.zero_lt_of_lt, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
i : ℕ
ih :
  ∀ {l : List M} (hlen : i ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'),
    (l.insertIdx i a).prod = a * l.prod
hd : M
tl : List M
hlen : i + 1 ≤ (hd :: tl).length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) (hd :: tl) → Commute a a'
simp : hd * (a * tl.prod) = a * (hd * tl.prod)
⊢ ((hd :: tl).insertIdx (i + 1) a).prod = a * (hd :: tl).prod

Tactic:
simp only [insertIdx_succ_cons, prod_cons,
      ih (Nat.le_of_lt_succ hlen) (fun a' a'_mem => hcomm a' (mem_of_mem_tail a'_mem))]

Premises used: List.insertIdx_succ_cons, List.mem_of_mem_tail, Nat.le_of_lt_succ, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
i : ℕ
ih :
  ∀ {l : List M} (hlen : i ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'),
    (l.insertIdx i a).prod = a * l.prod
hd : M
tl : List M
hlen : i + 1 ≤ (hd :: tl).length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) (hd :: tl) → Commute a a'
⊢ hd * (a * tl.prod) = a * (hd * tl.prod)

Tactic:
Commute.left_comm (hcomm hd (mem_of_mem_head? rfl)).symm tl.prod

Premises used: Commute.left_comm, List.mem_of_mem_head?, Commute.symm, rfl, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
a : M
i : ℕ
ih :
  ∀ {l : List M} (hlen : i ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'),
    (l.insertIdx i a).prod = a * l.prod
hd : M
tl : List M
hlen : i + 1 ≤ (hd :: tl).length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) (hd :: tl) → Commute a a'
⊢ hd * (a * tl.prod) = a * (hd * tl.prod)

Tactic:
exact Commute.left_comm (hcomm hd (mem_of_mem_head? rfl)).symm tl.prod

Premises used: Commute.left_comm, List.mem_of_mem_head?, Commute.symm, rfl, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute (getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen) a'
⊢ i ≤ (l.eraseIdx i).length

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute (getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen) a'
a' : M
a'_mem : a' ∈ take i (l.eraseIdx i)
rwa rwa₁ rwa₂ rwa₃ : ∀ (a'_mem : a' ∈ take i l), a' ∈ take i l
⊢ a' ∈ take i l

Tactic:
rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem

Premises used: List.take_eraseIdx_eq_take_of_le, Nat.le_refl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute (getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen) a'
rw : ((l.eraseIdx i).insertIdx i (getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen)).prod = l.prod
rw₁ rw₂ : l.prod = l.prod
⊢ getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen * (l.eraseIdx i).prod = l.prod

Tactic:
rw [← prod_insertIdx (by grind : i ≤ (l.eraseIdx i).length) (fun a' a'_mem =>
      hcomm a' (by rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem)),
    insertIdx_eraseIdx_getElem hlen]

Premises used: List.insertIdx_eraseIdx_getElem, List.prod_insertIdx
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : BEq M
inst_2 : LawfulBEq M
l : List M
nil : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
cons :
  ∀ (head : M) (tail : List M),
    (filter (fun (x : M) ↦ x != 1) tail).prod = tail.prod →
      (filter (fun (x : M) ↦ x != 1) (head :: tail)).prod = (head :: tail).prod
⊢ (filter (fun (x : M) ↦ x != 1) l).prod = l.prod

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : BEq M
inst_2 : LawfulBEq M
⊢ Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : BEq M
inst_2 : LawfulBEq M
head : M
tail : List M
tail_ih : (filter (fun (x : M) ↦ x != 1) tail).prod = tail.prod
⊢ (filter (fun (x : M) ↦ x != 1) (head :: tail)).prod = (head :: tail).prod

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : BEq M
inst_2 : LawfulBEq M
l : List M
nil : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
cons :
  ∀ (head : M) (tail : List M),
    (filter (fun (x : M) ↦ x != 1) tail).prod = tail.prod →
      (filter (fun (x : M) ↦ x != 1) (head :: tail)).prod = (head :: tail).prod
nil₁ : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
cons₁ :
  ∀ (head : M) (tail : List M),
    (filter (fun (x : M) ↦ x != 1) tail).prod = tail.prod →
      (filter (fun (x : M) ↦ x != 1) (head :: tail)).prod = (head :: tail).prod
nil₂ : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
cons₂ :
  ∀ (head : M) (tail : List M),
    (filter (fun (x : M) ↦ x != 1) tail).prod = tail.prod →
      (filter (fun (x : M) ↦ x != 1) (head :: tail)).prod = (head :: tail).prod
nil₃ : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
cons₃ :
  ∀ (head : M) (tail : List M),
    (filter (fun (x : M) ↦ x != 1) tail).prod = tail.prod →
      (filter (fun (x : M) ↦ x != 1) (head :: tail)).prod = (head :: tail).prod
⊢ (filter (fun (x : M) ↦ x != 1) l).prod = l.prod

Tactic:
classical induction l <;> grind
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
i : ℕ
h : i ≤ l.length
⊢ (l.insertIdx i a).prod = a * l.prod

Tactic:
List.prod_insertIdx h (fun a' _ ↦ Commute.all a a')

Premises used: List.prod_insertIdx, Commute.all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
l : List M
i : ℕ
h : i < l.length
⊢ getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i h * (l.eraseIdx i).prod = l.prod

Tactic:
List.mul_prod_eraseIdx h (fun a' _ ↦ Commute.all l[i] a')

Premises used: GetElem.getElem, List.mul_prod_eraseIdx, Commute.all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
inst_1 : DecidableEq M
ha : a ∈ l
⊢ a * (l.erase a).prod = l.prod

Tactic:
prod_erase_of_comm ha fun x _ y _ ↦ mul_comm x y

Premises used: mul_comm, List.prod_erase_of_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq α
f : α → M
a b : α
l : List α
h : a ∈ b :: l
inl : ∀ (h : a ∈ a :: l), f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod
inr : ∀ (ne : a ≠ b) (h : a ∈ l), f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h

Premises used: List.eq_or_ne_mem_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

Tactic:
simp only [map, erase_cons_head, prod_cons]

Premises used: List.map, List.erase_cons_head, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq α
f : α → M
a b : α
l : List α
h_1 : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
simp only [map, erase_cons_tail (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
        mul_left_comm (f a) (f b)]

Premises used: not_beq_of_ne, List.map, List.erase_cons_tail, Ne.symm, mul_left_comm, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ ~ l₂
⊢ l₁.prod = l₂.prod

Tactic:
h.foldr_op_eq

Premises used: List.Perm.foldr_op_eq, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
inst : One α
inst_1 : Mul α
inst_2 : Std.Associative fun (x1 x2 : α) ↦ x1 * x2
inst_3 : Std.Commutative fun (x1 x2 : α) ↦ x1 * x2
inst_4 : Std.LawfulLeftIdentity (fun (x1 x2 : α) ↦ x1 * x2) 1
l : List α
⊢ l.reverse.prod = l.prod

Tactic:
@List.sum_reverse α ⟨1⟩ ⟨(· * ·)⟩ _ _ _ l

Premises used: List.sum_reverse, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
ys : List M
⊢ prod [] * ys.prod =
    HMul.hMul (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) [] ys)) (prod (drop ys.length [])) *
      (drop (length.{u_4} (α := M) []) ys).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
xs : List M
⊢ xs.prod * prod [] =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs []) * (drop (length.{u_4} (α := M) []) xs).prod *
      prod (drop xs.length [])

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
simp :
  x * xs.prod * (y * ys.prod) =
    x * y * prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod
⊢ (x :: xs).prod * (y :: ys).prod =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) (x :: xs) (y :: ys)) * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
simp only [drop, zipWith_cons_cons, prod_cons]

Premises used: List.drop, List.zipWith_cons_cons, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
lhs : x * xs.prod * (y * ys.prod)
| x * xs.prod * (y * ys.prod) =
    x * y * prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod

Tactic:
lhs
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
rw : x * (xs.prod * (y * ys.prod))
| x * xs.prod * (y * ys.prod)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
right : xs.prod * (y * ys.prod)
| x * (xs.prod * (y * ys.prod))

Tactic:
right
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
rw : y * (ys.prod * xs.prod)
| xs.prod * (y * ys.prod)

Tactic:
rw [mul_comm, mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
right : ys.prod * xs.prod
| y * (ys.prod * xs.prod)

Tactic:
right
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
rw : prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod
| ys.prod * xs.prod

Tactic:
rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Premises used: mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
rw : prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod
| x * xs.prod * (y * ys.prod) =
    x * y * prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod

Tactic:
lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
conv :
  x * (y * (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod)) =
    x * y * prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod
⊢ x * xs.prod * (y * ys.prod) =
    x * y * prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod

Tactic:
conv =>
      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ x * (y * (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod)) =
    x * y * prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
l l' : List M
h : l.length = l'.length
apply :
  prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l') * (drop l'.length l).prod * (drop l.length l').prod =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
⊢ l.prod * l'.prod = prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')

Tactic:
apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans

Premises used: List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : CommMonoid M
l l' : List M
h : l.length = l'.length
rw :
  prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l') * (drop l.length l).prod * (drop l.length l').prod =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
rw₁ :
  HMul.hMul (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) (prod []) * (drop l.length l').prod =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
rw₂ :
  HMul.hMul (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) (prod []) * (drop l'.length l').prod =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
rw₃ :
  HMul.hMul (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) (prod []) * prod [] =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
rw₄ :
  HMul.hMul (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) 1 * 1 =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
rw₅ :
  HMul.hMul (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) 1 =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
rw₆ rw₇ :
  Eq (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l'))
⊢ prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l') * (drop l'.length l).prod * (drop l.length l').prod =
    prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')

Tactic:
rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]

Premises used: List.prod_nil, mul_one, List.drop_length
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
⊢ prod (map (fun (a : α) ↦ if p a then f a else g a) []) =
    (map f (filter (fun (b : α) ↦ decide (p b)) [])).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) [])).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  prod (map (fun (a : α) ↦ if p a then f a else g a) xs) =
    (map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod
cons :
  (if p x then f x else g x) * prod (map (fun (a : α) ↦ if p a then f a else g a) xs) =
    (map f
          (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
          else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
          else filter (fun (a : α) ↦ decide ¬p a) xs)).prod
⊢ prod (map (fun (a : α) ↦ if p a then f a else g a) (x :: xs)) =
    (map f (filter (fun (b : α) ↦ decide (p b)) (x :: xs))).prod *
      (map g (filter (fun (a : α) ↦ decide ¬p a) (x :: xs))).prod

Tactic:
simp only [map_cons, filter_cons, prod_cons] at ih ⊢

Premises used: List.map_cons, List.filter_cons, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  prod (map (fun (a : α) ↦ if p a then f a else g a) xs) =
    (map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod
cons :
  (if p x then f x else g x) *
      ((map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
          else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
          else filter (fun (a : α) ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) * prod (map (fun (a : α) ↦ if p a then f a else g a) xs) =
    (map f
          (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
          else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
          else filter (fun (a : α) ↦ decide ¬p a) xs)).prod

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
x : α
xs : List α
pos :
  ∀ (hx : p x),
    (if p x then f x else g x) *
        ((map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod) =
      (map f
            (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
            else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
        (map g
            (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
            else filter (fun (a : α) ↦ decide ¬p a) xs)).prod
neg :
  ∀ (hx : ¬p x),
    (if p x then f x else g x) *
        ((map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod) =
      (map f
            (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
            else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
        (map g
            (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
            else filter (fun (a : α) ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
          else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
          else filter (fun (a : α) ↦ decide ¬p a) xs)).prod

Tactic:
by_cases hx : p x
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
          else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
          else filter (fun (a : α) ↦ decide ¬p a) xs)).prod

Tactic:
simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]

Premises used: List.map_cons, mul_assoc, Bool.false_eq_true, not_true_eq_false, decide_false, decide_not, decide_true, reduceIte, List.prod_cons