awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
s_1 : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
exact card_union_le ..

Premises used: Finset.card_union_le
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
s_1 : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ ∑ a ∈ insert a s, #(t a)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
f : ι → M
s : Finset ι
t : Finset M
H : Set.MapsTo f (↑s : Set ι) (↑t : Set M)
⊢ #s = ∑ b ∈ t, #({a ∈ s | f a = b})

Tactic:
simp only [card_eq_sum_ones, sum_fiberwise_of_maps_to H]

Premises used: Finset.card_eq_sum_ones, Finset.sum_fiberwise_of_maps_to
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
f : ι → M
s : Finset ι
⊢ #s = ∑ b ∈ image f s, #({a ∈ s | f a = b})

Tactic:
card_eq_sum_card_fiberwise fun _ => mem_image_of_mem _

Premises used: Finset.card_eq_sum_card_fiberwise, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ Set.MapsTo e (↑univ : Set ι) (↑univ : Set κ)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ (i : κ), Membership.mem (γ := Finset κ) univ i → i ∉ e '' (↑univ : Set ι) → g i = 1

Tactic:
simpa using h'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : ι → M
rw : Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ j : κ, ∏ i : ι with g i = j, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ i : ι, f i)

Tactic:
rw [← Finset.prod_fiberwise _ g f]

Premises used: Finset.prod_fiberwise
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : ι → M
e_f : ∀ (j : κ), Eq.{u_4 + 1} (α := M) (∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ i : ι with g i = j, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ j : κ, ∏ i : ι with g i = j, f i)

