awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f_1 : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
refine_2 :
  n ≠ 0 →
    Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
        (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) →
      Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) =
        (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a n + f))
⊢ n ≠ 0 →
    Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
        (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) →
      Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) =
        (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a n + f))

Tactic:
_
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f_1 : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih :
  Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)
refine_2 :
  HAdd.hAdd (β := Multiset β)
      (HSMul.hSMul (β := Multiset β) n ((Multiset.mapAddMonoidHom g : (a : Multiset α) → Multiset β) {a} : Multiset β))
      ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) : Multiset β) =
    HAdd.hAdd (β := Multiset β) (HSMul.hSMul (β := Multiset β) n {g a})
      ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) : Multiset β)
⊢ Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) =
    (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g (single a n + f))

Tactic:
rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single,
      toMultiset_single, toMultiset_add, toMultiset_single, ← Multiset.coe_mapAddMonoidHom,
      (Multiset.mapAddMonoidHom g).map_nsmul]

Premises used: AddMonoidHom.map_nsmul, Finsupp.mapDomain_single, Finsupp.toMultiset_add, Multiset.mapAddMonoidHom, Finsupp.toMultiset_single, Multiset.map_add, Finsupp.mapDomain_add, Multiset.coe_mapAddMonoidHom
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
f_1 : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih :
  Multiset.map g ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = (toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f)
⊢ HAdd.hAdd (β := Multiset β)
      (HSMul.hSMul (β := Multiset β) n ((Multiset.mapAddMonoidHom g : (a : Multiset α) → Multiset β) {a} : Multiset β))
      ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) : Multiset β) =
    HAdd.hAdd (β := Multiset β) (HSMul.hSMul (β := Multiset β) n {g a})
      ((toMultiset : (a : β →₀ ℕ) → Multiset β) (mapDomain g f) : Multiset β)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
⊢ Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)

Tactic:
f.induction ?_ ?_

Premises used: Finsupp.induction
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
refine_1 :
  Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0))
    (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
refine_2 :
  ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n) →
          Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a b + f)))
            ((single a b + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)

Tactic:
refine f.induction ?_ ?_
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f : α →₀ ℕ
refine_1 : Eq.{u_1 + 1} (α := α) (Multiset.prod 0) (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
refine_1₁ : Eq.{u_1 + 1} (α := α) 1 (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)
refine_1₂ refine_1₃ : Eq.{u_1 + 1} (α := α) 1 1
⊢ Eq.{u_1 + 1} (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0))
    (prod 0 fun (a : α) (n : ℕ) ↦ a ^ n)

Tactic:
rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]

Premises used: Multiset.prod_zero, Finsupp.toMultiset_zero, Finsupp.prod_zero_index
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
refine_2 :
  a ∉ f.support →
    n ≠ 0 →
      Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n) →
        Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)))
          ((single a n + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ a ∉ f.support →
    n ≠ 0 →
      Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n) →
        Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)))
          ((single a n + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)

Tactic:
_
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
refine_2 :
  n ≠ 0 →
    Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n) →
      Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)))
        ((single a n + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ n ≠ 0 →
    Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n) →
      Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)))
        ((single a n + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)

Tactic:
_
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih : Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)
refine_2 : HPow.hPow (β := ℕ) a 0 = 1
⊢ Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)))
    ((single a n + f).prod fun (a : α) (n : ℕ) ↦ a ^ n)

Tactic:
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
      Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]

Premises used: Finsupp.prod_add_index', pow_add, Multiset.prod_singleton, Multiset.prod_nsmul, pow_zero, Finsupp.toMultiset_add, Multiset.prod_add, Finsupp.toMultiset_single, Finsupp.prod_single_index
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih : Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ HPow.hPow (β := ℕ) a 0 = 1

Tactic:
pow_zero a

Premises used: pow_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : CommMonoid α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
h : a ∉ f.support
h_1 : n ≠ 0
ih : Eq (α := α) (Multiset.prod ((toMultiset : (a : α →₀ ℕ) → Multiset α) f)) (f.prod fun (a : α) (n : ℕ) ↦ a ^ n)
⊢ HPow.hPow (β := ℕ) a 0 = 1

