awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod
have cons₁ : op (x * xs.prod) = (op x :: map op xs).reverse.prod
Tactic: rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod
have cons₂ : op (x * xs.prod) = ((map op xs).reverse.concat (op x)).prod
Tactic: rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod
have cons₃ : op (x * xs.prod) = (map op xs).reverse.prod * op x
Tactic: rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod
have cons₄ : op xs.prod * op x = (map op xs).reverse.prod * op x
Tactic: rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod
have cons₅ : (map op xs).reverse.prod * op x = (map op xs).reverse.prod * op x
Tactic: rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
⊢ op l.prod = (map op l).reverse.prod
have nil : Eq.{u_4 + 1} (α := Mᵐᵒᵖ) (op (prod [])) (prod (reverse (map op [])))
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
nil : Eq.{u_4 + 1} (α := Mᵐᵒᵖ) (op (prod [])) (prod (reverse (map op [])))
⊢ op l.prod = (map op l).reverse.prod
have 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
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List Mᵐᵒᵖ
⊢ unop l.prod = (map unop l).reverse.prod
have rw : op (unop l.prod) = op (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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List Mᵐᵒᵖ
rw : op (unop l.prod) = op (map unop l).reverse.prod
⊢ unop l.prod = (map unop l).reverse.prod
have rw₁ : l.prod = op (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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ unop l.prod = (map unop l).reverse.prod
have rw₂ : l.prod = (map op (map unop l).reverse).reverse.prod
Tactic: rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ unop l.prod = (map unop l).reverse.prod
have rw₃ : l.prod = (map op (map unop l)).reverse.reverse.prod
Tactic: rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ unop l.prod = (map unop l).reverse.prod
have rw₄ : l.prod = (map (op ∘ unop) l).reverse.reverse.prod
Tactic: rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ unop l.prod = (map unop l).reverse.prod
have rw₅ : l.prod = (map (op ∘ unop) l).prod
Tactic: rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ unop l.prod = (map unop l).reverse.prod
have rw₆ : l.prod = (map id l).prod
Tactic: rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ unop l.prod = (map unop l).reverse.prod
have rw₇ : l.prod = l.prod
Tactic: rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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
⊢ Eq.{u_5 + 1} (α := N) (MulOpposite.unop ((f : (a : M) → Nᵐᵒᵖ) l.prod))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
have 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)))
Tactic: rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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)))
⊢ Eq.{u_5 + 1} (α := N) (MulOpposite.unop ((f : (a : M) → Nᵐᵒᵖ) l.prod))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
have 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)))
Tactic: rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
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)))
⊢ Eq.{u_5 + 1} (α := N) (MulOpposite.unop ((f : (a : M) → Nᵐᵒᵖ) l.prod))
    (prod (reverse (map (MulOpposite.unop ∘ (⇑f : (a : M) → Nᵐᵒᵖ)) l)))
have 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)))
Tactic: rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
a : M
inst_1 : DecidableEq M
h : a ∈ s
⊢ a * (s.erase a).prod = s.prod
have rw : a * ((↑s.toList : Multiset M).erase a).prod = (↑s.toList : Multiset M).prod
Tactic: rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ a * (s.erase a).prod = s.prod
have rw₁ : a * (↑(s.toList.erase a) : Multiset M).prod = (↑s.toList : Multiset M).prod
Tactic: rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ a * (s.erase a).prod = s.prod
have rw₂ : a * (s.toList.erase a).prod = (↑s.toList : Multiset M).prod
Tactic: rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ a * (s.erase a).prod = s.prod
have rw₃ : a * (s.toList.erase a).prod = s.toList.prod
Tactic: rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ a * (s.erase a).prod = s.prod
have rw₄ : s.toList.prod = s.toList.prod
Tactic: rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
ι : Type u_2
M : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → M
inst_1 : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw : f a * (map f ((↑m.toList : Multiset ι).erase a)).prod = (map f (↑m.toList : Multiset ι)).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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw₁ : f a * (map f (↑(m.toList.erase a) : Multiset ι)).prod = (map f (↑m.toList : Multiset ι)).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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw₂ : f a * (↑(List.map f (m.toList.erase a)) : Multiset M).prod = (map f (↑m.toList : Multiset ι)).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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw₃ : f a * (↑(List.map f (m.toList.erase a)) : Multiset M).prod = (↑(List.map f m.toList) : Multiset 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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw₄ : f a * (List.map f (m.toList.erase a)).prod = (↑(List.map f m.toList) : Multiset 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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw₅ : f a * (List.map f (m.toList.erase a)).prod = (List.map f m.toList).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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ f a * (map f (m.erase a)).prod = (map f m).prod
have rw₆ : (List.map f m.toList).prod = (List.map f m.toList).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)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
m : Multiset M
⊢ (HSMul.hSMul (α := ℕ) 0 m).prod = HPow.hPow (β := ℕ) m.prod 0
have rw : Eq.{u_5 + 1} (α := M) (prod 0) 1
Tactic: rw [zero_nsmul, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
m : Multiset M
n : ℕ
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)
have rw : (n • m + HSMul.hSMul (α := ℕ) 1 m).prod = m.prod ^ (n + 1)
Tactic: rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
m : Multiset M
n : ℕ
rw : (n • m + HSMul.hSMul (α := ℕ) 1 m).prod = m.prod ^ (n + 1)
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)
have rw₁ : (n • m + m).prod = m.prod ^ (n + 1)
Tactic: rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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)
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)
have rw₂ : (n • m + m).prod = m.prod ^ n * HPow.hPow (β := ℕ) m.prod 1
Tactic: rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)
have rw₃ : (n • m + m).prod = m.prod ^ n * m.prod
Tactic: rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)
have rw₄ : (n • m).prod * m.prod = m.prod ^ n * m.prod
Tactic: rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ ((n + 1) • m).prod = m.prod ^ (n + 1)
have rw₅ : m.prod ^ n * m.prod = m.prod ^ n * m.prod
Tactic: rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
p : M → Prop
inst_1 : DecidablePred p
⊢ (filter p s).prod * (filter (fun (a : M) ↦ ¬p a) s).prod = s.prod
have rw : (filter p s + filter (fun (a : M) ↦ ¬p a) s).prod = s.prod
Tactic: rw [← prod_add, filter_add_not]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ (filter p s).prod * (filter (fun (a : M) ↦ ¬p a) s).prod = s.prod
have rw₁ : s.prod = s.prod
Tactic: rw [← prod_add, filter_add_not]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ (map f m).prod = f i ^ count i m
have h : ∀ (a : List ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a⟧ → f i' = 1), (map f ⟦a⟧).prod = f i ^ count i ⟦a⟧
Tactic: induction m using Quotient.inductionOn
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ s.prod = a ^ count a s
have h₁ : ∀ (a_1 : List M) (h : ∀ (a' : M), a' ≠ a → a' ∈ ⟦a_1⟧ → a' = 1), prod ⟦a_1⟧ = a ^ count a ⟦a_1⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
Goal:
M : Type u_5
inst : CommMonoid M
s : Multiset M
h : ∀ (x : M), x ∈ s → x = 1
⊢ s.prod = 1
have h₁ : ∀ (a : List M) (h : ∀ (x : M), x ∈ ⟦a⟧ → x = 1), prod ⟦a⟧ = 1
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Multiset.Basic (goal)
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
⊢ Eq.{u_6 + 1} (α := N) (prod (map (⇑f : (a : M) → N) s) : N) ((f : (a : M) → N) s.prod : N)
have 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)
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, hs