awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : CommGroup G
l₂ : List G
⊢ ([] ++ l₂).alternatingProd =
    alternatingProd [] * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (length.{u_7} (α := G) [])

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₃ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
simp_rw₄ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * HPow.hPow (α := ℤ) (-1) l₁.length)
simp_rw₅ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * HPow.hPow (α := ℤ) (-1) l₁.length))
simp_rw₆ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-HPow.hPow (α := ℤ) (-1) l₁.length)
simp_rw₇ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * (l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length)⁻¹
simp_rw₈ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd / l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length

Tactic:
simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]

Premises used: List.length_cons, div_eq_mul_inv, zpow_neg, Int.neg_mul, div_div, List.cons_append, pow_succ', List.alternatingProd_cons, one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : CommGroup G
⊢ alternatingProd (reverse []) =
    HPow.hPow (α := G) (alternatingProd []) (HPow.hPow (α := ℤ) (-1) (length.{u_7} (α := G) [] + 1))

Tactic:
simp only [alternatingProd_nil, one_zpow, reverse_nil]

Premises used: List.alternatingProd_nil, one_zpow, List.reverse_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
simp_rw :
  (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ * a ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
⊢ (a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ HPow.hPow (α := ℤ) (-1) ((a :: l).length + 1)

Tactic:
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]

Premises used: List.length_reverse, List.alternatingProd_append, List.reverse_cons, inv_inv, zpow_neg, Int.neg_mul, List.length, pow_succ', List.alternatingProd_cons, one_mul, List.alternatingProd_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
rw :
  a ^ HPow.hPow (α := ℤ) (-1) l.length * (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
rw₁ :
  a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
rw₂ rw₃ :
  a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length =
    a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length
⊢ (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ * a ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length

Tactic:
rw [mul_comm, ← div_eq_mul_inv, div_zpow]

Premises used: div_zpow, div_eq_mul_inv, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
⊢ Eq.{u_4 + 1} (α := Mᵐᵒᵖ) (op (prod [])) (prod (reverse (map op [])))

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
cons : op (x * xs.prod) = (map op (x :: xs)).reverse.prod
cons₁ : op (x * xs.prod) = (op x :: map op xs).reverse.prod
cons₂ : op (x * xs.prod) = ((map op xs).reverse.concat (op x)).prod
cons₃ : op (x * xs.prod) = (map op xs).reverse.prod * op x
cons₄ : op xs.prod * op x = (map op xs).reverse.prod * op x
cons₅ cons₆ : (map op xs).reverse.prod * op x = (map op xs).reverse.prod * op x
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod

Tactic:
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

Premises used: List.map_cons, List.prod_concat, MulOpposite.op_mul, List.reverse_cons', List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l : List M
nil : Eq.{u_4 + 1} (α := Mᵐᵒᵖ) (op (prod [])) (prod (reverse (map op [])))
cons :
  ∀ (x : M) (xs : List M) (ih : op xs.prod = (map op xs).reverse.prod),
    op (x :: xs).prod = (map op (x :: xs)).reverse.prod
⊢ op l.prod = (map op l).reverse.prod

Tactic:
induction l with
  | nil => rfl
  | cons x xs ih =>
    rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

Premises used: List.map_cons, List.cons, List.prod_concat, MulOpposite.op_mul, List.reverse_cons', List.prod_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l : List Mᵐᵒᵖ
rw : op (unop l.prod) = op (map unop l).reverse.prod
rw₁ : l.prod = op (map unop l).reverse.prod
rw₂ : l.prod = (map op (map unop l).reverse).reverse.prod
rw₃ : l.prod = (map op (map unop l)).reverse.reverse.prod
rw₄ : l.prod = (map (op ∘ unop) l).reverse.reverse.prod
rw₅ : l.prod = (map (op ∘ unop) l).prod
rw₆ : l.prod = (map id l).prod
rw₇ rw₈ : l.prod = l.prod
⊢ unop l.prod = (map unop l).reverse.prod

Tactic:
rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]

Premises used: MulOpposite.op_unop, List.map_id, List.map_map, MulOpposite.op_list_prod, List.reverse_reverse, MulOpposite.op_inj, List.map_reverse, MulOpposite.op_comp_unop
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : Monoid N
F : Type u_8
inst_2 : FunLike.{u_8 + 1, u_4 + 1, u_5 + 1} F M Nᵐᵒᵖ
inst_3 : MonoidHomClass.{u_8, u_4, u_5} F M Nᵐᵒᵖ
f : F
l : List M
rw :
  Eq.{u_5 + 1} (α := N) (MulOpposite.unop (prod (map (⇑f : (a : M) → Nᵐᵒᵖ) l)))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
rw₁ :
  Eq.{u_5 + 1} (α := N) (prod (reverse (map MulOpposite.unop (map (⇑f : (a : M) → Nᵐᵒᵖ) l))))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := N) (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
⊢ Eq.{u_5 + 1} (α := N) (MulOpposite.unop ((f : (a : M) → Nᵐᵒᵖ) l.prod))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))