Tactic:
exact pow_zero a

Premises used: pow_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support

Tactic:
f.induction ?_ ?_

Premises used: Finsupp.induction
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
refine_1 :
  Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)
refine_2 :
  ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 →
        Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support →
          Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a b + f)) = (single a b + f).support
⊢ Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support

Tactic:
refine f.induction ?_ ?_
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
refine_1 : Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset 0) (support (M := ℕ) 0)
refine_1₁ : Eq.{u_1 + 1} (α := Finset α) ∅ (support (M := ℕ) 0)
refine_1₂ refine_1₃ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Finset α) (Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) 0)) (support (M := ℕ) 0)

Tactic:
rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]

Premises used: Finsupp.toMultiset_zero, Finsupp.support_zero, Multiset.toFinset_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
refine_2 : Disjoint (support (single a n)) f.support
⊢ Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) (single a n + f)) = (single a n + f).support

Tactic:
rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
      support_single _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]

Premises used: Finsupp.support_single, Multiset.toFinset_nsmul, Multiset.toFinset_add, Finsupp.support_add_eq, Finsupp.toMultiset_add, Finsupp.toMultiset_single, Multiset.toFinset_singleton
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
⊢ Disjoint (support (single a n)) f.support

Tactic:
Disjoint.mono_left support_single_subset ?_

Premises used: Disjoint.mono_left, Finsupp.support_single_subset
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
refine_2 : Disjoint {a} f.support
⊢ Disjoint (support (single a n)) f.support

Tactic:
refine Disjoint.mono_left support_single_subset ?_

Premises used: Disjoint.mono_left
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f_1 : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : Multiset.toFinset ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) = f.support
refine_2 refine_2₁ refine_2₂ refine_2₃ : a ∉ f.support
⊢ Disjoint {a} f.support

Tactic:
rwa [Finset.disjoint_singleton_left]

Premises used: Finset.disjoint_singleton_left
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
rw :
  Multiset.count a (f.sum fun (a : α) (n : ℕ) ↦ HSMul.hSMul (β := Multiset α) n {a}) =
    f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x})
⊢ Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) =
    f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x})

Tactic:
rw [toMultiset_apply]

Premises used: Finsupp.toMultiset_apply
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun (a : α) (n : ℕ) ↦ HSMul.hSMul (β := Multiset α) n {a}) =
    f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x})

Tactic:
map_sum (Multiset.countAddMonoidHom a) _ f.support

Premises used: Multiset.countAddMonoidHom, Finsupp.sum, Finsupp.support, Multiset.count, map_sum, Multiset.countP
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun (a : α) (n : ℕ) ↦ HSMul.hSMul (β := Multiset α) n {a}) =
    f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x})

Tactic:
exact map_sum (Multiset.countAddMonoidHom a) _ f.support

Premises used: Multiset.countAddMonoidHom, Finsupp.support, map_sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Eq (α := ℕ) (f.sum fun (x : α) (n : ℕ) ↦ Multiset.count a (HSMul.hSMul (β := Multiset α) n {x}))
    (f.sum fun (x : α) (n : ℕ) ↦ n * Multiset.count a {x})

Tactic:
simp only [Multiset.count_nsmul]

Premises used: Multiset.count_nsmul
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a a' : α
h : Ne (α := ℕ) ((f : (a : α) → ℕ) a' : ℕ) (0 : ℕ)
H : a' ≠ a
⊢ HMul.hMul (α := ℕ) ((f : (a : α) → ℕ) a' : ℕ) (Multiset.count a {a'}) = 0

Tactic:
simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]

