awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl_1 : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
nil : ∀ (x : ι) (hl : [x] ≠ []), prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) [x]) = f (map f₁ [x]).prod (map f₂ [x]).prod
cons :
  ∀ (head : ι) (tail : List ι),
    (∀ (x : ι) (hl : x :: tail ≠ []),
        prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: tail)) =
          f (map f₁ (x :: tail)).prod (map f₂ (x :: tail)).prod) →
      ∀ (x : ι) (hl : x :: head :: tail ≠ []),
        prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: head :: tail)) =
          f (map f₁ (x :: head :: tail)).prod (map f₂ (x :: head :: tail)).prod
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: xs)) = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod

Tactic:
induction xs generalizing x
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl_1 : l ≠ []
x : ι
hl : [x] ≠ []
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) [x]) = f (map f₁ [x]).prod (map f₂ [x]).prod

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl_1 : l ≠ []
head : ι
tail : List ι
tail_ih :
  ∀ (x : ι) (hl : x :: tail ≠ []),
    prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: tail)) = f (map f₁ (x :: tail)).prod (map f₂ (x :: tail)).prod
x : ι
hl : x :: head :: tail ≠ []
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) (x :: head :: tail)) =
    f (map f₁ (x :: head :: tail)).prod (map f₂ (x :: head :: tail)).prod

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl : l ≠ []
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) l) = f (map f₁ l).prod (map f₂ l).prod

Tactic:
match l, hl with | x :: xs, hl => induction xs generalizing x <;> simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
simp :
  foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l =
    f (foldr (fun (x : ι) (y : M) ↦ f₁ x * y) 1 l) (foldr (fun (x : ι) (y : N) ↦ f₂ x * y) 1 l)
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) l) = f (map f₁ l).prod (map f₂ l).prod

Tactic:
simp only [prod_eq_foldr, foldr_map]

Premises used: List.prod_eq_foldr, List.foldr_map
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ ∀ (a : M) (b : N) (i : ι), f (f₁ i * a) (f₂ i * b) = (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) i (f a b)

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
rw : foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l = foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) (f 1 1) l
rw₁ rw₂ :
  Eq.{u_6 + 1} (α := P) (foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l)
    (foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l)
⊢ foldr (fun (x : ι) (y : P) ↦ f (f₁ x) (f₂ x) * y) 1 l =
    f (foldr (fun (x : ι) (y : M) ↦ f₁ x * y) 1 l) (foldr (fun (x : ι) (y : N) ↦ f₂ x * y) 1 l)

Tactic:
rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y)) _ _ (by simp [hf]), hf']

Premises used: HMul.hMul, List.foldr_hom₂
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_8
inst : CommMonoid M
l : List ι
f g : ι → M
⊢ prod (map (fun (i : ι) ↦ f i * g i) l) = (map f l).prod * (map g l).prod

Tactic:
l.prod_hom₂ (· * ·) mul_mul_mul_comm (mul_one _) _ _

Premises used: HMul.hMul, List.prod_hom₂, mul_one
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst_2 : FunLike G M N
inst_3 : MonoidHomClass G M N
g : G
rw : Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L)) (prod (map (⇑g : (a : M) → N) (map f L)))
rw₁ rw₂ : Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L)) (prod (map ((⇑g : (a : M) → N) ∘ f) L))
⊢ Eq.{u_5 + 1} (α := N) (prod (map ((⇑g : (a : M) → N) ∘ f) L) : N) ((g : (a : M) → N) (map f L).prod : N)

Tactic:
rw [← prod_hom, map_map]

Premises used: List.map_map, List.prod_hom
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
L : List M
i : ℕ
⊢ (take i L).prod * (drop i L).prod = L.prod

Tactic:
simp [← prod_append]