Tactic:
rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]

Premises used: List.map_map, map_list_prod, MulOpposite.unop_list_prod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
a : M
inst_1 : DecidableEq M
h : a ∈ s
rw : a * ((↑s.toList : Multiset M).erase a).prod = (↑s.toList : Multiset M).prod
rw₁ : a * (↑(s.toList.erase a) : Multiset M).prod = (↑s.toList : Multiset M).prod
rw₂ : a * (s.toList.erase a).prod = (↑s.toList : Multiset M).prod
rw₃ : a * (s.toList.erase a).prod = s.toList.prod
rw₄ rw₅ : s.toList.prod = s.toList.prod
⊢ a * (s.erase a).prod = s.prod

Tactic:
rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]

Premises used: Iff.mpr, Multiset.coe_toList, List.prod_erase, Multiset.mem_toList, Multiset.coe_erase, Multiset.prod_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → M
inst_1 : DecidableEq ι
a : ι
h : a ∈ m
rw : f a * (map f ((↑m.toList : Multiset ι).erase a)).prod = (map f (↑m.toList : Multiset ι)).prod
rw₁ : f a * (map f (↑(m.toList.erase a) : Multiset ι)).prod = (map f (↑m.toList : Multiset ι)).prod
rw₂ : f a * (↑(List.map f (m.toList.erase a)) : Multiset M).prod = (map f (↑m.toList : Multiset ι)).prod
rw₃ : f a * (↑(List.map f (m.toList.erase a)) : Multiset M).prod = (↑(List.map f m.toList) : Multiset M).prod
rw₄ : f a * (List.map f (m.toList.erase a)).prod = (↑(List.map f m.toList) : Multiset M).prod
rw₅ : f a * (List.map f (m.toList.erase a)).prod = (List.map f m.toList).prod
rw₆ rw₇ : (List.map f m.toList).prod = (List.map f m.toList).prod
⊢ f a * (map f (m.erase a)).prod = (map f m).prod

Tactic:
rw [← m.coe_toList, coe_erase, map_coe, map_coe, prod_coe, prod_coe,
    List.prod_map_erase f (mem_toList.2 h)]

Premises used: Iff.mpr, Multiset.coe_toList, Multiset.mem_toList, Multiset.coe_erase, Multiset.map_coe, Multiset.prod_coe, List.prod_map_erase
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s t : Multiset M
l₁ l₂ : List M
⊢ (⟦l₁⟧ + ⟦l₂⟧).prod = prod ⟦l₁⟧ * prod ⟦l₂⟧

Tactic:
simp [List.prod_append]

Premises used: List.prod_append
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
m : Multiset M
rw : Eq.{u_5 + 1} (α := M) (prod 0) 1
⊢ (HSMul.hSMul (α := ℕ) 0 m).prod = HPow.hPow (β := ℕ) m.prod 0

Tactic:
rw [zero_nsmul, pow_zero]

