awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
l : List ℕ
n : ℕ
nil : sum [] % n = sum (map (fun (x : ℕ) ↦ x % n) []) % n
cons :
  ∀ (a : ℕ) (l : List ℕ) (ih : l.sum % n = sum (map (fun (x : ℕ) ↦ x % n) l) % n),
    (a :: l).sum % n = sum (map (fun (x : ℕ) ↦ x % n) (a :: l)) % n
⊢ l.sum % n = sum (map (fun (x : ℕ) ↦ x % n) l) % n

Tactic:
induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

Premises used: List.map_cons, Nat.add_mod_mod, List.cons, Nat.mod_add_mod, List.sum_cons, List.map_nil, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n : ℕ
⊢ prod [] % n = prod (map (fun (x : ℕ) ↦ x % n) []) % n

Tactic:
simp only [map_nil]

Premises used: List.map_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n a : ℕ
l : List ℕ
ih : l.prod % n = prod (map (fun (x : ℕ) ↦ x % n) l) % n
⊢ (a :: l).prod % n = prod (map (fun (x : ℕ) ↦ x % n) (a :: l)) % n

Tactic:
simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

Premises used: Nat.mod_mul_mod, List.map_cons, Nat.mul_mod_mod, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
l : List ℕ
n : ℕ
nil : prod [] % n = prod (map (fun (x : ℕ) ↦ x % n) []) % n
cons :
  ∀ (a : ℕ) (l : List ℕ) (ih : l.prod % n = prod (map (fun (x : ℕ) ↦ x % n) l) % n),
    (a :: l).prod % n = prod (map (fun (x : ℕ) ↦ x % n) (a :: l)) % n
⊢ l.prod % n = prod (map (fun (x : ℕ) ↦ x % n) l) % n

Tactic:
induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

Premises used: Nat.mod_mul_mod, List.map_cons, Nat.mul_mod_mod, List.cons, List.prod_cons, List.map_nil, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
l : List ℤ
n : ℤ
nil : sum [] % n = sum (map (fun (x : ℤ) ↦ x % n) []) % n
cons :
  ∀ (head : ℤ) (tail : List ℤ),
    tail.sum % n = sum (map (fun (x : ℤ) ↦ x % n) tail) % n →
      (head :: tail).sum % n = sum (map (fun (x : ℤ) ↦ x % n) (head :: tail)) % n
⊢ l.sum % n = sum (map (fun (x : ℤ) ↦ x % n) l) % n

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n : ℤ
⊢ sum [] % n = sum (map (fun (x : ℤ) ↦ x % n) []) % n

Tactic:
simp [Int.add_emod, *]

Premises used: Int.add_emod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n head : ℤ
tail : List ℤ
tail_ih : tail.sum % n = sum (map (fun (x : ℤ) ↦ x % n) tail) % n
⊢ (head :: tail).sum % n = sum (map (fun (x : ℤ) ↦ x % n) (head :: tail)) % n

Tactic:
simp [Int.add_emod, *]

Premises used: Int.add_emod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
l : List ℤ
n : ℤ
nil : prod [] % n = prod (map (fun (x : ℤ) ↦ x % n) []) % n
cons :
  ∀ (head : ℤ) (tail : List ℤ),
    tail.prod % n = prod (map (fun (x : ℤ) ↦ x % n) tail) % n →
      (head :: tail).prod % n = prod (map (fun (x : ℤ) ↦ x % n) (head :: tail)) % n
⊢ l.prod % n = prod (map (fun (x : ℤ) ↦ x % n) l) % n

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n : ℤ
⊢ prod [] % n = prod (map (fun (x : ℤ) ↦ x % n) []) % n

Tactic:
simp [Int.mul_emod, *]

Premises used: Int.mul_emod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n head : ℤ
tail : List ℤ
tail_ih : tail.prod % n = prod (map (fun (x : ℤ) ↦ x % n) tail) % n
⊢ (head :: tail).prod % n = prod (map (fun (x : ℤ) ↦ x % n) (head :: tail)) % n

Tactic:
simp [Int.mul_emod, *]

Premises used: Int.mul_emod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
l : List M
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) l.prod : N) (List.prod (List.map (⇑f : (a : M) → N) l) : N)

Tactic:
(l.prod_hom f).symm

Premises used: List.prod_hom, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
f : M →* N
l : List M
⊢ Eq.{u_5 + 1} (α := N) ((f : (a : M) → N) l.prod : N) (List.prod (List.map (⇑f : (a : M) → N) l) : N)

Tactic:
map_list_prod f l

Premises used: map_list_prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
β : Type u_8
inst : DivisionCommMonoid β
r : ℤ
l : List β
⊢ l.prod ^ r = prod (map (fun (x : β) ↦ x ^ r) l)

Tactic:
let fr : β →* β := ⟨⟨fun b ↦ b ^ r, one_zpow r⟩, (mul_zpow · · r)⟩
  map_list_prod fr l

Premises used: OneHom.mk, one_zpow, mul_zpow, MonoidHom.mk, map_list_prod, HPow.hPow
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
L : List (List α)
i : ℕ
nil :
  ∀ (i : ℕ),
    Eq.{u_2 + 1} (α := List α) (take (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
      (flatten (take i []))
cons :
  ∀ (head : List α) (tail : List (List α)),
    (∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten) →
      ∀ (i : ℕ), take (take i (map length (head :: tail))).sum (head :: tail).flatten = (take i (head :: tail)).flatten
⊢ take (take i (map length L)).sum L.flatten = (take i L).flatten

Tactic:
induction L generalizing i
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
i : ℕ
⊢ Eq.{u_2 + 1} (α := List α) (take (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
    (flatten (take i []))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten
i : ℕ
cons : take (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (take 0 (head :: tail)).flatten
cons₁ :
  ∀ (n : ℕ),
    take (take (n + 1) (map length (head :: tail))).sum (head :: tail).flatten = (take (n + 1) (head :: tail)).flatten
⊢ take (take i (map length (head :: tail))).sum (head :: tail).flatten = (take i (head :: tail)).flatten

Tactic:
cases i
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten
⊢ take (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (take 0 (head :: tail)).flatten

Tactic:
simp [take_length_add_append, *]

Premises used: List.take_length_add_append
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten
n : ℕ
⊢ take (take (n + 1) (map length (head :: tail))).sum (head :: tail).flatten = (take (n + 1) (head :: tail)).flatten

Tactic:
simp [take_length_add_append, *]

Premises used: List.take_length_add_append
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
L : List (List α)
i : ℕ
nil :
  ∀ (i : ℕ),
    Eq.{u_2 + 1} (α := List α) (drop (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
      (flatten (drop i []))
cons :
  ∀ (head : List α) (tail : List (List α)),
    (∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten) →
      ∀ (i : ℕ), drop (take i (map length (head :: tail))).sum (head :: tail).flatten = (drop i (head :: tail)).flatten
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten

Tactic:
induction L generalizing i
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
i : ℕ
⊢ Eq.{u_2 + 1} (α := List α) (drop (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
    (flatten (drop i []))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten
i : ℕ
cons : drop (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (drop 0 (head :: tail)).flatten
cons₁ :
  ∀ (n : ℕ),
    drop (take (n + 1) (map length (head :: tail))).sum (head :: tail).flatten = (drop (n + 1) (head :: tail)).flatten
⊢ drop (take i (map length (head :: tail))).sum (head :: tail).flatten = (drop i (head :: tail)).flatten

Tactic:
cases i
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten
⊢ drop (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (drop 0 (head :: tail)).flatten

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten
n : ℕ
⊢ drop (take (n + 1) (map length (head :: tail))).sum (head :: tail).flatten = (drop (n + 1) (head :: tail)).flatten

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
h : ∀ (i : ℕ), Membership.mem (γ := List ℕ) [] i → 1 ≤ i
⊢ length (α := ℕ) [] ≤ sum []

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
j : ℕ
L : List ℕ
IH : ∀ (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i), L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
cons : 1 + L.length ≤ j + L.sum
⊢ (j :: L).length ≤ (j :: L).sum

Tactic:
rw [sum_cons, length, add_comm]

Premises used: add_comm, List.sum_cons, List.length
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
j : ℕ
L : List ℕ
IH : ∀ (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i), L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum

Tactic:
Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

Premises used: Iff.mpr, Nat.add_le_add, List.mem_cons_self, List.mem_cons, Or.inr
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
j : ℕ
L : List ℕ
IH : ∀ (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i), L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum

Tactic:
exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

Premises used: Iff.mpr, Nat.add_le_add, List.mem_cons_self, List.mem_cons, Or.inr
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
nil : ∀ (h : ∀ (i : ℕ), Membership.mem (γ := List ℕ) [] i → 1 ≤ i), length (α := ℕ) [] ≤ sum []
cons :
  ∀ (j : ℕ) (L : List ℕ) (IH : ∀ (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i), L.length ≤ L.sum) (h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i),
    (j :: L).length ≤ (j :: L).sum
⊢ L.length ≤ L.sum

Tactic:
induction L with
  | nil => simp
  | cons j L IH =>
    rw [sum_cons, length, add_comm]
    exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

Premises used: add_comm, List.cons, List.sum_cons, List.length, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x
⊢ p (prod [])

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
cons : p (a * l.prod)
⊢ p (a :: l).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p a ∧ ∀ (a : M), a ∈ l → p a

Tactic:
simp only [mem_cons, forall_eq_or_imp] at base

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)

Tactic:
hom _ _ (base.1) (ih base.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)

Tactic:
exact hom _ _ (base.1) (ih base.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ l → p x
nil : ∀ (base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x), p (prod [])
cons :
  ∀ (a : M) (l : List M) (ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod) (base : ∀ (x : M), x ∈ a :: l → p x),
    p (a :: l).prod
⊢ p l.prod

Tactic:
induction l with
  | nil => simpa
  | cons a l ih =>
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)

Premises used: forall_eq_or_imp, List.cons, List.mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
⊢ Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) [])) 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
head : ι
tail : List ι
tail_ih : Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) tail)) 1
⊢ Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) (head :: tail))) 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
l : List ι
nil : Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) [])) 1
cons :
  ∀ (head : ι) (tail : List ι),
    Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) tail)) 1 →
      Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) (head :: tail))) 1