Tactic:
congr with j
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : ι → M
j : κ
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) {i : ι | g i = j} x ↔ g x = j

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : ι → M
j : κ
⊢ Eq.{u_4 + 1} (α := M) (∏ i : { i : ι // g i = j }, f (↑i : ι)) (∏ i : ι with g i = j, f i)

Tactic:
exact (prod_subtype _ (by simp) _).symm

Premises used: Finset.prod_subtype, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : κ → M
rw : Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ _i : { i : ι // g i = j }, f j) (∏ j : κ, ∏ i : ι with g i = j, f j)
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ _i : { i : ι // g i = j }, f j) (∏ i : ι, f (g i))

Tactic:
rw [← Finset.prod_fiberwise' _ g f]

Premises used: Finset.prod_fiberwise'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : κ → M
e_f : ∀ (j : κ), Eq.{u_4 + 1} (α := M) (∏ _i : { i : ι // g i = j }, f j) (∏ i : ι with g i = j, f j)
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ _i : { i : ι // g i = j }, f j) (∏ j : κ, ∏ i : ι with g i = j, f j)

Tactic:
congr with j
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : κ → M
j : κ
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) {i : ι | g i = j} x ↔ g x = j

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : Fintype κ
inst_2 : CommMonoid M
inst_3 : DecidableEq κ
g : ι → κ
f : κ → M
j : κ
⊢ Eq.{u_4 + 1} (α := M) (∏ _i : { i : ι // g i = j }, f j) (∏ i : ι with g i = j, f j)

Tactic:
exact (prod_subtype _ (by simp) fun _ ↦ _).symm

Premises used: Finset.prod_subtype, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Unique ι
f : ι → M
rw : ∏ x ∈ {default}, f x = f default
rw₁ rw₂ : f default = f default
⊢ ∏ x : ι, f x = f default

Tactic:
rw [univ_unique, prod_singleton]

Premises used: Finset.prod_singleton, Finset.univ_unique
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Subsingleton ι
f : ι → M
a : ι
have : ∀ (this : Unique ι), ∏ x : ι, f x = f a
⊢ ∏ x : ι, f x = f a

Tactic:
have : Unique ι := uniqueOfSubsingleton a
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
rw : f default = f a
rw₁ rw₂ : f a = f a
⊢ ∏ x : ι, f x = f a

Tactic:
rw [prod_unique f, Subsingleton.elim default a]

Premises used: Inhabited.default, Fintype.prod_unique, Subsingleton.elim
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : Prop → M
⊢ ∏ p : Prop, f p = f True * f False

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
rw : HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
h : ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
h₁ : ∀ (x : ι), x ∈ s ↔ p x
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i

Tactic:
rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]

Premises used: Compl.compl, Finset.prod_subtype
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
⊢ HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i

Tactic:
Finset.prod_mul_prod_compl _ _

Premises used: Finset.prod_mul_prod_compl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
⊢ HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i

Tactic:
exact Finset.prod_mul_prod_compl _ _

Premises used: Finset.prod_mul_prod_compl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

Tactic:
simp [s]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
s : Finset ι := Set.toFinset {x : ι | p x}
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
simp [s]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
p : ι → Prop
f : ι → M
inst_2 : DecidablePred p
let let₁ let₂ :
  HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i
let₃ :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  HMul.hMul (α := M) (∏ a ∈ s, f a) (∏ a ∈ sᶜ, f a) = ∏ i : ι, f i
h :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
h₁ :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  ∀ (x : ι), x ∈ s ↔ p x
h₂ :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
h₃ h₄ :
  let s : Finset ι := Set.toFinset {x : ι | p x};
  ∀ (x : ι), x ∈ s ↔ p x
⊢ HMul.hMul (α := M) (∏ i : { x : ι // p x }, f (↑i : ι)) (∏ i : { x : ι // ¬p x }, f (↑i : ι)) = ∏ i : ι, f i

Tactic:
classical
    let s := { x | p x }.toFinset
    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
    · exact Finset.prod_mul_prod_compl _ _
    · simp [s]
    · simp [s]

Premises used: Finset.prod_mul_prod_compl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_7
inst : Fintype ι
inst_1 : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ (i : ι), f i ≠ 1 → i ∈ s
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) univ x → x ∉ s → f x = 1

Tactic:
simpa [not_imp_comm (a := _ ∈ s)]

Premises used: not_imp_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid M
f : ι → M
h : Nodup.{u_1} (α := ι) []
⊢ Finset.prod (toFinset []) f = (map f []).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid M
f : ι → M
a : ι
l : List ι
hl : (a :: l).Nodup
⊢ a ∉ l

Tactic:
let ⟨notMem, hl⟩ := List.nodup_cons.mp hl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid M
f : ι → M
a : ι
l : List ι
hl : (a :: l).Nodup
notMem : a ∉ l
⊢ l.Nodup

Tactic:
let ⟨notMem, hl⟩ := List.nodup_cons.mp hl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid M
f : ι → M
a : ι
l : List ι
hl_1 : (a :: l).Nodup
notMem : a ∉ l
hl : l.Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod

Tactic:
simp [Finset.prod_insert (mt List.mem_toFinset.mp notMem), prod_toFinset _ hl]

Premises used: List.mem_toFinset, Finset.prod_insert, mt, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
l : List ι
⊢ ∑ a ∈ l.toFinset, count a l = l.length

Tactic:
simpa [List.map_const'] using (Finset.sum_list_map_count l fun _ => (1 : ℕ)).symm

Premises used: List.map_const', OfNat.ofNat, Eq.symm, Finset.sum_list_map_count
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
a : M
m : ι → Multiset M
⊢ Membership.mem (γ := Multiset M) (∑ i ∈ ∅, m i) a ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ m i

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
a : M
m : ι → Multiset M
a_1 : ι
s : Finset ι
h : a_1 ∉ s
h_1 : Membership.mem (γ := Multiset M) (∑ i ∈ s, m i) a ↔ ∃ i ∈ s, a ∈ m i
⊢ Membership.mem (γ := Multiset M) (∑ i ∈ Finset.cons a_1 s h, m i) a ↔ ∃ i ∈ Finset.cons a_1 s h, a ∈ m i

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
a : M
s : Finset ι
m : ι → Multiset M
empty : Membership.mem (γ := Multiset M) (∑ i ∈ ∅, m i) a ↔ ∃ (i : ι), Membership.mem (γ := Finset ι) ∅ i ∧ a ∈ m i
cons :
  ∀ (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
    (Membership.mem (γ := Multiset M) (∑ i ∈ s, m i) a ↔ ∃ i ∈ s, a ∈ m i) →
      (Membership.mem (γ := Multiset M) (∑ i ∈ Finset.cons a_1 s h, m i) a ↔ ∃ i ∈ Finset.cons a_1 s h, a ∈ m i)
⊢ Membership.mem (γ := Multiset M) (∑ i ∈ s, m i) a ↔ ∃ i ∈ s, a ∈ m i

Tactic:
induction s using Finset.cons_induction with grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → α → M
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
f : ι → α → M
a : α
s : Finset α
ha : a ∉ s
ih : Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ insert a s, f i a) m))
    (∏ a ∈ insert a s, prod (map (fun (i : ι) ↦ f i a) m))

Tactic:
simp [Finset.prod_insert ha, prod_map_mul, ih]

Premises used: Finset.prod_insert, Multiset.prod_map_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
empty :
  Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ih :
      Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m))
        (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))),
    Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ Insert.insert a s, f i a) m))
      (∏ a ∈ Insert.insert a s, prod (map (fun (i : ι) ↦ f i a) m))
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]