Premises used: List.prod_append
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
L : List M
i : ℕ
p : i < L.length
rw :
  (take i L).prod * [getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p].prod =
    (take i L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p
⊢ (take (i + 1) L).prod = (take i L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p

Tactic:
rw [← take_concat_get' _ _ p, prod_append]

Premises used: List.prod_append, List.take_concat_get'
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take i L).prod * [getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p].prod =
    (take i L).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i p

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
L : List M
h : L.prod ≠ 1
nil : ∀ (h : Ne.{u_4 + 1} (α := M) (prod []) 1), 0 < length.{u_4} (α := M) []
cons : ∀ (head : M) (tail : List M) (h : (head :: tail).prod ≠ 1), 0 < (head :: tail).length
⊢ 0 < L.length

Tactic:
cases L
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
h : Ne.{u_4 + 1} (α := M) (prod []) 1
⊢ 0 < length.{u_4} (α := M) []

Tactic:
simp at h
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
head : M
tail : List M
h : (head :: tail).prod ≠ 1
⊢ 0 < (head :: tail).length

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Preorder M
L : List M
h : 1 < L.prod
⊢ 0 < L.length

Tactic:
length_pos_of_prod_ne_one L h.ne'

Premises used: LT.lt.ne', List.length_pos_of_prod_ne_one
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Preorder M
L : List M
h : L.prod < 1
⊢ 0 < L.length

Tactic:
length_pos_of_prod_ne_one L h.ne

Premises used: List.length_pos_of_prod_ne_one, LT.lt.ne
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
x : M
xs : List M
a : M
⊢ ((x :: xs).set 0 a).prod =
    ((take 0 (x :: xs)).prod * if 0 < (x :: xs).length then a else 1) * (drop (HAdd.hAdd (α := ℕ) 0 1) (x :: xs)).prod

Tactic:
simp [set]

Premises used: List.set
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
x : M
xs : List M
i : ℕ
a : M
⊢ ((x :: xs).set (i + 1) a).prod =
    ((take (i + 1) (x :: xs)).prod * if i + 1 < (x :: xs).length then a else 1) * (drop (i + 1 + 1) (x :: xs)).prod

Tactic:
simp [set, prod_set xs i a, mul_assoc]

Premises used: mul_assoc, List.set
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
x : ℕ
x_1 : M
⊢ (set [] x x_1).prod = (prod (take x []) * if x < length.{u_4} (α := M) [] then x_1 else 1) * prod (drop (x + 1) [])

Tactic:
simp [set]

Premises used: List.set
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
nil : (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) [] 0).getD 1 * prod (tail []) = prod []
cons :
  ∀ (head : M) (tail : List M),
    (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (head :: tail) 0).getD 1 * (head :: tail).tail.prod =
      (head :: tail).prod
⊢ (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) l 0).getD 1 * l.tail.prod = l.prod

Tactic:
cases l
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
⊢ (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) [] 0).getD 1 * prod (tail []) = prod []

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
head : M
tail : List M
⊢ (getElem? (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (head :: tail) 0).getD 1 * (head :: tail).tail.prod =
    (head :: tail).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
l : List M
h : l ≠ []
nil : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
cons :
  ∀ (head : M) (tail : List M) (h : head :: tail ≠ []),
    (head :: tail).headI * (head :: tail).tail.prod = (head :: tail).prod
⊢ l.headI * l.tail.prod = l.prod

Tactic:
cases l
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
h : Ne.{u_4 + 1} (α := List M) [] []
⊢ HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []

Tactic:
contradiction
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
head : M
tail : List M
h : head :: tail ≠ []
⊢ (head :: tail).headI * (head :: tail).tail.prod = (head :: tail).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
inst_1 : Inhabited M
l : List M
h : l ≠ []
nil : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
cons :
  ∀ (head : M) (tail : List M) (h : head :: tail ≠ []),
    (head :: tail).headI * (head :: tail).tail.prod = (head :: tail).prod
nil₁ : ∀ (h : Ne.{u_4 + 1} (α := List M) [] []), HMul.hMul (α := M) (headI []) (prod (tail [])) = prod []
cons₁ :
  ∀ (head : M) (tail : List M) (h : head :: tail ≠ []),
    (head :: tail).headI * (head :: tail).tail.prod = (head :: tail).prod
⊢ l.headI * l.tail.prod = l.prod

Tactic:
cases l <;> [contradiction; simp]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
y : M
h : ∀ (x : M), Membership.mem (γ := List M) [] x → Commute y x
⊢ Commute y (prod [])

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
y z : M
l : List M
IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod
h : ∀ (x : M), x ∈ z :: l → Commute y x
⊢ Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x

Tactic:
rw [List.forall_mem_cons] at h

Premises used: List.forall_mem_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
y z : M
l : List M
IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
cons : Commute y (z * l.prod)
⊢ Commute y (z :: l).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
y z : M
l : List M
IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)