⊢ Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) l)) 1

Tactic:
induction l with simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : Ne.{u_2 + 1} (α := List M) [] []
base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x
⊢ p (prod [])

Tactic:
simp at hl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
pos : ∀ (hl_empty : l = []), p (a :: l).prod
neg : ∀ (hl_empty : ¬l = []), p (a :: l).prod
⊢ p (a :: l).prod

Tactic:
by_cases hl_empty : l = []
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : l = []
⊢ p (a :: l).prod

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
neg : p (a * l.prod)
⊢ p (a :: l).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p a ∧ ∀ (a : M), a ∈ l → p a

Tactic:
simp only [mem_cons, forall_eq_or_imp] at base

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
hl_empty : ¬l = []
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)

Tactic:
hom _ _ (base.1) (ih hl_empty base.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
hl_empty : ¬l = []
base : p a ∧ ∀ (a : M), a ∈ l → p a
⊢ p (a * l.prod)

Tactic:
exact hom _ _ (base.1) (ih hl_empty base.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : l ≠ []
base : ∀ (x : M), x ∈ l → p x
nil : ∀ (hl : Ne.{u_2 + 1} (α := List M) [] []) (base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x), p (prod [])
cons :
  ∀ (a : M) (l : List M) (ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod) (hl : a :: l ≠ [])
    (base : ∀ (x : M), x ∈ a :: l → p x), p (a :: l).prod
⊢ p l.prod

Tactic:
induction l with
  | nil => simp at hl
  | cons a l ih =>
    by_cases hl_empty : l = []
    · simp [*]
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih hl_empty base.2)

Premises used: forall_eq_or_imp, List.cons, List.mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
zero : (replicate 0 a).prod = 1
zero₁ : Eq.{u_2 + 1} (α := M) (prod []) 1
zero₂ zero₃ : Eq.{u_2 + 1} (α := M) 1 1
⊢ (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0

Tactic:
rw [pow_zero, replicate_zero, prod_nil]

Premises used: List.replicate_zero, pow_zero, List.prod_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
succ : (a :: replicate n a).prod = a ^ (n + 1)
succ₁ : a * (replicate n a).prod = a ^ (n + 1)
succ₂ : a * a ^ n = a ^ (n + 1)
succ₃ succ₄ : a * a ^ n = a * a ^ n
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)

Tactic:
rw [replicate_succ, prod_cons, ih, pow_succ']

Premises used: List.replicate_succ, List.prod_cons, pow_succ'
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
a : M
zero : (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0
succ : ∀ (n : ℕ) (ih : (replicate n a).prod = a ^ n), (replicate (n + 1) a).prod = a ^ (n + 1)
⊢ (replicate n a).prod = a ^ n

Tactic:
induction n with
  | zero => rw [pow_zero, replicate_zero, prod_nil]
  | succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']

Premises used: List.replicate_zero, pow_zero, List.replicate_succ, List.prod_nil, List.prod_cons, pow_succ'
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
M : Type u_2
inst : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
rw : l.prod = (replicate l.length m).prod
rw₁ rw₂ : l.prod = l.prod
⊢ l.prod = m ^ l.length

Tactic:
rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]

Premises used: Iff.mpr, And.intro, List.eq_replicate_iff, List.prod_replicate, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Defs
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
inst : Monoid M
inst_1 : Monoid N
l_1 : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (map f l).prod (map g l).prod
⊢ r (map f (a :: l)).prod (map g (a :: l)).prod

Tactic:
simp only [map_cons, prod_cons, h₂ hl]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
h : ∀ (m : M), Membership.mem (γ := List M) [] m → IsUnit m
⊢ IsUnit.{u_4} (M := M) (prod [])

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
simp : IsUnit (h * t.prod)
⊢ IsUnit (h :: t).prod

Tactic:
simp only [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h * t.prod)

Tactic:
IsUnit.mul (u h mem_cons_self) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

Premises used: List.mem_cons_of_mem, IsUnit.mul, List.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h * t.prod)

Tactic:
exact IsUnit.mul (u h mem_cons_self) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

Premises used: List.mem_cons_of_mem, IsUnit.mul, List.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
L : List M
⊢ IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
⟨fun h => ?_, prod_isUnit⟩

Premises used: List.prod_isUnit, Iff.intro
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
L : List M
refine : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m
⊢ IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
refine ⟨fun h => ?_, prod_isUnit⟩
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
h : IsUnit.{u_8} (M := M) (prod [])
⊢ ∀ (m : M), Membership.mem (γ := List M) [] m → IsUnit m

Tactic:
fun m' h' => False.elim (not_mem_nil h')

Premises used: False.elim, List.not_mem_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
h : IsUnit.{u_8} (M := M) (prod [])
⊢ ∀ (m : M), Membership.mem (γ := List M) [] m → IsUnit m

Tactic:
exact fun m' h' => False.elim (not_mem_nil h')

Premises used: False.elim, List.not_mem_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
m : M
L : List M
ih : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m
h : IsUnit (m :: L).prod
⊢ IsUnit m ∧ IsUnit L.prod

Tactic:
rw [prod_cons, IsUnit.mul_iff] at h

Premises used: IsUnit.mul_iff, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
m : M
L : List M
ih : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

Premises used: List.eq_or_mem_of_mem_cons, And.right, Eq.substr, Or.elim
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
m : M
L : List M
ih : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

Premises used: List.eq_or_mem_of_mem_cons, And.right, Or.elim
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_8
inst : CommMonoid M
L : List M
h : IsUnit L.prod
nil : ∀ (h : IsUnit.{u_8} (M := M) (prod [])) (m : M), Membership.mem (γ := List M) [] m → IsUnit m
cons :
  ∀ (m : M) (L : List M) (ih : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m) (h : IsUnit (m :: L).prod) (m_1 : M),
    m_1 ∈ m :: L → IsUnit m_1
⊢ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

Premises used: IsUnit.mul_iff, False.elim, List.cons, List.prod_cons, List.not_mem_nil, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ l₁.prod = l₂.prod

Tactic:
h.foldr_eq' ?_ _

Premises used: List.Perm.foldr_eq', List.prod