awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : T ⊆ S
IH : (map g1 T).prod ∣ (map g2 T).prod
⊢ (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod

Tactic:
simp [mul_dvd_mul (h a haS) IH]

Premises used: mul_dvd_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
⊢ Eq.{u_5 + 1} (α := (a : Multiset M) → M) (⇑sumAddMonoidHom : (a : Multiset M) → M) sum

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset G
⊢ (map Inv.inv m).prod = m.prod⁻¹

Tactic:
m.prod_hom (invMonoidHom : G →* G)

Premises used: invMonoidHom, Multiset.prod_hom
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
rw : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map Inv.inv (map f m)).prod
rw₁ : prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map (Inv.inv ∘ f) m).prod
rw₂ rw₃ : Eq.{u_4 + 1} (α := G) (prod (map (fun (i : ι) ↦ (f i)⁻¹) m)) (prod (map (fun (x : ι) ↦ (f x)⁻¹) m))
⊢ prod (map (fun (i : ι) ↦ (f i)⁻¹) m) = (map f m).prod⁻¹

Tactic:
rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]

Premises used: Multiset.map, Multiset.prod_map_inv', Function.comp_def, Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f g : ι → G
⊢ prod (map (fun (i : ι) ↦ f i / g i) m) = (map f m).prod / (map g m).prod

Tactic:
m.prod_hom₂ (· / ·) mul_div_mul_comm (div_one _) _ _

Premises used: HDiv.hDiv, Multiset.prod_hom₂
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
⊢ Eq (α := G) (prod (map (⇑(zpowGroupHom n) : (a : G) → G) (map f m)) : G)
    ((zpowGroupHom n : (a : G) → G) (map f m).prod : G)

Tactic:
(m.map f).prod_hom (zpowGroupHom n : G →* G)

Premises used: Multiset.map, zpowGroupHom, Multiset.prod_hom
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
h : Eq (α := Multiset G) (map (fun (i : ι) ↦ f i ^ n) m) (map (⇑(zpowGroupHom n) : (a : G) → G) (map f m))
⊢ prod (map (fun (i : ι) ↦ f i ^ n) m) = (map f m).prod ^ n

Tactic:
convert! (m.map f).prod_hom (zpowGroupHom n : G →* G)

Premises used: Multiset.map, zpowGroupHom, Multiset.prod_hom
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
G : Type u_4
inst : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
⊢ Eq (α := Multiset G) (map (fun (i : ι) ↦ f i ^ n) m) (map (⇑(zpowGroupHom n) : (a : G) → G) (map f m))

Tactic:
simp only [map_map, Function.comp_apply, zpowGroupHom_apply]

