awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
d : α →₀ ℕ
refine_1 : ∀ (h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1), ∃ (a : α), d = single a 1
refine_2 refine_2₁ : (∃ (a : α), d = single a 1) → Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1

Tactic:
classical
  refine ⟨fun h1 ↦ ?_, ?_⟩
  · have hd0 : d ≠ 0 := (by simp [·] at h1)
    obtain ⟨a, ha⟩ := ne_iff.mp hd0
    obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]
    use a
    ext b
    by_cases hb : b = a
    · rw [hb, single_eq_same, hda]
    · simpa only [single_eq_of_ne hb] using hda' b hb
  · rintro ⟨a, rfl⟩
    rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]
    exact fun _ _ hba ↦ single_eq_of_ne hba

Premises used: Finsupp.single_eq_same, Finsupp.single_eq_of_ne, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
h₁ h₂ : α → M → N
⊢ (f.prod fun (a : α) (b : M) ↦ h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂

Tactic:
Finset.prod_mul_distrib

Premises used: Finset.prod_mul_distrib, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
G : Type u_12
inst : Zero M
inst_1 : CommGroup G
f : α →₀ M
h : α → M → G
⊢ (f.prod fun (a : α) (b : M) ↦ (h a b)⁻¹) = (f.prod h)⁻¹

Tactic:
(map_prod (MonoidHom.id G)⁻¹ _ _).symm

Premises used: Multiset.foldr, Multiset.prod, map_prod, Finset.prod, Inv.inv, MonoidHom.id, Eq.symm, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
G : Type u_12
inst : Zero M
inst_1 : SubtractionCommMonoid G
f : α →₀ M
h₁ h₂ : α → M → G
⊢ (f.sum fun (a : α) (b : M) ↦ h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂

Tactic:
Finset.sum_sub_distrib ..

Premises used: Finsupp.sum, Finset.sum_sub_distrib
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : DecidableEq α
inst_1 : AddZeroClass M
inst_2 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
rw :
  Eq.{u_10 + 1} (α := N) (∏ x ∈ f.support ∪ g.support, h x ((f + g : (a : α) → M) x))
    (∏ x ∈ f.support ∪ g.support, h x ((f : (a : α) → M) x) * h x ((g : (a : α) → M) x))
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
rw [Finsupp.prod_of_support_subset f subset_union_left h h_zero,
    Finsupp.prod_of_support_subset g subset_union_right h h_zero, ←
    Finset.prod_mul_distrib, Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]

Premises used: Finset.prod_mul_distrib, Finsupp.prod_of_support_subset, Finset.subset_union_left, HAdd.hAdd, Finsupp.support_add, Finset.subset_union_right
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : DecidableEq α
inst_1 : AddZeroClass M
inst_2 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
x : α
hx : x ∈ f.support ∪ g.support
⊢ h x ((f + g : (a : α) → M) x) = h x ((f : (a : α) → M) x) * h x ((g : (a : α) → M) x)

Tactic:
apply h_add x hx
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : DecidableEq α
inst_1 : AddZeroClass M
inst_2 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ f.support ∪ g.support, h x ((f + g : (a : α) → M) x))
    (∏ x ∈ f.support ∪ g.support, h x ((f : (a : α) → M) x) * h x ((g : (a : α) → M) x))

Tactic:
exact Finset.prod_congr rfl fun x hx => by apply h_add x hx

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
prod_add_index (fun a _ => h_zero a) fun a _ => h_add a

Premises used: Finsupp.prod_add_index
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a

Premises used: Finsupp.prod_add_index
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : AddCommMonoid N
f g : α →₀ M
h : α → M →+ N
⊢ ((f + g).sum fun (x : α) ↦ (⇑(h x) : (a : M) → N)) =
    HAdd.hAdd (α := N) (f.sum fun (x : α) ↦ (⇑(h x) : (a : M) → N)) (g.sum fun (x : α) ↦ (⇑(h x) : (a : M) → N))

Tactic:
sum_add_index' (fun a => (h a).map_zero) fun a => (h a).map_add

Premises used: AddMonoidHom.map_zero, Finsupp.sum_add_index', AddMonoidHom.map_add
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : CommMonoid N
f g : α →₀ M
h : α → MonoidHom.{u_8, u_10} (Multiplicative M) N
⊢ ((f + g).prod fun (a : α) (b : M) ↦
      (h a : (a : Multiplicative M) → N) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) b : Multiplicative M)) =
    HMul.hMul (α := N)
      (f.prod fun (a : α) (b : M) ↦
        (h a : (a : Multiplicative M) → N) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) b : Multiplicative M))
      (g.prod fun (a : α) (b : M) ↦
        (h a : (a : Multiplicative M) → N) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) b : Multiplicative M))