Premises used: if_false, Ne.symm, MulZeroClass.mul_zero, Multiset.count_singleton
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : α →₀ ℕ
a : α
rw : HMul.hMul (α := ℕ) (β := ℕ) ((f : (a : α) → ℕ) a : ℕ) (1 : ℕ) = (f : (a : α) → ℕ) a
rw₁ rw₂ : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) ((f : (a : α) → ℕ) a : ℕ)
⊢ HMul.hMul (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (Multiset.count a {a}) = (f : (a : α) → ℕ) a

Tactic:
rw [Multiset.count_singleton_self, mul_one]

Premises used: Multiset.count_singleton_self, mul_one
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a :
  ∀ (a : α),
    Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
      Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
⊢ Eq (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g) : Multiset α)
    ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g : Multiset α)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a_1 : α
a :
  Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
    max (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f))
      (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) g))
a₁ : Eq (α := ℕ) ((f ⊔ g : (a : α) → ℕ) a_1 : ℕ) (max ((f : (a : α) → ℕ) a_1) ((g : (a : α) → ℕ) a_1) : ℕ)
⊢ Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊔ g)) =
    Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∪ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)

Tactic:
simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]

Premises used: Finsupp.count_toMultiset, Multiset.count_union, Finsupp.sup_apply
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a :
  ∀ (a : α),
    Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
      Multiset.count a ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)
⊢ Eq (α := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g) : Multiset α)
    ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g : Multiset α)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : α →₀ ℕ
a_1 : α
a :
  Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
    min (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f))
      (Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) g))
a₁ : Eq (α := ℕ) ((f ⊓ g : (a : α) → ℕ) a_1 : ℕ) (min ((f : (a : α) → ℕ) a_1) ((g : (a : α) → ℕ) a_1) : ℕ)
⊢ Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) (f ⊓ g)) =
    Multiset.count a_1 ((toMultiset : (a : α →₀ ℕ) → Multiset α) f ∩ (toMultiset : (a : α →₀ ℕ) → Multiset α) g)

Tactic:
simp_rw [Multiset.count_inter, Finsupp.count_toMultiset, Finsupp.inf_apply]

Premises used: Finsupp.inf_apply, Finsupp.count_toMultiset, Multiset.count_inter
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
rw₁ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ i ∈ f.support
rw₂ rw₃ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support

Tactic:
rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finsupp.count_toMultiset, Multiset.count_ne_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
f : α →₀ ℕ
i : α
rw : Multiset.count i ((toMultiset : (a : α →₀ ℕ) → Multiset α) f) ≠ 0 ↔ i ∈ f.support
rw₁ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ i ∈ f.support
rw₂ rw₃ : Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ) ↔ Ne (α := ℕ) ((f : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ Membership.mem (γ := Multiset α) ((toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α) i ↔ i ∈ f.support

Tactic:
classical
  rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finsupp.count_toMultiset, Multiset.count_ne_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ s.toFinset ↔ Ne (α := ℕ) ((fun (a : α) ↦ count a s) a) 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
s : Multiset α
⊢ (fun (f : α →₀ ℕ) ↦ ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α))
      ((fun (s : Multiset α) ↦
          ({ support := s.toFinset, toFun := fun (a : α) ↦ count a s, mem_support_toFun := ⋯ } : α →₀ ℕ))
        s) =
    s

Tactic:
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk,
    Multiset.toFinset_sum_count_nsmul_eq]

Premises used: Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk, Multiset.toFinset_sum_count_nsmul_eq
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
f : α →₀ ℕ
a : α
simp : Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ) → Eq (α := ℕ) (0 : ℕ) ((f : (a : α) → ℕ) a : ℕ)
⊢ Eq (α := ℕ)
    (((fun (s : Multiset α) ↦
              ({ support := s.toFinset, toFun := fun (a : α) ↦ count a s, mem_support_toFun := ⋯ } : α →₀ ℕ))
            ((fun (f : α →₀ ℕ) ↦ ((Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) f : Multiset α)) f) :
          (a : α) → ℕ)
        a :
      ℕ)
    ((f : (a : α) → ℕ) a : ℕ)