Premises used: zpowGroupHom_apply, Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
s : Multiset M
⊢ Eq.{u_5 + 1} (α := Multiset M) (sum (map (fun (a : M) ↦ {a}) 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
M : Type u_5
s : Multiset M
⊢ ∀ (a : M) (s : Multiset M), sum (map (fun (a : M) ↦ {a}) s) = s → sum (map (fun (a : M) ↦ {a}) (a ::ₘ s)) = a ::ₘ s

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
s : Multiset ℕ
n : ℕ
empty : sum 0 % n = sum (map (fun (x : ℕ) ↦ x % n) 0) % n
cons :
  ∀ (a : ℕ) (s : Multiset ℕ),
    s.sum % n = sum (map (fun (x : ℕ) ↦ x % n) s) % n →
      (a ::ₘ s).sum % n = sum (map (fun (x : ℕ) ↦ x % n) (a ::ₘ s)) % n
⊢ s.sum % n = sum (map (fun (x : ℕ) ↦ x % n) s) % n

Tactic:
induction s using Multiset.induction
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n : ℕ
⊢ sum 0 % n = sum (map (fun (x : ℕ) ↦ x % n) 0) % n

Tactic:
simp [Nat.add_mod, *]

Premises used: Nat.add_mod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n a : ℕ
s : Multiset ℕ
h : s.sum % n = sum (map (fun (x : ℕ) ↦ x % n) s) % n
⊢ (a ::ₘ s).sum % n = sum (map (fun (x : ℕ) ↦ x % n) (a ::ₘ s)) % n

Tactic:
simp [Nat.add_mod, *]

Premises used: Nat.add_mod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
s : Multiset ℕ
n : ℕ
empty : prod 0 % n = prod (map (fun (x : ℕ) ↦ x % n) 0) % n
cons :
  ∀ (a : ℕ) (s : Multiset ℕ),
    s.prod % n = prod (map (fun (x : ℕ) ↦ x % n) s) % n →
      (a ::ₘ s).prod % n = prod (map (fun (x : ℕ) ↦ x % n) (a ::ₘ s)) % n
⊢ s.prod % n = prod (map (fun (x : ℕ) ↦ x % n) s) % n

Tactic:
induction s using Multiset.induction
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n : ℕ
⊢ prod 0 % n = prod (map (fun (x : ℕ) ↦ x % n) 0) % n

Tactic:
simp [Nat.mul_mod, *]

Premises used: Nat.mul_mod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n a : ℕ
s : Multiset ℕ
h : s.prod % n = prod (map (fun (x : ℕ) ↦ x % n) s) % n
⊢ (a ::ₘ s).prod % n = prod (map (fun (x : ℕ) ↦ x % n) (a ::ₘ s)) % n

Tactic:
simp [Nat.mul_mod, *]

Premises used: Nat.mul_mod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
s : Multiset ℤ
n : ℤ
empty : sum 0 % n = sum (map (fun (x : ℤ) ↦ x % n) 0) % n
cons :
  ∀ (a : ℤ) (s : Multiset ℤ),
    s.sum % n = sum (map (fun (x : ℤ) ↦ x % n) s) % n →
      (a ::ₘ s).sum % n = sum (map (fun (x : ℤ) ↦ x % n) (a ::ₘ s)) % n
⊢ s.sum % n = sum (map (fun (x : ℤ) ↦ x % n) s) % n

Tactic:
induction s using Multiset.induction
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n : ℤ
⊢ sum 0 % n = sum (map (fun (x : ℤ) ↦ x % n) 0) % n

Tactic:
simp [Int.add_emod, *]

Premises used: Int.add_emod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n a : ℤ
s : Multiset ℤ
h : s.sum % n = sum (map (fun (x : ℤ) ↦ x % n) s) % n
⊢ (a ::ₘ s).sum % n = sum (map (fun (x : ℤ) ↦ x % n) (a ::ₘ s)) % n

Tactic:
simp [Int.add_emod, *]

Premises used: Int.add_emod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
s : Multiset ℤ
n : ℤ
empty : prod 0 % n = prod (map (fun (x : ℤ) ↦ x % n) 0) % n
cons :
  ∀ (a : ℤ) (s : Multiset ℤ),
    s.prod % n = prod (map (fun (x : ℤ) ↦ x % n) s) % n →
      (a ::ₘ s).prod % n = prod (map (fun (x : ℤ) ↦ x % n) (a ::ₘ s)) % n
⊢ s.prod % n = prod (map (fun (x : ℤ) ↦ x % n) s) % n

Tactic:
induction s using Multiset.induction
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n : ℤ
⊢ prod 0 % n = prod (map (fun (x : ℤ) ↦ x % n) 0) % n

Tactic:
simp [Int.mul_emod, *]

Premises used: Int.mul_emod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
n a : ℤ
s : Multiset ℤ
h : s.prod % n = prod (map (fun (x : ℤ) ↦ x % n) s) % n
⊢ (a ::ₘ s).prod % n = prod (map (fun (x : ℤ) ↦ x % n) (a ::ₘ s)) % n

Tactic:
simp [Int.mul_emod, *]

Premises used: Int.mul_emod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : ExistsAddOfLE M
inst_3 : AddLeftMono M
inst_4 : AddLeftReflectLE M
inst_5 : Sub M
inst_6 : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
rw : sum (map (fun (i : ι) ↦ f i - g i + g i) l) = (map f l).sum
⊢ sum (map (fun (x : ι) ↦ f x - g x) l) + (map g l).sum = (map f l).sum

Tactic:
rw [← sum_map_add]

Premises used: Multiset.sum_map_add
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : ExistsAddOfLE M
inst_3 : AddLeftMono M
inst_4 : AddLeftReflectLE M
inst_5 : Sub M
inst_6 : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
e_a : map (fun (i : ι) ↦ f i - g i + g i) l = map f l
⊢ sum (map (fun (i : ι) ↦ f i - g i + g i) l) = (map f l).sum

Tactic:
congr 1
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : ExistsAddOfLE M
inst_3 : AddLeftMono M
inst_4 : AddLeftReflectLE M
inst_5 : Sub M
inst_6 : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ map (fun (i : ι) ↦ f i - g i + g i) l = map f l

Tactic:
map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

Premises used: tsub_add_cancel_of_le, Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
ι : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : ExistsAddOfLE M
inst_3 : AddLeftMono M
inst_4 : AddLeftReflectLE M
inst_5 : Sub M
inst_6 : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ map (fun (i : ι) ↦ f i - g i + g i) l = map f l

Tactic:
exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

Premises used: tsub_add_cancel_of_le, Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Goal:
F : Type u_1
ι : Type u_2
κ : Type u_3
G : Type u_4
M_1 : Type u_5
N : Type u_6
O : Type u_7
M : Type u_8
n : ℕ
hn : n ≠ 0
x y : Multiset M
h : Eq.{u_8 + 1} (α := Multiset M) ((fun (a : Multiset M) ↦ n • a) x) ((fun (a : Multiset M) ↦ n • a) y)
x_1 : M
⊢ n * count x_1 x = n * count x_1 y

Tactic:
simp only [← Multiset.count_nsmul, h]

Premises used: Multiset.count_nsmul
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
⊢ s.prod = foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 s

Tactic:
rfl

Premises used: Multiset.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
⊢ Eq (α := M) (foldl (fun (x y : M) ↦ y * x) 1 s) (foldl (fun (x1 x2 : M) ↦ x1 * x2) 1 s)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
l : List M
⊢ (↑l : Multiset M).prod = l.prod

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, rfl, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
rw : (↑s.toList : Multiset M).prod
| s.prod

Tactic:
rw [← coe_toList s]

Premises used: Multiset.coe_toList
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
conv_rhs : s.toList.prod = (↑s.toList : Multiset M).prod
⊢ s.toList.prod = s.prod

Tactic:
conv_rhs => rw [← coe_toList s]

Premises used: Multiset.coe_toList
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
rw rw₁ : s.toList.prod = s.toList.prod
⊢ s.toList.prod = (↑s.toList : Multiset M).prod

Tactic:
rw [prod_coe]

Premises used: Multiset.prod_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
s : Multiset ι
f : ι → M
rw : (↑(List.map f s.toList) : Multiset M).prod = (map f s).prod
rw₁ : (map f (↑s.toList : Multiset ι)).prod = (map f s).prod
rw₂ rw₃ : (map f s).prod = (map f s).prod
⊢ (List.map f s.toList).prod = (map f s).prod

Tactic:
rw [← Multiset.prod_coe, ← Multiset.map_coe, coe_toList]

Premises used: Multiset.coe_toList, Multiset.map_coe, Multiset.prod_coe
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
⊢ Eq.{u_3 + 1} (α := M) (prod 0) 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, List.foldr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
a : M
s : Multiset M
⊢ (a ::ₘ s).prod = a * s.prod

Tactic:
foldr_cons _ _ _ _

Premises used: Multiset.prod, Multiset.foldr_cons
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
a : M
⊢ prod {a} = a

Tactic:
simp only [mul_one, prod_cons, ← cons_zero, prod_zero]

Premises used: Multiset.prod_zero, Multiset.prod_cons, mul_one, Multiset.cons_zero
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
a b : M
rw : (a ::ₘ {b}).prod = a * b
rw₁ : a * prod {b} = a * b
rw₂ rw₃ : a * b = a * b
⊢ prod {a, b} = a * b

Tactic:
rw [insert_eq_cons, prod_cons, prod_singleton]

Premises used: Multiset.prod_cons, Multiset.prod_singleton, Multiset.insert_eq_cons
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
simp [replicate, List.prod_replicate]

Premises used: Multiset.replicate, List.prod_replicate
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
inst_1 : DecidableEq M
a : M
rw : a ^ count a s = (replicate (count a s) a).prod
rw₁ rw₂ : a ^ count a s = a ^ count a s
⊢ a ^ count a s = (filter (Eq a) s).prod

Tactic:
rw [filter_eq, prod_replicate]

Premises used: Multiset.prod_replicate, Multiset.filter_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
ι : Type u_2
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
s : Multiset ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (map f ⟦l⟧).prod (map g ⟦l⟧).prod

Tactic:
simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]

Premises used: Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe, List.prod_hom_rel
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
ι : Type u_2
M : Type u_3
inst : CommMonoid M
m : Multiset ι
rw : Eq.{u_3 + 1} (α := M) (prod (replicate m.card 1)) 1
rw₁ : HPow.hPow (α := M) 1 m.card = 1
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 1 1
⊢ Eq.{u_3 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) m)) 1