Premises used: pow_zero, zero_nsmul
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
m : Multiset M
⊢ Eq.{u_5 + 1} (α := M) (prod 0) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
m : Multiset M
n : ℕ
rw : (n • m + HSMul.hSMul (α := ℕ) 1 m).prod = m.prod ^ (n + 1)
rw₁ : (n • m + m).prod = m.prod ^ (n + 1)
rw₂ : (n • m + m).prod = m.prod ^ n * HPow.hPow (β := ℕ) m.prod 1
rw₃ : (n • m + m).prod = m.prod ^ n * m.prod
rw₄ : (n • m).prod * m.prod = m.prod ^ n * m.prod
rw₅ rw₆ : m.prod ^ n * m.prod = m.prod ^ n * m.prod
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)

Tactic:
rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]

Premises used: pow_add, pow_one, Multiset.prod_add, one_nsmul, add_nsmul
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
p : M → Prop
inst_1 : DecidablePred p
rw : (filter p s + filter (fun (a : M) ↦ ¬p a) s).prod = s.prod
rw₁ rw₂ : s.prod = s.prod
⊢ (filter p s).prod * (filter (fun (a : M) ↦ ¬p a) s).prod = s.prod

Tactic:
rw [← prod_add, filter_add_not]

Premises used: Multiset.filter_add_not, Multiset.prod_add
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → M
inst_1 : DecidableEq ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
h : ∀ (a : List ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a⟧ → f i' = 1), (map f ⟦a⟧).prod = f i ^ count i ⟦a⟧
⊢ (map f m).prod = f i ^ count i m

Tactic:
induction m using Quotient.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → M
inst_1 : DecidableEq ι
i : ι
a : List ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a⟧ → f i' = 1
⊢ (map f ⟦a⟧).prod = f i ^ count i ⟦a⟧

Tactic:
simp [List.prod_map_eq_pow_single i f hf]

Premises used: List.prod_map_eq_pow_single
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
inst_1 : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ s → a' = 1
h₁ : ∀ (a_1 : List M) (h : ∀ (a' : M), a' ≠ a → a' ∈ ⟦a_1⟧ → a' = 1), prod ⟦a_1⟧ = a ^ count a ⟦a_1⟧
⊢ s.prod = a ^ count a s

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
inst_1 : DecidableEq M
a : M
a_1 : List M
h : ∀ (a' : M), a' ≠ a → a' ∈ ⟦a_1⟧ → a' = 1
⊢ prod ⟦a_1⟧ = a ^ count a ⟦a_1⟧

Tactic:
simp [List.prod_eq_pow_single a h]

Premises used: List.prod_eq_pow_single
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
h : ∀ (x : M), x ∈ s → x = 1
h₁ : ∀ (a : List M) (h : ∀ (x : M), x ∈ ⟦a⟧ → x = 1), prod ⟦a⟧ = 1
⊢ s.prod = 1

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
a : List M
h : ∀ (x : M), x ∈ ⟦a⟧ → x = 1
⊢ prod ⟦a⟧ = 1

Tactic:
simp [List.prod_eq_one h]

Premises used: List.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset M
hs : s ≠ 0
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
h :
  ∀ (a : List M) (hs : Ne (α := Multiset M) (Quot.mk (⇑(List.isSetoid M) : List M → List M → Prop) a) 0),
    Eq.{u_6 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (Quot.mk (⇑(List.isSetoid M) : List M → List M → Prop) a)) : N)
      ((f : (a : M) → N) (prod (Quot.mk (⇑(List.isSetoid M) : List M → List M → Prop) a)) : N)
⊢ Eq.{u_6 + 1} (α := N) (prod (map (⇑f : (a : M) → N) s) : N) ((f : (a : M) → N) s.prod : N)

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
a : List M
hs : Ne (α := Multiset M) (Quot.mk (⇑(List.isSetoid M) : List M → List M → Prop) a) 0
⊢ Eq.{u_6 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (Quot.mk (⇑(List.isSetoid M) : List M → List M → Prop) a)) : N)
    ((f : (a : M) → N) (prod (Quot.mk (⇑(List.isSetoid M) : List M → List M → Prop) a)) : N)

Tactic:
aesop (add simp List.prod_hom_nonempty)

Premises used: List.prod_hom_nonempty
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset M
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
l : List M
⊢ Eq.{u_6 + 1} (α := N) (prod (map (⇑f : (a : M) → N) ⟦l⟧) : N) ((f : (a : M) → N) (prod ⟦l⟧) : N)

Tactic:
simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

Premises used: Multiset.quot_mk_to_coe, List.prod_hom, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset ι
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
g : ι → M
⊢ Eq.{u_6 + 1} (α := N) (prod (map (⇑f : (a : M) → N) (map g s)) : N) ((f : (a : M) → N) (map g s).prod : N)

Tactic:
(s.map g).prod_hom f

Premises used: Multiset.map, Multiset.prod_hom
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset ι
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
g : ι → M
h : Eq.{u_6 + 1} (α := Multiset N) (map (fun (i : ι) ↦ (f : (a : M) → N) (g i)) s) (map (⇑f : (a : M) → N) (map g s))
⊢ Eq.{u_6 + 1} (α := N) (prod (map (fun (i : ι) ↦ (f : (a : M) → N) (g i)) s) : N)
    ((f : (a : M) → N) (map g s).prod : N)

Tactic:
convert! (s.map g).prod_hom f

Premises used: Multiset.map, Multiset.prod_hom
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset ι
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
g : ι → M
⊢ Eq.{u_6 + 1} (α := Multiset N) (map (fun (i : ι) ↦ (f : (a : M) → N) (g i)) s) (map (⇑f : (a : M) → N) (map g s))

Tactic:
(map_map _ _ _).symm

Premises used: Multiset.map_map, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset ι
F : Type u_8
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
g : ι → M
⊢ Eq.{u_6 + 1} (α := Multiset N) (map (fun (i : ι) ↦ (f : (a : M) → N) (g i)) s) (map (⇑f : (a : M) → N) (map g s))

Tactic:
exact (map_map _ _ _).symm

Premises used: Multiset.map_map, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : CommMonoid O
s : Multiset ι
hs : s ≠ 0
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
h :
  ∀ (a : List ι) (hs : ⟦a⟧ ≠ 0), prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) ⟦a⟧) = f (map f₁ ⟦a⟧).prod (map f₂ ⟦a⟧).prod
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) s) = f (map f₁ s).prod (map f₂ s).prod

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : CommMonoid O
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
a : List ι
hs : ⟦a⟧ ≠ 0
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) ⟦a⟧) = f (map f₁ ⟦a⟧).prod (map f₂ ⟦a⟧).prod