Tactic:
Commute.mul_right h.1 (IH h.2)

Premises used: Commute.mul_right, And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
y z : M
l : List M
IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)

Tactic:
exact Commute.mul_right h.1 (IH h.2)

Premises used: Commute.mul_right, And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
nil : ∀ (h : ∀ (x : M), Membership.mem (γ := List M) [] x → Commute y x), Commute y (prod [])
cons :
  ∀ (z : M) (l : List M) (IH : ∀ (h : ∀ (x : M), x ∈ l → Commute y x), Commute y l.prod)
    (h : ∀ (x : M), x ∈ z :: l → Commute y x), Commute y (z :: l).prod
⊢ Commute y l.prod

Tactic:
induction l with
  | nil => simp
  | cons z l IH =>
    rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)

Premises used: List.cons, List.forall_mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute x y
⊢ Commute l.prod y

Tactic:
((Commute.list_prod_right _ _) fun _ hx => (h _ hx).symm).symm

Premises used: Commute.list_prod_right, Commute.symm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (range n ++ [n])).prod = (map f (range n)).prod * f n
rw₁ : (map f (range n) ++ map f [n]).prod = (map f (range n)).prod * f n
rw₂ : (map f (range n) ++ [f n]).prod = (map f (range n)).prod * f n
rw₃ : (map f (range n)).prod * [f n].prod = (map f (range n)).prod * f n
rw₄ : (map f (range n)).prod * (f n * prod []) = (map f (range n)).prod * f n
rw₅ : (map f (range n)).prod * (f n * 1) = (map f (range n)).prod * f n
rw₆ rw₇ : (map f (range n)).prod * f n = (map f (range n)).prod * f n
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n

Tactic:
rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]

Premises used: List.prod_append, List.map_singleton, List.prod_nil, List.map_append, mul_one, List.prod_cons, List.range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
rw : (map f (0 :: map Nat.succ (range n))).prod = f 0 * prod (map (fun (i : ℕ) ↦ f i.succ) (range n))
⊢ (map f (range n.succ)).prod = f 0 * prod (map (fun (i : ℕ) ↦ f i.succ) (range n))

Tactic:
rw [range_succ_eq_map]

Premises used: List.range_succ_eq_map
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (0 :: map Nat.succ (range n))).prod = f 0 * prod (map (fun (i : ℕ) ↦ f i.succ) (range n))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
hl : ∀ (x : M), Membership.mem (γ := List M) [] x → x = 1
⊢ Eq.{u_4 + 1} (α := M) (prod []) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
i : M
l : List M
hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
cons : i * l.prod = 1
cons₁ : i * 1 = 1
cons₂ : HMul.hMul (α := M) 1 1 = 1
cons₃ cons₄ : Eq.{u_4 + 1} (α := M) 1 1
⊢ (i :: l).prod = 1

Tactic:
rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]

Premises used: List.mem_cons_of_mem, List.mem_cons_self, List.prod_cons, one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
nil : ∀ (hl : ∀ (x : M), Membership.mem (γ := List M) [] x → x = 1), Eq.{u_4 + 1} (α := M) (prod []) 1
cons :
  ∀ (i : M) (l : List M) (hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1) (hl : ∀ (x : M), x ∈ i :: l → x = 1),
    (i :: l).prod = 1
⊢ l.prod = 1

Tactic:
induction l with
  | nil => rfl
  | cons i l hil =>
    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]

