awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
δ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
inst_2 : (i : ι) → SMulZeroClass.{u_1, v} δ (β i)
inst_3 : SMul γ δ
inst_4 : ∀ (i : ι), IsScalarTower.{w, u_1, v} γ δ (β i)
r : γ
s : δ
m : Π₀ (i : ι), β i
i : ι
⊢ ((r • s) • m : (a : ι) → β a) i = (r • s • m : (a : ι) → β a) i

Tactic:
simp only [smul_apply, smul_assoc r s (m i)]

Premises used: smul_assoc, DFinsupp.smul_apply, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γᵐᵒᵖ (β i)
inst_3 : ∀ (i : ι), IsCentralScalar.{w, v} γ (β i)
r : γ
m : Π₀ (i : ι), β i
i : ι
⊢ (MulOpposite.op r • m : (a : ι) → β a) i = (r • m : (a : ι) → β a) i

Tactic:
simp only [smul_apply, op_smul_eq_smul r (m i)]

Premises used: DFinsupp.smul_apply, DFunLike.coe, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : Semiring γ
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → Module.{w, v} γ (β i)
c x : γ
y : Π₀ (i : ι), β i
i : ι
⊢ ((c + x) • y : (a : ι) → β a) i = (c • y + x • y : (a : ι) → β a) i

Tactic:
simp only [add_apply, smul_apply, add_smul]

Premises used: DFinsupp.smul_apply, add_smul, DFinsupp.add_apply
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : Semiring γ
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → Module.{w, v} γ (β i)
c : Π₀ (i : ι), β i
i : ι
⊢ (HSMul.hSMul (α := γ) 0 c : (a : ι) → β a) i = (0 : (a : ι) → β a) i

Tactic:
simp only [smul_apply, zero_smul, zero_apply]

Premises used: DFinsupp.zero_apply, DFinsupp.smul_apply, zero_smul
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : Semiring γ
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → Module.{w, v} γ (β i)
v : Π₀ (i : ι), β i
⊢ (coeFnLinearMap γ (β := β) : (a : Π₀ (i : ι), β i) → (i : ι) → β i) v = (⇑v : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
p : ι → Prop
inst_2 : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
h : ∀ (i : ι), (filter (β := β) p (r • f) : (a : ι) → β a) i = (r • filter (β := β) p f : (a : ι) → β a) i
⊢ filter (β := β) p (r • f) = r • filter (β := β) p f

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
p : ι → Prop
inst_2 : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
i : ι
⊢ (filter (β := β) p (r • f) : (a : ι) → β a) i = (r • filter (β := β) p f : (a : ι) → β a) i

Tactic:
simp [smul_apply, smul_ite]

Premises used: DFinsupp.smul_apply, smul_ite
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
p : ι → Prop
inst_2 : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
⊢ subtypeDomain (β := β) p (r • f) = r • subtypeDomain (β := β) p f

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
simp :
  (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)
⊢ (mk (β := β) s (c • x) : (a : ι) → β a) i = (HSMul.hSMul (β := Π₀ (i : ι), β i) c (mk (β := β) s x) : (a : ι) → β a) i

Tactic:
simp only [smul_apply, mk_apply]

Premises used: DFinsupp.smul_apply, DFinsupp.mk_apply
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSMul.hSMul (β := β i) c
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
neg : i ∉ s → 0 = HSMul.hSMul (β := β i) c 0
⊢ (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∈ s
⊢ (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
    HSMul.hSMul (β := β i) c
      (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
        β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
h : i ∉ s
neg neg₁ : Eq.{v + 1} (α := β i) 0 0
⊢ 0 = HSMul.hSMul (β := β i) c 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
s : Finset ι
c : γ
x : (i : (↑(↑s : Set ι) : Type u)) → β (↑i : ι)
i : ι
pos :
  ∀ (h : i ∈ s),
    (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSMul.hSMul (β := β i) c
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
neg : i ∉ s → 0 = HSMul.hSMul (β := β i) c 0
pos₁ :
  ∀ (h : i ∈ s),
    (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) =
      HSMul.hSMul (β := β i) c
        (x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) :
          β (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) : ι))
neg₁ : i ∉ s → 0 = HSMul.hSMul (β := β i) c 0
⊢ (if H : i ∈ s then (c • x) (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0) =
    HSMul.hSMul (β := β i) c (if H : i ∈ s then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i H) else 0)

Tactic:
split_ifs <;> [rfl; rw [smul_zero]]

Premises used: smul_zero
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
simp :
  (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ else 0) =
    HSMul.hSMul (β := β i) c (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ else 0)
⊢ (single (β := β) i_1 (c • x) : (a : ι) → β a) i =
    (HSMul.hSMul (β := Π₀ (i : ι), β i) c (single (β := β) i_1 x) : (a : ι) → β a) i

Tactic:
simp only [smul_apply, single_apply]

Premises used: DFinsupp.smul_apply, DFinsupp.single_apply
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
pos :
  ∀ (h : i_1 = i),
    Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ =
      HSMul.hSMul (β := β i) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ : β i)
neg : ∀ (h : ¬i_1 = i), 0 = HSMul.hSMul (β := β i) c 0
⊢ (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ else 0) =
    HSMul.hSMul (β := β i) c (if h : i_1 = i then Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
h : i_1 = i
pos :
  Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ =
    HSMul.hSMul (β := β i_1) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ : β i_1)
⊢ Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) (c • x) ⋯ =
    HSMul.hSMul (β := β i) c (Eq.rec (motive := fun (x : ι) (x_1 : i_1 = x) ↦ β x) x ⋯ : β i)

Tactic:
cases h
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i : ι
c : γ
x : β i
⊢ Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ β x) (c • x) ⋯ =
    HSMul.hSMul (β := β i) c (Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ β x) x ⋯ : β i)

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
i_1 : ι
c : γ
x : β i_1
i : ι
h : ¬i_1 = i
neg neg₁ : Eq.{v + 1} (α := β i) 0 0
⊢ 0 = HSMul.hSMul (β := β i) c 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
γ : Type w
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
b : γ
v : Π₀ (i : ι), β i
⊢ (b • v).support (β := β) ⊆ v.support (β := β)

Tactic:
support_mapRange

Premises used: Set.Mem, setOf, DFinsupp.support_mapRange
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
h₁ :
  ∀ (i : κ),
    (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
⊢ comapDomain (β := β) h hh (r • f) = r • comapDomain (β := β) h hh f

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ : (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
h₃ : HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
h₄ h₅ :
  HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i))
⊢ (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i

Tactic:
rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]

Premises used: DFinsupp.smul_apply, DFinsupp.comapDomain_apply
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
h₁ :
  ∀ (i : κ),
    (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
      (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
⊢ comapDomain' (β := β) h hh' (r • f) = r • comapDomain' (β := β) h hh' f

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
h₃ :
  HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
h₄ h₅ :
  HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i))
⊢ (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i

Tactic:
rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]

Premises used: DFinsupp.smul_apply, DFinsupp.comapDomain'_apply
-- Module: Mathlib.Data.DFinsupp.Module
Goal:
ι : Type u
γ : Type w
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
inst_1 : (i : Option ι) → SMulZeroClass.{w, v} γ (α i)
r : γ
f : Π₀ (i : Option ι), α i
⊢ (equivProdDFinsupp (α := α) : (a : Π₀ (i : Option ι), α i) → α none × Π₀ (i : ι), α (some i)) (r • f) =
    HSMul.hSMul (β := α none × Π₀ (i : ι), α (some i)) r
      ((equivProdDFinsupp (α := α) : (a : Π₀ (i : Option ι), α i) → α none × Π₀ (i : ι), α (some i)) f :
        α none × Π₀ (i : ι), α (some i))

Tactic:
Prod.ext (smul_apply _ _ _) (comapDomain_smul _ (Option.some_injective _) _ _)

Premises used: DFinsupp.smul_apply, DFinsupp.comapDomain_smul, Prod.ext, Option.some_injective
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ (toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) (single (β := fun (x : α) ↦ ℕ) a n) = Multiset.replicate n a

Tactic:
DFinsupp.sumAddHom_single _ _ _

Premises used: DFinsupp.sumAddHom_single, Multiset.ofList, Multiset.replicate
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ) : (a : α) → ℕ) a = count a s

Tactic:
rfl

Premises used: Multiset.count, Multiset.countP, rfl
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ DFinsupp.support (β := fun (x : α) ↦ ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) = s.toFinset

Tactic:
Finset.filter_true_of_mem fun _ hx ↦ count_ne_zero.mpr <| Multiset.mem_toFinset.1 hx

Premises used: Iff.mpr, DFinsupp.support, Multiset.count_ne_zero, Finset.filter_true_of_mem, Iff.mp, Finset.filter, Multiset.mem_toFinset, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
h :
  ∀ (i : α),
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate n a) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
      (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate n a) : Π₀ (x : α), ℕ)
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : Π₀ (i : α), ℕ)

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
i : α
h : count i (replicate n a) = (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i
⊢ (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate n a) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i

Tactic:
dsimp [toDFinsupp]

Premises used: Multiset.toDFinsupp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i

Tactic:
simp [count_replicate]

Premises used: Multiset.count_replicate
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
a : α
rw :
  Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate 1 a) : Π₀ (x : α), ℕ)
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1 : Π₀ (i : α), ℕ)
rw₁ rw₂ :
  Eq (α := Π₀ (x : α), ℕ) (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1) (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1)
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) {a})
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1)

Tactic:
rw [← replicate_one, toDFinsupp_replicate]

Premises used: Multiset.toDFinsupp_replicate, Multiset.replicate_one
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h :
  ∀ (x a : α),
    count a ((AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp : (a : Multiset α) → Multiset α) {x}) =
      count a ((AddMonoidHom.id (Multiset α) : (a : Multiset α) → Multiset α) {x})
⊢ Eq.{u_1 + 1} (α := Multiset α →+ Multiset α) (AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp)
    (AddMonoidHom.id (Multiset α))

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
x a : α
⊢ count a ((AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp : (a : Multiset α) → Multiset α) {x}) =
    count a ((AddMonoidHom.id (Multiset α) : (a : Multiset α) → Multiset α) {x})

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
H :
  ∀ (x i : α),
    (((AddMonoidHom.comp (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset)
                  (DFinsupp.singleAddHom (fun (i : α) ↦ ℕ) x) :
                (a : ℕ) → Π₀ (x : α), ℕ)
              1 :
            Π₀ (x : α), ℕ) :
          (a : α) → ℕ)
        i =
      ((((AddMonoidHom.comp (AddMonoidHom.id (Π₀ (x : α), ℕ)) (DFinsupp.singleAddHom (fun (i : α) ↦ ℕ) x) :
                  ℕ →+ Π₀ (x : α), ℕ) :
                (a : ℕ) → Π₀ (x : α), ℕ)
              1 :
            Π₀ (x : α), ℕ) :
          (a : α) → ℕ)
        i
⊢ Eq.{u_1 + 1} (α := (Π₀ (x : α), ℕ) →+ Π₀ (x : α), ℕ) (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset)
    (AddMonoidHom.id (Π₀ (x : α), ℕ))

Tactic:
ext
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
x i : α
⊢ (((AddMonoidHom.comp (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset) (DFinsupp.singleAddHom (fun (i : α) ↦ ℕ) x) :
              (a : ℕ) → Π₀ (x : α), ℕ)
            1 :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i =
    ((((AddMonoidHom.comp (AddMonoidHom.id (Π₀ (x : α), ℕ)) (DFinsupp.singleAddHom (fun (i : α) ↦ ℕ) x) :
                ℕ →+ Π₀ (x : α), ℕ) :
              (a : ℕ) → Π₀ (x : α), ℕ)
            1 :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
⊢ (DFinsupp.toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s) = s

Tactic:
equivDFinsupp.symm_apply_apply s

Premises used: Multiset.sum, Multiset.foldr, AddEquiv.symm_apply_apply, Multiset.equivDFinsupp, Finset.sum, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Multiset α) (β := Π₀ (x : α), ℕ) (⇑toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ)

Tactic:
equivDFinsupp.injective

Premises used: AddEquiv.injective, Multiset.equivDFinsupp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ)
      ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) ↔
    s = t

Tactic:
toDFinsupp_injective.eq_iff

Premises used: Function.Injective.eq_iff, Multiset.toDFinsupp_injective
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ LE.le (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ)
      ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) ↔
    s ≤ t

Tactic:
simp [Multiset.le_iff_count, DFinsupp.le_def]

Premises used: Multiset.le_iff_count, DFinsupp.le_def
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ LT.lt (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s : Π₀ (x : α), ℕ)
      ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t : Π₀ (x : α), ℕ) ↔
    s < t

Tactic:
lt_iff_lt_of_le_iff_le' toDFinsupp_le_toDFinsupp toDFinsupp_le_toDFinsupp

Premises used: lt_iff_lt_of_le_iff_le', Multiset.toDFinsupp_le_toDFinsupp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h :
  ∀ (i : α),
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∩ t) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
      (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊓ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
            Π₀ (x : α), ℕ) :
          (a : α) → ℕ)
        i
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∩ t) : Π₀ (x : α), ℕ)
    ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊓ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
      Π₀ (x : α), ℕ)

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
i : α
⊢ (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∩ t) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊓ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h :
  ∀ (i : α),
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∪ t) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
      (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊔ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
            Π₀ (x : α), ℕ) :
          (a : α) → ℕ)
        i
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∪ t) : Π₀ (x : α), ℕ)
    ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊔ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
      Π₀ (x : α), ℕ)

Tactic:
ext i
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
i : α
⊢ (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∪ t) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊔ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i

Tactic:
simp
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f : Π₀ (x : α), ℕ
⊢ (Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f) = f

Tactic:
Multiset.equivDFinsupp.apply_symm_apply f

Premises used: AddEquiv.apply_symm_apply, Multiset.equivDFinsupp, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Π₀ (x : α), ℕ) (β := Multiset α) (⇑toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α)

Tactic:
Multiset.equivDFinsupp.symm.injective

Premises used: AddEquiv.injective, Multiset.equivDFinsupp, AddEquiv.symm, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Eq (α := Multiset α) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f : Multiset α)
      ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g : Multiset α) ↔
    f = g

Tactic:
toMultiset_injective.eq_iff

Premises used: Function.Injective.eq_iff, DFinsupp.toMultiset_injective
-- Module: Mathlib.Data.DFinsupp.Multiset
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
simp_rw :
  LE.le (α := Π₀ (x : α), ℕ)
      ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f) :
        Π₀ (x : α), ℕ)
      ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g) :
        Π₀ (x : α), ℕ) ↔
    f ≤ g
⊢ LE.le (α := Multiset α) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f : Multiset α)
      ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g : Multiset α) ↔
    f ≤ g

Tactic:
simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]

Premises used: DFinsupp.toMultiset_toDFinsupp, Multiset.toDFinsupp_le_toDFinsupp