Tactic:
aesop (add simp List.prod_hom₂_nonempty)

Premises used: List.prod_hom₂_nonempty
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : CommMonoid O
s : Multiset ι
f : M → N → O
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
l : List ι
⊢ prod (map (fun (i : ι) ↦ f (f₁ i) (f₂ i)) ⟦l⟧) = f (map f₁ ⟦l⟧).prod (map f₂ ⟦l⟧).prod

Tactic:
simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]

Premises used: Multiset.quot_mk_to_coe, List.prod_hom₂, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : CommMonoid M
m : Multiset ι
f g : ι → M
⊢ prod (map (fun (i : ι) ↦ f i * g i) m) = (map f m).prod * (map g m).prod

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

Premises used: HMul.hMul, mul_one, Multiset.prod_hom₂
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → M
n : ℕ
⊢ prod (map (fun (i : ι) ↦ f i ^ n) m) = (map f m).prod ^ n

Tactic:
m.prod_hom' (powMonoidHom n : M →* M) f

Premises used: powMonoidHom, Multiset.prod_hom'
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
κ : Type u_3
M : Type u_5
inst : CommMonoid M
m : Multiset ι
n : Multiset κ
f : ι → κ → M
⊢ Eq.{u_5 + 1} (α := M) (prod (map (fun (a : ι) ↦ prod (map (fun (b : κ) ↦ f a b) n)) 0))
    (prod (map (fun (b : κ) ↦ prod (map (fun (a : ι) ↦ f a b) 0)) n))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
κ : Type u_3
M : Type u_5
inst : CommMonoid M
m_1 : Multiset ι
n : Multiset κ
f : ι → κ → M
a : ι
m : Multiset ι
ih :
  Eq.{u_5 + 1} (α := M) (prod (map (fun (a : ι) ↦ prod (map (fun (b : κ) ↦ f a b) n)) m))
    (prod (map (fun (b : κ) ↦ prod (map (fun (a : ι) ↦ f a b) m)) n))
⊢ Eq.{u_5 + 1} (α := M) (prod (map (fun (a : ι) ↦ prod (map (fun (b : κ) ↦ f a b) n)) (a ::ₘ m)))
    (prod (map (fun (b : κ) ↦ prod (map (fun (a : ι) ↦ f a b) (a ::ₘ m))) n))

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s t : Multiset M
h : s ≤ t
obtain : ∀ (z : Multiset M) (h : s ≤ s + z), s.prod ∣ (s + z).prod
⊢ s.prod ∣ t.prod

Tactic:
obtain ⟨z, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s z : Multiset M
h : s ≤ s + z
⊢ s.prod ∣ (s + z).prod

Tactic:
simp only [prod_add, dvd_mul_right]

Premises used: Multiset.prod_add, dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
F : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
f : F
s : Multiset M
⊢ Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) s.prod : N) (prod (map (⇑f : (a : M) → N) s) : N)

Tactic:
(s.prod_hom f).symm

Premises used: Multiset.prod_hom, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
F : Type u_1
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
s : Multiset M
hs : s ≠ 0
⊢ Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) s.prod : N) (prod (map (⇑f : (a : M) → N) s) : N)

Tactic:
(s.prod_hom_ne_zero hs f).symm

Premises used: Eq.symm, Multiset.prod_hom_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →* N
s : Multiset M
⊢ Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) s.prod : N) (prod (map (⇑f : (a : M) → N) s) : N)

Tactic:
(s.prod_hom f).symm

Premises used: Multiset.prod_hom, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
f : M →ₙ* N
s : Multiset M
hs : s ≠ 0
⊢ Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) s.prod : N) (prod (map (⇑f : (a : M) → N) s) : N)

Tactic:
(s.prod_hom_ne_zero hs f).symm

Premises used: Eq.symm, Multiset.prod_hom_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
a_1 : M
l : List M
a : M
h : a ∈ ⟦l⟧
⊢ a ∣ prod ⟦l⟧

Tactic:
simpa using List.dvd_prod h

Premises used: List.dvd_prod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset (M × N)
⊢ s.prod.1 = (map Prod.fst s).prod

Tactic:
map_multiset_prod (MonoidHom.fst _ _) _

Premises used: map_multiset_prod, MonoidHom.fst
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset (M × N)
⊢ s.prod.2 = (map Prod.snd s).prod

Tactic:
map_multiset_prod (MonoidHom.snd _ _) _

Premises used: map_multiset_prod, MonoidHom.snd
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
h₁ : (map g1 0).prod ∣ (map g2 0).prod
h₂ :
  ∀ {a : M} {s : Multiset M},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
⊢ (map g1 S).prod ∣ (map g2 S).prod

Tactic:
apply Multiset.induction_on' S

Premises used: Multiset.induction_on'
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ (map g1 0).prod ∣ (map g2 0).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
N : Type u_6
inst : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
T : Multiset M
haS : a ∈ S
h₂ : T ⊆ S → (map g1 T).prod ∣ (map g2 T).prod → (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod
⊢ T ⊆ S → (map g1 T).prod ∣ (map g2 T).prod → (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod

Tactic:
_