Premises used: List.cons, List.prod_cons, one_mul, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
h : l.prod ≠ 1
⊢ ∃ (x : M), x ∈ l ∧ x ≠ 1

Tactic:
simpa only [not_forall, exists_prop] using mt prod_eq_one h

Premises used: List.prod_eq_one, mt, exists_prop, Classical.not_forall
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
a : M
inst_1 : DecidableEq M
ha : Membership.mem (γ := List M) [] a
comm : ∀ (x : M), Membership.mem (γ := List M) [] x → ∀ (y : M), Membership.mem (γ := List M) [] y → x * y = y * x
⊢ a * (List.erase [] a).prod = prod []

Tactic:
simp only [not_mem_nil] at ha

Premises used: List.not_mem_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
cons :
  ∀ (ha : a ∈ a :: l) (comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x),
    a * ((a :: l).erase a).prod = (a :: l).prod
cons₁ : ∀ (ne : a ≠ b) (h : a ∈ l), a * ((b :: l).erase a).prod = (b :: l).prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

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

Premises used: List.eq_or_ne_mem_of_mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

Tactic:
simp only [erase_cons_head, prod_cons]

Premises used: List.erase_cons_head, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
cons₃ : a * (b * (l.erase a).prod) = b * l.prod
cons₄ : a * b * (l.erase a).prod = b * l.prod
cons₅ : b * a * (l.erase a).prod = b * l.prod
cons₆ : b * (a * (l.erase a).prod) = b * l.prod
cons₇ cons₈ : b * l.prod = b * l.prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

Premises used: mul_assoc, beq_false_of_ne, List.mem_cons_of_mem, Ne.symm, List.erase, List.mem_cons_self, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
inst : Monoid M
l : List M
a : M
inst_1 : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
nil :
  ∀ (ha : Membership.mem (γ := List M) [] a)
    (comm :
      ∀ (x : M), Membership.mem (γ := List M) [] x → ∀ (y : M), Membership.mem (γ := List M) [] y → x * y = y * x),
    a * (List.erase [] a).prod = prod []
cons :
  ∀ (b : M) (l : List M)
    (ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod)
    (ha : a ∈ b :: l) (comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x),
    a * ((b :: l).erase a).prod = (b :: l).prod
⊢ a * (l.erase a).prod = l.prod

Tactic:
induction l with
  | nil => simp only [not_mem_nil] at ha
  | cons b l ih =>
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

Premises used: mul_assoc, List.eq_or_ne_mem_of_mem, List.cons, List.erase, List.erase_cons_head, List.prod_cons, List.not_mem_nil, rfl, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1
nil : prod [] = f a ^ count a []
nil₁ : 1 = f a ^ count a []
nil₂ : 1 = HPow.hPow (β := ℕ) (f a) 0
nil₃ nil₄ : Eq.{u_4 + 1} (α := M) 1 1
⊢ (map f []).prod = f a ^ count a []

Tactic:
rw [map_nil, prod_nil, count_nil, _root_.pow_zero]

Premises used: pow_zero, List.count_nil, List.prod_nil, List.map_nil
-- 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 α
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 as).prod = f a ^ count a as

Tactic:
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')

Premises used: List.mem_cons_of_mem
-- 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
cons : f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
rw [List.map_cons, List.prod_cons, count_cons, h]

Premises used: List.map_cons, List.count_cons, List.prod_cons
-- 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
cons : f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)

Tactic:
simp only [beq_iff_eq]

Premises used: beq_iff_eq
-- 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
pos : ∀ (ha' : a' = a), f a' * f a ^ count a as = f a ^ (count a as + 1)
neg : ∀ (ha' : ¬a' = a), f a' * f a ^ count a as = f a ^ (count a as + 0)
⊢ f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)

Tactic:
split_ifs with ha'
-- 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
pos : f a * f a ^ count a as = f a ^ (count a as + 1)
pos₁ pos₂ : f a * f a ^ count a as = f a * f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)

Tactic:
rw [ha', _root_.pow_succ']

Premises used: pow_succ'