Tactic:
rw [map_const', prod_replicate, one_pow]

Premises used: one_pow, Multiset.prod_replicate, Multiset.map_const'
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
rw : p (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 s)
⊢ p s.prod

Tactic:
rw [prod_eq_foldr]

Premises used: Multiset.prod_eq_foldr
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 s)

Tactic:
foldr_induction (· * ·) 1 p s p_mul p_one p_s

Premises used: HMul.hMul, Multiset.foldr_induction, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun (x1 x2 : M) ↦ x1 * x2) 1 s)

Tactic:
exact foldr_induction (· * ·) 1 p s p_mul p_one p_s

Premises used: HMul.hMul, Multiset.foldr_induction, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : Ne.{u_3 + 1} (α := Multiset M) 0 ∅
p_s : ∀ (a : M), Membership.mem (γ := Multiset M) 0 a → p a
⊢ p (prod 0)

Tactic:
simp at hs
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
cons : p (a * s.prod)
⊢ p (a ::ₘ s).prod

Tactic:
rw [prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
pos : ∀ (hs_empty : s = ∅), p (a * s.prod)
neg : ∀ (hs_empty : ¬s = ∅), p (a * s.prod)
⊢ p (a * s.prod)

Tactic:
by_cases hs_empty : s = ∅
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : s = ∅
⊢ p (a * s.prod)

Tactic:
simp [hs_empty, p_s a]
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
neg : ∀ (hps : ∀ (x : M), x ∈ s → p x), p (a * s.prod)
⊢ p (a * s.prod)

Tactic:
have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hps : ∀ (x : M), x ∈ s → p x
⊢ p (a * s.prod)

Tactic:
p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)