Tactic:
prod_add_index' (fun a => (h a).map_one) fun a => (h a).map_mul

Premises used: Finsupp.prod_add_index', MonoidHom.map_one, MonoidHom.map_mul
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F : α → M →+ N
h :
  ∀ (x : α) (x_1 : M),
    Eq.{u_10 + 1} (α := N)
      (((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x))
              ((fun (F : α → M →+ N) ↦
                  ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯,
                      map_add' := ⋯ } :
                    (α →₀ M) →+ N))
                F)
              x :
            (a : M) → N)
          x_1 :
        N)
      ((F x : (a : M) → N) x_1 : N)
⊢ (fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x))
      ((fun (F : α → M →+ N) ↦
          ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
            (α →₀ M) →+ N))
        F) =
    F

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F : α → M →+ N
x_1 : α
x_2 : M
⊢ Eq.{u_10 + 1} (α := N)
    (((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x))
            ((fun (F : α → M →+ N) ↦
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯,
                    map_add' := ⋯ } :
                  (α →₀ M) →+ N))
              F)
            x_1 :
          (a : M) → N)
        x_2 :
      N)
    ((F x_1 : (a : M) → N) x_2 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F : (α →₀ M) →+ N
H₁ :
  ∀ (x : α) (x_1 : M),
    Eq.{u_10 + 1} (α := N)
      ((AddMonoidHom.comp
              ((fun (F : α → M →+ N) ↦
                  ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯,
                      map_add' := ⋯ } :
                    (α →₀ M) →+ N))
                ((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x)) F))
              (singleAddHom x) :
            (a : M) → N)
          x_1 :
        N)
      ((F.comp (singleAddHom x) : (a : M) → N) x_1 : N)
⊢ (fun (F : α → M →+ N) ↦
        ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
          (α →₀ M) →+ N))
      ((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x)) F) =
    F

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F : (α →₀ M) →+ N
x_1 : α
x_2 : M
⊢ Eq.{u_10 + 1} (α := N)
    ((AddMonoidHom.comp
            ((fun (F : α → M →+ N) ↦
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯,
                    map_add' := ⋯ } :
                  (α →₀ M) →+ N))
              ((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x)) F))
            (singleAddHom x_1) :
          (a : M) → N)
        x_2 :
      N)
    ((F.comp (singleAddHom x_1) : (a : M) → N) x_2 : N)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G_1 : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F G : α → M →+ N
H₁ :
  ∀ (x : α) (x_1 : M),
    Eq.{u_10 + 1} (α := N)
      ((AddMonoidHom.comp (N := α →₀ M)
              ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑((F + G) x) : (a : M) → N), map_zero' := ⋯,
                  map_add' := ⋯ } :
                (α →₀ M) →+ N)
              (singleAddHom x : M →+ α →₀ M) :
            (a : M) → N)
          x_1 :
        N)
      (((HAdd.hAdd (α := (α →₀ M) →+ N) (β := (α →₀ M) →+ N)
                  ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯,
                      map_add' := ⋯ } :
                    (α →₀ M) →+ N)
                  ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(G x) : (a : M) → N), map_zero' := ⋯,
                      map_add' := ⋯ } :
                    (α →₀ M) →+ N)).comp
              (singleAddHom x) :
            (a : M) → N)
          x_1 :
        N)
⊢ { toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑((F + G) x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } =
    HAdd.hAdd (α := (α →₀ M) →+ N) (β := (α →₀ M) →+ N)
      ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
        (α →₀ M) →+ N)
      ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(G x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
        (α →₀ M) →+ N)

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G_1 : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F G : α → M →+ N
x_1 : α
x_2 : M
⊢ Eq.{u_10 + 1} (α := N)
    ((AddMonoidHom.comp (N := α →₀ M)
            ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑((F + G) x) : (a : M) → N), map_zero' := ⋯,
                map_add' := ⋯ } :
              (α →₀ M) →+ N)
            (singleAddHom x_1 : M →+ α →₀ M) :
          (a : M) → N)
        x_2 :
      N)
    (((HAdd.hAdd (α := (α →₀ M) →+ N) (β := (α →₀ M) →+ N)
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯,
                    map_add' := ⋯ } :
                  (α →₀ M) →+ N)
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(G x) : (a : M) → N), map_zero' := ⋯,
                    map_add' := ⋯ } :
                  (α →₀ M) →+ N)).comp
            (singleAddHom x_1) :
          (a : M) → N)
        x_2 :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : AddCommMonoid N