Premises used: Insert.insert, Multiset.prod_map_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
α : Type u_5
inst : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
empty :
  Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ ∅, f i a) m)) (∏ a ∈ ∅, prod (map (fun (i : ι) ↦ f i a) m))
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s)
    (ih :
      Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m))
        (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))),
    Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ Insert.insert a s, f i a) m))
      (∏ a ∈ Insert.insert a s, prod (map (fun (i : ι) ↦ f i a) m))
⊢ Eq.{u_4 + 1} (α := M) (prod (map (fun (i : ι) ↦ ∏ a ∈ s, f i a) m)) (∏ a ∈ s, prod (map (fun (i : ι) ↦ f i a) m))

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]

Premises used: Insert.insert, Multiset.prod_map_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, count a s = s.card

Tactic:
simpa using (Finset.sum_multiset_map_count s (fun _ => (1 : ℕ))).symm

Premises used: Finset.sum_multiset_map_count, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
rw : Eq (α := ℕ) (∑ x ∈ s with count x m ≠ 0, count x m) (∑ a ∈ m.toFinset, count a m)
⊢ ∑ a ∈ s, count a m = m.card

Tactic:
rw [← toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]

Premises used: Multiset.toFinset_sum_count_eq, Finset.sum_filter_ne_zero
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
e_s : ∀ (a : ι), a ∈ {x ∈ s | count x m ≠ 0} ↔ a ∈ m.toFinset
⊢ Eq (α := ℕ) (∑ x ∈ s with count x m ≠ 0, count x m) (∑ a ∈ m.toFinset, count a m)

Tactic:
congr with a
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
a : ι
⊢ a ∈ {x ∈ s | count x m ≠ 0} ↔ a ∈ m.toFinset

Tactic:
simpa using hms a
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
rw : sum (map singleton s) = s
rw₁ rw₂ : s = s
⊢ ∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s) {a} = s

Tactic:
rw [← Finset.sum_multiset_map_count, Multiset.sum_map_singleton]

Premises used: Finset.sum_multiset_map_count, Multiset.sum_map_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₁ : s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})
⊢ ∃ (u : Multiset ι), s = k • u

Tactic:
use ∑ a ∈ s.toFinset, (s.count a / k) • {a}

Premises used: Multiset.toFinset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
apply :
  ∀ x ∈ s.toFinset,
    k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
⊢ Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
rw : HSMul.hSMul (β := Multiset ι) (k * (count x s / k)) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
rw₁ rw₂ : HSMul.hSMul (β := Multiset ι) (count x s) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}
⊢ k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x} = HSMul.hSMul (β := Multiset ι) (count x s) {x}

Tactic:
rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]

Premises used: mul_nsmul', Iff.mp, Multiset.mem_toFinset, Nat.mul_div_cancel'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})

Tactic:
have h₂ :
    (∑ x ∈ s.toFinset, k • (count x s / k) • ({x} : Multiset ι)) =
      ∑ x ∈ s.toFinset, count x s • {x} := by
    apply Finset.sum_congr rfl
    intro x hx
    rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ :
  Eq (α := Multiset ι) (∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x})
    (∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x})
h₁ : s = ∑ x ∈ s.toFinset, k • HSMul.hSMul (β := Multiset ι) (count x s / k) {x}
h₃ : s = ∑ x ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count x s) {x}
h₄ h₅ : s = s
⊢ s = HSMul.hSMul (β := Multiset ι) k (∑ a ∈ s.toFinset, HSMul.hSMul (β := Multiset ι) (count a s / k) {a})

Tactic:
rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]

Premises used: Finset.sum_nsmul, Multiset.toFinset_sum_count_nsmul_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_5
inst : CommMonoid M
f : ι → Multiset M
⊢ Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ ∅, f x)) (∏ x ∈ ∅, (f x).prod)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_5
inst : CommMonoid M
f : ι → Multiset M
a : ι
s : Finset ι
h : a ∉ s
h_1 : Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ s, f x)) (∏ x ∈ s, (f x).prod)
⊢ Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ Finset.cons a s h, f x)) (∏ x ∈ Finset.cons a s h, (f x).prod)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
ι : Type u_5
inst : CommMonoid M
f : ι → Multiset M
s : Finset ι
empty : Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ ∅, f x)) (∏ x ∈ ∅, (f x).prod)
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ s, f x)) (∏ x ∈ s, (f x).prod) →
      Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ Finset.cons a s h, f x)) (∏ x ∈ Finset.cons a s h, (f x).prod)
⊢ Eq.{u_4 + 1} (α := M) (prod (∑ x ∈ s, f x)) (∏ x ∈ s, (f x).prod)

Tactic:
induction s using Finset.cons_induction with grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
⊢ IsUnit.{u_4} (M := M) (∏ a ∈ ∅, f a) ↔ ∀ (a : ι), Membership.mem (γ := Finset ι) ∅ a → IsUnit (f a)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
a : ι
s_1 : Finset ι
h : a ∉ s_1
h_1 : IsUnit.{u_4} (M := M) (∏ a ∈ s_1, f a) ↔ ∀ a ∈ s_1, IsUnit (f a)
⊢ IsUnit.{u_4} (M := M) (∏ a ∈ Finset.cons a s_1 h, f a) ↔ ∀ a_1 ∈ Finset.cons a s_1 h, IsUnit (f a_1)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
empty : IsUnit.{u_4} (M := M) (∏ a ∈ ∅, f a) ↔ ∀ (a : ι), Membership.mem (γ := Finset ι) ∅ a → IsUnit (f a)
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (IsUnit.{u_4} (M := M) (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)) →
      (IsUnit.{u_4} (M := M) (∏ a ∈ Finset.cons a s h, f a) ↔ ∀ a_2 ∈ Finset.cons a s h, IsUnit (f a_2))
⊢ IsUnit.{u_4} (M := M) (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)

Tactic:
induction s using Finset.cons_induction with grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
f : ι → M
⊢ IsUnit.{u_4} (M := M) (∏ a : ι, f a) ↔ ∀ (a : ι), IsUnit (f a)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
f : ι → ℤ
⊢ natAbs (∑ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, (f i).natAbs

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
f : ι → ℤ
a : ι
s : Finset ι
h : a ∉ s
h_1 : natAbs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natAbs
⊢ natAbs (∑ i ∈ Finset.cons a s h, f i) ≤ ∑ i ∈ Finset.cons a s h, (f i).natAbs

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℤ
empty : natAbs (∑ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, (f i).natAbs
cons :
  ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    natAbs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natAbs →
      natAbs (∑ i ∈ Finset.cons a s h, f i) ≤ ∑ i ∈ Finset.cons a s h, (f i).natAbs
⊢ natAbs (∑ i ∈ s, f i) ≤ ∑ i ∈ s, (f i).natAbs

Tactic:
induction s using Finset.cons_induction with grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Multiset ι
hs : s.Nodup
f : ι → M
⊢ { val := s, nodup := hs : Finset ι }.prod f = (Multiset.map f s).prod

Tactic:
rfl

Premises used: Finset.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
M : Type u_3
inst : CommMonoid M
s : Finset M
rw : s.val.prod = (Multiset.map id s.val).prod
rw₁ rw₂ : s.val.prod = s.val.prod
⊢ s.val.prod = s.prod id

Tactic:
rw [Finset.prod, Multiset.map_id]

Premises used: Multiset.map_id, Finset.prod
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x = (Multiset.map f s.val).prod

Tactic:
rfl

Premises used: Finset.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
⊢ (Multiset.map f s.val).prod = ∏ a ∈ s, f a

Tactic:
rfl

Premises used: Finset.prod, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs
Goal:
ι : Type u_1
s : Finset ι
⊢ ∑ a ∈ s, {a} = s.val

Tactic:
simp only [sum_eq_multiset_sum, Multiset.sum_map_singleton]

Premises used: Finset.sum_eq_multiset_sum, Multiset.sum_map_singleton