Tactic:
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum',
        Multiset.count_singleton, mul_boole, Finsupp.coe_mk, Finsupp.mem_support_iff,
        Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]

Premises used: Finsupp.mem_support_iff, Finsupp.toMultiset_apply, Finsupp.sum, mul_boole, Multiset.count_sum', Multiset.count_nsmul, ite_eq_right_iff, ite_not, Multiset.count_singleton, Finsupp.coe_mk, Finset.sum_ite_eq
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ) → Eq (α := ℕ) (0 : ℕ) ((f : (a : α) → ℕ) a : ℕ)

Tactic:
Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Eq (α := ℕ) ((f : (a : α) → ℕ) a : ℕ) (0 : ℕ) → Eq (α := ℕ) (0 : ℕ) ((f : (a : α) → ℕ) a : ℕ)

Tactic:
exact Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ Finsupp.support (M := ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s) = s.toFinset

Tactic:
rfl

Premises used: Multiset.toFinset, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ (((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ) : (a : α) → ℕ) a = count a s

Tactic:
rfl

Premises used: Multiset.count, Multiset.countP, rfl
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) 0 : α →₀ ℕ) (0 : α →₀ ℕ)

Tactic:
_root_.map_zero _

Premises used: map_zero
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ (toFinsupp : (a : Multiset α) → α →₀ ℕ) (s + t) =
    HAdd.hAdd (α := α →₀ ℕ) (β := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s : α →₀ ℕ)
      ((toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ)

Tactic:
_root_.map_add toFinsupp s t

Premises used: map_add, Multiset.toFinsupp
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
h :
  ∀ (a_1 : α),
    Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
      ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) (Finsupp.single a 1 : α →₀ ℕ)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
h : count a_1 {a} = (Finsupp.single a 1 : (a : α) → ℕ) a_1
h₁ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)
h₂ : Eq (α := ℕ) (if a_1 = a then 1 else 0 : ℕ) (Pi.single (M := fun (j : α) ↦ ℕ) a 1 a_1 : ℕ)
h₃ h₄ : Eq (α := ℕ) (if a_1 = a then 1 else 0) (if a_1 = a then 1 else 0)
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) {a} : α →₀ ℕ) : (a : α) → ℕ) a_1 : ℕ)
    ((Finsupp.single a 1 : (a : α) → ℕ) a_1 : ℕ)

Tactic:
rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]

Premises used: Pi.single_apply, Multiset.toFinsupp_apply, Multiset.count_singleton, Finsupp.single_eq_pi_single
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ (Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s) = s

Tactic:
Multiset.toFinsupp.symm_apply_apply s

Premises used: Multiset.sum, Multiset.foldr, AddEquiv.symm_apply_apply, Finsupp.sum, Multiset.toFinsupp, Finset.sum
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
f : α →₀ ℕ
⊢ (toFinsupp : (a : Multiset α) → α →₀ ℕ) s = f ↔ s = (Finsupp.toMultiset : (a : α →₀ ℕ) → Multiset α) f

Tactic:
Multiset.toFinsupp.apply_eq_iff_symm_apply

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Multiset.toFinsupp, Finset.sum, AddEquiv.apply_eq_iff_symm_apply
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h :
  ∀ (a : α),
    Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∪ t) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊔ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ)
          a :
        ℕ)
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∪ t) : α →₀ ℕ)
    ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊔ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∪ t) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊔ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ)
        a :
      ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h :
  ∀ (a : α),
    Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∩ t) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
      ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊓ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ)
          a :
        ℕ)
⊢ Eq (α := α →₀ ℕ) ((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∩ t) : α →₀ ℕ)
    ((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊓ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ Eq (α := ℕ) ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) (s ∩ t) : α →₀ ℕ) : (a : α) → ℕ) a : ℕ)
    ((((toFinsupp : (a : Multiset α) → α →₀ ℕ) s ⊓ (toFinsupp : (a : Multiset α) → α →₀ ℕ) t : α →₀ ℕ) : (a : α) → ℕ)
        a :
      ℕ)

Tactic:
simp