Premises used: Multiset.prod, Multiset.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s_1 : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hps : ∀ (x : M), x ∈ s → p x
⊢ p (a * s.prod)

Tactic:
exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)

Premises used: Multiset.prod, Multiset.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : s ≠ ∅
p_s : ∀ (a : M), a ∈ s → p a
empty :
  ∀ (hs : Ne.{u_3 + 1} (α := Multiset M) 0 ∅) (p_s : ∀ (a : M), Membership.mem (γ := Multiset M) 0 a → p a), p (prod 0)
cons :
  ∀ (a : M) (s : Multiset M) (hsa : ∀ (hs : s ≠ ∅) (p_s : ∀ (a : M), a ∈ s → p a), p s.prod) (hs : a ::ₘ s ≠ ∅)
    (p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1), p (a ::ₘ s).prod
⊢ p s.prod

Tactic:
induction s using Multiset.induction_on with
  | empty => simp at hs
  | cons a s hsa =>
    rw [prod_cons]
    by_cases hs_empty : s = ∅
    · simp [hs_empty, p_s a]
    have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
    exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)

Premises used: Multiset.prod_cons, Multiset.cons
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : AddMonoid N
inst_1 : DistribSMul M N
r : M
l : List N
⊢ r • l.sum = sum (map (fun (x : N) ↦ r • x) l)

Tactic:
map_list_sum (DistribSMul.toAddMonoidHom N r) l

Premises used: map_list_sum, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulDistribMulAction M N
r : M
l : List N
⊢ r • l.prod = prod (map (fun (x : N) ↦ r • x) l)

Tactic:
map_list_prod (MulDistribMulAction.toMonoidHom N r) l

Premises used: map_list_prod, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid N
inst_1 : DistribSMul M N
r : M
s : Multiset N
⊢ r • s.sum = sum (map (fun (x : N) ↦ r • x) s)

Tactic:
(DistribSMul.toAddMonoidHom N r).map_multiset_sum s

Premises used: AddMonoidHom.map_multiset_sum, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
γ : Type u_3
inst : AddCommMonoid N
inst_1 : DistribSMul M N
r : M
f : γ → N
s : Finset γ
⊢ HSMul.hSMul (β := N) r (∑ x ∈ s, f x) = ∑ x ∈ s, r • f x

Tactic:
map_sum (DistribSMul.toAddMonoidHom N r) f s

