awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
⊢ Eq (α := β →₀ M) (embDomain f 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, dite, Multiset.ofList, Finsupp.embDomain, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
simp :
  Eq.{u_4 + 1} (α := M)
    (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
      (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯)
    else 0)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
      (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
    else 0)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) b : M)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
        (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
      else 0 :
      M)

Tactic:
simp only [embDomain, mem_map, mem_support_iff, coe_mk]

Premises used: Finsupp.mem_support_iff, Finsupp.embDomain, Finset.mem_map, Finsupp.coe_mk
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
pos :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b)
    (h_1 : ∃ (a : α), (f : (a : α) → β) a = b),
    Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M)
      ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
neg :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b),
    (¬∃ (a : α), (f : (a : α) → β) a = b) →
      Eq.{u_4 + 1} (α := M)
        ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M) (0 : M)
pos₁ :
  (¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b) →
    ∀ (h : ∃ (a : α), (f : (a : α) → β) a = b),
      Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
neg₁ :
  (¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b) →
    (¬∃ (a : α), (f : (a : α) → β) a = b) → Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M)
    (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
      (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯)
    else 0)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
      (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
    else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b
h_1 : ∃ (a : α), (f : (a : α) → β) a = b
⊢ Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M)
    ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b
h_1 : ¬∃ (a : α), (f : (a : α) → β) a = b
⊢ Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M)
    (0 : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
h : ¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b
h_1 : ∃ (a : α), (f : (a : α) → β) a = b
⊢ Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
h : ¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b
h_1 : ¬∃ (a : α), (f : (a : α) → β) a = b
⊢ Eq.{u_4 + 1} (α := M) 0 0

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
simp_rw :
  Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)

Tactic:
simp_rw [embDomain, coe_mk, mem_map']

Premises used: Finsupp.embDomain, Finset.mem_map', Finsupp.coe_mk
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
pos :
  ∀ (h : a ∈ v.support),
    Eq.{u_4 + 1} (α := M)
      ((v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯) :
        M)
      ((v : (a : α) → M) a : M)
neg : ∀ (h : a ∉ v.support), Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∈ v.support
⊢ Eq.{u_4 + 1} (α := M)
    ((v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
          ⋯) :
      M)
    ((v : (a : α) → M) a : M)

Tactic:
congr_arg (v : α → M) (f.inj' ?_)

Premises used: Function.Embedding.inj', congr_arg, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∈ v.support
pos :
  f.toFun
      (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support ⋯) =
    f.toFun a
⊢ Eq.{u_4 + 1} (α := M)
    ((v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
          ⋯) :
      M)
    ((v : (a : α) → M) a : M)

Tactic:
refine congr_arg (v : α → M) (f.inj' ?_)

Premises used: Function.Embedding.inj', congr_arg, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∈ v.support
⊢ f.toFun
      (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support ⋯) =
    f.toFun a

Tactic:
Finset.choose_property (fun a₁ => f a₁ = f a) _ _

Premises used: Finset.choose_property, Eq, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∈ v.support
⊢ f.toFun
      (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support ⋯) =
    f.toFun a

Tactic:
exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _

Premises used: Finset.choose_property, Eq, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∉ v.support
⊢ Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) a : M)

Tactic:
(notMem_support_iff.1 h).symm

Premises used: Finsupp.notMem_support_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∉ v.support
⊢ Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) a : M)

Tactic:
exact (notMem_support_iff.1 h).symm

Premises used: Finsupp.notMem_support_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
simp_rw :
  Eq.{u_4 + 1} (α := M)
    (({ support := map f v.support,
            toFun := fun (a₂ : β) ↦
              if h : a₂ ∈ map f v.support then
                (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
              else 0,
            mem_support_toFun := ⋯ } :
          (a : β) → M)
        ((f : (a : α) → β) a : β) :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M)
    (if h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β) then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
pos :
  ∀ (h : a ∈ v.support),
    Eq.{u_4 + 1} (α := M)
      ((v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯) :
        M)
      ((v : (a : α) → M) a : M)
neg neg₁ : ∀ (h : a ∉ v.support), Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)

Tactic:
classical
    simp_rw [embDomain, coe_mk, mem_map']
    split_ifs with h
    · refine congr_arg (v : α → M) (f.inj' ?_)
      exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
    · exact (notMem_support_iff.1 h).symm

Premises used: Function.Embedding.inj', congr_arg, Finsupp.embDomain, Finset.mem_map', Finsupp.coe_mk, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) (0 : M)

Tactic:
grind [embDomain]

Premises used: Finsupp.embDomain
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
l₁ l₂ : α →₀ M
h : embDomain f l₁ = embDomain f l₂
a : α
⊢ Eq.{u_4 + 1} (α := M) ((l₁ : (a : α) → M) a : M) ((l₂ : (a : α) → M) a : M)

Tactic:
simpa only [embDomain_apply_self] using DFunLike.ext_iff.1 h (f a)

Premises used: DFunLike.ext_iff, Finsupp.embDomain_apply_self, Iff.mp, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
l₁ l₂ : α →₀ M
⊢ embDomain f l₁ = embDomain f l₂ ↔ l₁ = l₂

Tactic:
(embDomain_injective f).eq_iff

Premises used: Finsupp.embDomain_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
l : α →₀ M
⊢ embDomain f l = 0 ↔ l = 0

Tactic:
(embDomain_injective f).eq_iff' <| embDomain_zero f

Premises used: Finsupp.embDomain_injective, Function.Injective.eq_iff', Finsupp.embDomain_zero
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
⊢ embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
h :
  ∀ (x : α →₀ M) (a : α),
    Eq.{u_4 + 1} (α := M) ((embDomain (Embedding.refl α) x : (a : α) → M) a : M) ((id x : (a : α) → M) a : M)
⊢ Eq (α := (v : α →₀ M) → α →₀ M) (embDomain (Embedding.refl α)) id

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
x : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((embDomain (Embedding.refl α) x : (a : α) → M) a : M) ((id x : (a : α) → M) a : M)

Tactic:
simp [embDomain_apply]

Premises used: Finsupp.embDomain_apply
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H_1 : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f ((g₁ : (a : α) → M) a) ((g₂ : (a : α) → N) a) ≠ 0
⊢ a ∈ g₁.support ∪ g₂.support

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H_1 : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f ((g₁ : (a : α) → M) a) ((g₂ : (a : α) → N) a) ≠ 0
⊢ a ∈ g₁.support ∪ g₂.support

Tactic:
classical
      grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
⊢ (zipWith f hf g₁ g₂ : (a : α) → O) a = f ((g₁ : (a : α) → M) a) ((g₂ : (a : α) → N) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
D : DecidableEq α
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ support.{u_1, u_6} (M := O)
      (onFinset (g₁.support ∪ g₂.support) (fun (a : α) ↦ f ((g₁ : (a : α) → M) a) ((g₂ : (a : α) → N) a)) ⋯) ⊆
    g₁.support ∪ g₂.support

Tactic:
support_onFinset_subset

Premises used: Finsupp.support_onFinset_subset
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
D : DecidableEq α
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Tactic:
convert! support_onFinset_subset

Premises used: Finsupp.support_onFinset_subset
-- Module: Mathlib.Data.Finsupp.Encodable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Countable β
inst_2 : Zero β
⊢ Countable (α →₀ β)

Tactic:
.of_equiv _ finsuppEquivDFinsupp.symm

Premises used: Countable.of_equiv, finsuppEquivDFinsupp, Equiv.symm
-- Module: Mathlib.Data.Finsupp.Encodable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Countable β
inst_2 : Zero β
⊢ Countable (α →₀ β)

Tactic:
exact .of_equiv _ finsuppEquivDFinsupp.symm
-- Module: Mathlib.Data.Finsupp.Encodable
Goal:
α : Type u_1
β : Type u_2
inst : Countable α
inst_1 : Countable β
inst_2 : Zero β
⊢ Countable (α →₀ β)

Tactic:
classical exact .of_equiv _ finsuppEquivDFinsupp.symm
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
⊢ Eq (α := AddSubmonoid (α →₀ M)) (AddSubmonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = single a b}) ⊤

Tactic:
top_unique fun x _hx =>
    Finsupp.induction x (AddSubmonoid.zero_mem _) fun a b _f _ha _hb hf =>
      AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure <| ⟨a, b, rfl⟩) hf

Premises used: top_unique, Finsupp.induction
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : AddZeroClass N
f g : (α →₀ M) →+ N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N) ((f : (a : α →₀ M) → N) (single x y) : N) ((g : (a : α →₀ M) → N) (single x y) : N)
⊢ f = g

Tactic:
AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_

Premises used: AddMonoidHom.eq_of_eqOn_denseM, Finsupp.add_closure_setOf_eq_single
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : AddZeroClass N
f g : (α →₀ M) →+ N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N) ((f : (a : α →₀ M) → N) (single x y) : N) ((g : (a : α →₀ M) → N) (single x y) : N)
refine :
  Set.EqOn (α := α →₀ M) (β := N) (⇑f : (a : α →₀ M) → N) (⇑g : (a : α →₀ M) → N)
    {f : α →₀ M | ∃ (a : α) (b : M), f = single a b}
⊢ f = g

Tactic:
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_

Premises used: AddMonoidHom.eq_of_eqOn_denseM, Finsupp.add_closure_setOf_eq_single
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : AddZeroClass N
f g : (α →₀ M) →+ N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N) ((f : (a : α →₀ M) → N) (single x y) : N) ((g : (a : α →₀ M) → N) (single x y) : N)
x : α
y : M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : α →₀ M) → N) (single x y) : N) ((g : (a : α →₀ M) → N) (single x y) : N)

Tactic:
apply H
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α), f.comp (singleAddHom x) = g.comp (singleAddHom x)
⊢ f = g

Tactic:
addHom_ext fun x => DFunLike.congr_fun (H x)

Premises used: DFunLike.congr_fun, Finsupp.addHom_ext
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
⊢ Eq (α := (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
      (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
      (α →₀ M) →+ Additive N)

Tactic:
have := addHom_ext (f := f.toAdditiveRight) (g := g.toAdditiveRight) H
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
this :
  Eq (α := (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
      (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
      (α →₀ M) →+ Additive N)
h :
  ∀ (x : α) (x_1 : M),
    Eq.{u_3 + 1} (α := N)
      ((Additive.toMul : (a : Additive N) → N)
          ((AddMonoidHom.comp
                  ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                  (singleAddHom x) :
                (a : M) → Additive N)
              x_1 :
            Additive N) :
        N)
      ((Additive.toMul : (a : Additive N) → N)
          ((AddMonoidHom.comp
                  ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                  (singleAddHom x) :
                (a : M) → Additive N)
              x_1 :
            Additive N) :
        N)
⊢ f = g

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
this :
  Eq (α := (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
      (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
      (α →₀ M) →+ Additive N)
x : α
x_1 : M
h :
  ∀
    (this :
      ∀ (x : α →₀ M),
        Eq.{u_3 + 1} (α := Additive N)
          ((((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
                  (α →₀ M) →+ Additive N) :
                (a : α →₀ M) → Additive N)
              x :
            Additive N)
          ((((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
                  (α →₀ M) →+ Additive N) :
                (a : α →₀ M) → Additive N)
              x :
            Additive N))
    (x : α) (x_2 : M),
    Eq.{u_3 + 1} (α := N)
      ((Additive.toMul : (a : Additive N) → N)
          ((AddMonoidHom.comp
                  ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                  (singleAddHom x) :
                (a : M) → Additive N)
              x_2 :
            Additive N) :
        N)
      ((Additive.toMul : (a : Additive N) → N)
          ((AddMonoidHom.comp
                  ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                  (singleAddHom x) :
                (a : M) → Additive N)
              x_2 :
            Additive N) :
        N)
⊢ Eq.{u_3 + 1} (α := N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)

Tactic:
rw [DFunLike.ext_iff] at this

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
this :
  ∀ (x : α →₀ M),
    Eq.{u_3 + 1} (α := Additive N)
      ((((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
              (α →₀ M) →+ Additive N) :
            (a : α →₀ M) → Additive N)
          x :
        Additive N)
      ((((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
              (α →₀ M) →+ Additive N) :
            (a : α →₀ M) → Additive N)
          x :
        Additive N)
x : α
x_1 : M
⊢ Eq.{u_3 + 1} (α := N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)

Tactic:
apply this