F : α → M →+ N
f : α →₀ M
⊢ Eq.{u_10 + 1} (α := N)
    ((((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) F : (α →₀ M) →+ N) : (a : α →₀ M) → N) f : N)
    (f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N) : N)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : AddCommMonoid N
F : (α →₀ M) →+ N
x : α
⊢ (AddEquiv.symm liftAddHom : (a : (α →₀ M) →+ N) → α → M →+ N) F x = F.comp (singleAddHom x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : AddCommMonoid N
F : (α →₀ M) →+ N
x : α
y : M
⊢ Eq.{u_10 + 1} (α := N)
    ((((AddEquiv.symm liftAddHom : (a : (α →₀ M) →+ N) → α → M →+ N) F x : M →+ N) : (a : M) → N) y : N)
    ((F : (a : α →₀ M) → N) (single x y) : N)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
⊢ Eq (α := (α →₀ M) →+ α →₀ M)
    ((liftAddHom : (a : α → M →+ α →₀ M) → (α →₀ M) →+ α →₀ M) singleAddHom : (α →₀ M) →+ α →₀ M)
    (AddMonoidHom.id (α →₀ M) : (α →₀ M) →+ α →₀ M)

Tactic:
liftAddHom.toEquiv.apply_eq_iff_eq_symm_apply.2 rfl

Premises used: Iff.mpr, AddEquiv.toEquiv, rfl, Finsupp.liftAddHom, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f : α →₀ M
⊢ f.sum single = f

Tactic:
DFunLike.congr_fun liftAddHom_singleAddHom f

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, Finsupp.liftAddHom_singleAddHom, Finset.sum, Finsupp.single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
⊢ ∑ a : α, single a ((f : (a : α) → M) a) = f

Tactic:
DFunLike.coe_injective ?_

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
refine :
  Eq (α := (a : α) → M)
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)
⊢ ∑ a : α, single a ((f : (a : α) → M) a) = f

Tactic:
refine DFunLike.coe_injective ?_

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
simp_rw simp_rw₁ : Eq (α := (a : α) → M) (⇑(∑ a : α, single a ((f : (a : α) → M) a)) : (a : α) → M) (⇑f : (a : α) → M)
simp_rw₂ :
  Eq (α := (a : α) → M) (∑ i : α, (⇑(single i ((f : (a : α) → M) i) : α →₀ M) : (a : α) → M)) (⇑f : (a : α) → M)
simp_rw₃ : Eq (α := (a : α) → M) (∑ x : α, Pi.single (M := fun (j : α) ↦ M) x ((f : (a : α) → M) x)) (⇑f : (a : α) → M)
⊢ Eq (α := (a : α) → M)
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)

Tactic:
simp_rw [coe_finsetSum, single_eq_pi_single, Finset.univ_sum_single]

Premises used: Finset.univ_sum_single, Finsupp.coe_finsetSum, Finsupp.single_eq_pi_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
refine :
  Eq (α := (a : α) → M)
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)
⊢ ∑ a : α, single a ((f : (a : α) → M) a) = f

Tactic:
classical
  refine DFunLike.coe_injective ?_
  simp_rw [coe_finsetSum, single_eq_pi_single, Finset.univ_sum_single]

Premises used: Finset.univ_sum_single, DFunLike.coe_injective, Finsupp.coe_finsetSum, Finsupp.single_eq_pi_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
rw : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
⊢ ∑ j : α, (single i m : (a : α) → M) j = m