Premises used: map_sum, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
γ : Type u_3
inst : AddCommMonoid N
inst_1 : DistribSMul M N
r : M
f : γ → N
s : Set γ
hs : s.Finite
⊢ HSMul.hSMul (β := N) r (∑ᶠ (x : γ) (_ : x ∈ s), f x) = ∑ᶠ (x : γ) (_ : x ∈ s), r • f x

Tactic:
(DistribSMul.toAddMonoidHom N r).map_finsum_mem f hs

Premises used: DistribSMul.toAddMonoidHom, AddMonoidHom.map_finsum_mem
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulDistribMulAction M N
r : M
s : Multiset N
⊢ r • s.prod = prod (map (fun (x : N) ↦ r • x) s)

Tactic:
(MulDistribMulAction.toMonoidHom N r).map_multiset_prod s

Premises used: MonoidHom.map_multiset_prod, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
γ : Type u_3
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulDistribMulAction M N
r : M
f : γ → N
s : Finset γ
⊢ HSMul.hSMul (β := N) r (∏ x ∈ s, f x) = ∏ x ∈ s, r • f x

Tactic:
map_prod (MulDistribMulAction.toMonoidHom N r) f s

Premises used: map_prod, MulDistribMulAction.toMonoidHom
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulDistribMulAction M N
ι : Sort u_4
inst_3 : Finite ι
f : ι → N
r : M
intro : ∀ (val : Fintype (PLift ι)), HSMul.hSMul (β := N) r (∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), r • f x
⊢ HSMul.hSMul (β := N) r (∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), r • f x

Tactic:
cases nonempty_fintype (PLift ι)

Premises used: PLift, nonempty_fintype
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulDistribMulAction M N
ι : Sort u_4
inst_3 : Finite ι
f : ι → N
r : M
val : Fintype (PLift ι)
⊢ Function.mulSupport (?m.44 ∘ PLift.down) ⊆ (↑Finset.univ : Set (PLift ?m.42))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : CommMonoid N
inst_2 : MulDistribMulAction M N
ι : Sort u_4
inst_3 : Finite ι
f : ι → N
r : M
val : Fintype (PLift ι)
⊢ HSMul.hSMul (β := N) r (∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), r • f x

Tactic:
simp only [finprod_eq_prod_plift_of_mulSupport_subset (s := Finset.univ) (by simp),
    Finset.smul_prod']

Premises used: finprod_eq_prod_plift_of_mulSupport_subset, Finset.smul_prod'
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
N : Type u_2
inst : CommMonoid N
G : Type u_4
inst_1 : Group G
inst_2 : MulDistribMulAction G N
inst_3 : Fintype G
b : N
g : G
simp : Eq.{u_2 + 1} (α := N) (∏ x : G, (g * x) • b) (∏ h : G, h • b)
⊢ HSMul.hSMul (β := N) g (∏ h : G, h • b) = ∏ h : G, h • b

Tactic:
simp only [smul_prod', smul_smul]

Premises used: smul_smul, Finset.smul_prod'
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
N : Type u_2
inst : CommMonoid N
G : Type u_4
inst_1 : Group G
inst_2 : MulDistribMulAction G N
inst_3 : Fintype G
b : N
g : G
⊢ ∀ (i : G), Membership.mem (γ := Finset G) univ i ↔ Membership.mem (γ := Finset G) univ ((fun (x : G) ↦ g * x) i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
N : Type u_2
inst : CommMonoid N
G : Type u_4
inst_1 : Group G
inst_2 : MulDistribMulAction G N
inst_3 : Fintype G
b : N
g : G
⊢ Eq.{u_2 + 1} (α := N) (∏ x : G, (g * x) • b) (∏ h : G, h • b)

Tactic:
exact Finset.prod_bijective (g * ·) (Group.mulLeft_bijective g) (by simp) (fun _ _ ↦ rfl)

Premises used: HMul.hMul, Finset.prod_bijective, Group.mulLeft_bijective, rfl
-- Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action
Goal:
N : Type u_2
inst : CommMonoid N
G : Type u_4
inst_1 : Group G
inst_2 : MulDistribMulAction G N
inst_3 : Finite G
b : N
g : G
intro : ∀ (val : Fintype G), HSMul.hSMul (β := N) g (∏ᶠ (h : G), h • b) = ∏ᶠ (h : G), h • b
⊢ HSMul.hSMul (β := N) g (∏ᶠ (h : G), h • b) = ∏ᶠ (h : G), h • b

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype