awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ (l.insertIdx i a).prod = a * l.prod
have 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
Tactic: induction i generalizing l
Cleared hypotheses: l, i, hlen, hcomm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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'
⊢ (l.insertIdx (i + 1) a).prod = a * l.prod
have 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
Tactic: obtain ⟨hd, tl, rfl⟩ := exists_cons_of_length_pos (Nat.zero_lt_of_lt hlen)
Cleared hypotheses: l, hlen, hcomm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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 :: tl).insertIdx (i + 1) a).prod = a * (hd :: tl).prod
have simp : hd * (a * tl.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))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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)
⊢ a' ∈ take i l
have rwa : ∀ (a'_mem : 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
Cleared hypotheses: a'_mem
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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'
⊢ getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen * (l.eraseIdx i).prod = l.prod
have rw : ((l.eraseIdx i).insertIdx i (getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen)).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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l i hlen * (l.eraseIdx i).prod = l.prod
have rw₁ : l.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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : BEq M
inst_2 : LawfulBEq M
l : List M
⊢ (filter (fun (x : M) ↦ x != 1) l).prod = l.prod
have nil : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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 [])
⊢ (filter (fun (x : M) ↦ x != 1) l).prod = l.prod
have 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
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : BEq M
inst_2 : LawfulBEq M
l : List M
⊢ (filter (fun (x : M) ↦ x != 1) l).prod = l.prod
have nil : Eq.{u_4 + 1} (α := M) (prod (filter (fun (x : M) ↦ x != 1) [])) (prod [])
Tactic: classical induction l <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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 [])
⊢ (filter (fun (x : M) ↦ x != 1) l).prod = l.prod
have 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
Tactic: classical induction l <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq α
f : α → M
a b : α
l : List α
h : a ∈ b :: l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
have inl : ∀ (h : a ∈ a :: l), f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod
Tactic: obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
have inr : ∀ (ne : a ≠ b) (h : a ∈ l), 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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ (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
have 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
Tactic: simp only [drop, zipWith_cons_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| 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
have lhs : x * xs.prod * (y * ys.prod)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod)
have rw : x * (xs.prod * (y * ys.prod))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * (xs.prod * (y * ys.prod))
have right : xs.prod * (y * ys.prod)
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| xs.prod * (y * ys.prod)
have rw : y * (ys.prod * xs.prod)
Tactic: rw [mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| y * (ys.prod * xs.prod)
have right : ys.prod * xs.prod
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| ys.prod * xs.prod
have rw : prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) xs ys) * (drop ys.length xs).prod * (drop xs.length ys).prod
Tactic: rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| 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
have rw : 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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ l.prod * l'.prod = prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')
have 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')
Tactic: apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ 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')
have 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')
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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')
⊢ 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')
have rw₆ : Eq (α := M) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l')) (prod (zipWith (fun (x1 x2 : M) ↦ x1 * x2) l l'))
Tactic: rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ 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
have 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
Tactic: simp only [map_cons, filter_cons, prod_cons] at ih ⊢
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
x : α
xs : List α
⊢ (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
have 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
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ (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
have 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
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
l : List α
⊢ prod (map (fun (a : α) ↦ if p a then f a else g a) l) =
    (map f (filter (fun (b : α) ↦ decide (p b)) l)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) l)).prod
have nil : 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: induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, filter_cons, prod_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : p x
    · simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]
    · simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true,
      decide_true, map_cons, prod_cons, mul_left_comm]
Cleared hypotheses: l