Tactic:
rw [single, coe_mk, Finset.sum_pi_single']

Premises used: Finset.sum_pi_single', Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
classical : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
⊢ ∑ j : α, (single i m : (a : α) → M) j = m

Tactic:
classical rw [single, coe_mk, Finset.sum_pi_single']

Premises used: Finset.sum_pi_single', Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
⊢ (if Membership.mem (γ := Finset α) univ i then m else 0) = m

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
simp_rw : ∑ x : α, Pi.single (M := fun (a : α) ↦ M) x m i = m
⊢ ∑ j : α, (single j m : (a : α) → M) i = m

Tactic:
simp_rw [single, coe_mk]

Premises used: Finsupp.coe_mk, Finsupp.single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
rw : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
⊢ ∑ x : α, Pi.single (M := fun (a : α) ↦ M) x m i = m

Tactic:
rw [Finset.sum_pi_single]

Premises used: Finset.sum_pi_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
classical : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
⊢ ∑ x : α, Pi.single (M := fun (a : α) ↦ M) x m i = m

Tactic:
classical rw [Finset.sum_pi_single]

Premises used: Finset.sum_pi_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
A : Type u_4
B : Type u_5
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
f₁ f₂ : ι
g₁ g₂ : A
F : ι → A → B
H : f₁ ≠ f₂
HF : ∀ (f : ι), F f 0 = 0
⊢ (HAdd.hAdd (α := ι →₀ A) (single f₁ g₁) (single f₂ g₂)).sum F = F f₁ g₁ + F f₂ g₂

Tactic:
simp [sum_of_support_subset _ support_single_add_single_subset, single_apply, H, HF, H.symm]

Premises used: Ne.symm, Finsupp.support_single_add_single_subset, Finsupp.single_apply, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
ι : Type u_2
A : Type u_4
B : Type u_5
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
f₁ f₂ : ι
g₁ g₂ : A
F : ι → A → B
H : f₁ ≠ f₂
HF : ∀ (f : ι), F f 0 = 0
⊢ (HAdd.hAdd (α := ι →₀ A) (single f₁ g₁) (single f₂ g₂)).sum F = F f₁ g₁ + F f₂ g₂

Tactic:
classical
  simp [sum_of_support_subset _ support_single_add_single_subset, single_apply, H, HF, H.symm]

Premises used: Ne.symm, Finsupp.support_single_add_single_subset, Finsupp.single_apply, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α → M
⊢ Eq (α := α →₀ M) ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) f : α →₀ M) (∑ a : α, single a (f a) : α →₀ M)

Tactic:
(univ_sum_single _).symm

Premises used: Finsupp.univ_sum_single, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α → M
⊢ (⇑(∑ a : α, single a (f a)) : (a : α) → M) = f

Tactic:
congrArg _ (equivFunOnFinite_symm_eq_sum f).symm

Premises used: congrArg, Eq.symm, Finsupp.equivFunOnFinite_symm_eq_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α → M
rw : Eq.{u_8 + 1} (α := M) (sum (∑ a : α, single a (f a)) fun (x : α) (n : M) ↦ n) (∑ a : α, f a)
rw₁ : Eq.{u_8 + 1} (α := M) (∑ i : α, (∑ a : α, single a (f a) : (a : α) → M) i) (∑ a : α, f a)
rw₂ rw₃ : Eq.{u_8 + 1} (α := M) (∑ i : α, f i) (∑ a : α, f a)
⊢ Eq.{u_8 + 1} (α := M) (sum ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) f) fun (x : α) (n : M) ↦ n)
    (∑ a : α, f a)

Tactic:
rw [equivFunOnFinite_symm_eq_sum, sum_fintype _ _ fun _ ↦ rfl, coe_univ_sum_single]

Premises used: Finsupp.sum_fintype, Finsupp.coe_univ_sum_single, Finsupp.equivFunOnFinite_symm_eq_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : AddCommMonoid N
f : α → M →+ N
a : α
b : M
⊢ Eq.{u_10 + 1} (α := N)
    ((((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f : (α →₀ M) →+ N) : (a : α →₀ M) → N) (single a b) : N)
    ((f a : (a : M) → N) b : N)

Tactic:
sum_single_index (f a).map_zero

Premises used: Multiset.sum, AddMonoidHom.map_zero, Multiset.foldr, Finsupp.sum_single_index, Finsupp.sum, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddZeroClass M
inst_1 : AddCommMonoid N
f : α → M →+ N
a : α
⊢ AddMonoidHom.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f) (singleAddHom a) = f a

Tactic:
AddMonoidHom.ext fun b => liftAddHom_apply_single f a b

Premises used: AddMonoidHom.ext, Finsupp.liftAddHom_apply_single