awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ HAdd.hAdd (α := M) (β := M) ((x : (a : α) → M) a : M) (0 : M) = (x : (a : α) → M) a

Tactic:
add_zero (x a)

Premises used: add_zero, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
h : Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0
⊢ HAdd.hAdd (α := M) (β := M) ((x : (a : α) → M) a : M)
      (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M) =
    (x : (a : α) → M) a

Tactic:
convert! add_zero (x a)

Premises used: add_zero, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0

Tactic:
Finset.sum_eq_zero fun i hi => if_neg ?_

Premises used: Finset.sum_eq_zero, if_neg
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
h : ∀ (i : α) (hi : i ∈ x.support.erase a), ¬f i = f a
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0

Tactic:
refine Finset.sum_eq_zero fun i hi => if_neg ?_

Premises used: Finset.sum_eq_zero, if_neg
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
⊢ ¬f i = f a

Tactic:
(hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)

Premises used: Finset.ne_of_mem_erase, Finset.mem_of_mem_erase, Set.InjOn.ne, Set.InjOn.mono
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
i : α
hi : i ∈ x.support.erase a
⊢ ¬f i = f a

Tactic:
exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)

Premises used: Finset.ne_of_mem_erase, Finset.mem_of_mem_erase, Set.InjOn.ne, Set.InjOn.mono
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
neg : Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)

Tactic:
rw [notMem_support_iff.1 hax]

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0

Tactic:
Finset.sum_eq_zero fun i hi => if_neg ?_

Premises used: Finset.sum_eq_zero, if_neg
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
neg : ∀ (i : α) (hi : i ∈ x.support), ¬f i = f a
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0

Tactic:
refine Finset.sum_eq_zero fun i hi => if_neg ?_

Premises used: Finset.sum_eq_zero, if_neg
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
i : α
hi : i ∈ x.support
⊢ ¬f i = f a

Tactic:
hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

Premises used: ne_of_mem_of_not_mem, Set.InjOn.ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
i : α
hi : i ∈ x.support
⊢ ¬f i = f a

Tactic:
exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

Premises used: ne_of_mem_of_not_mem, Set.InjOn.ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₁ : Eq (α := M) (x.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₂ rw₃ rw₄ :
  Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
    ((x : (a : α) → M) a : M)
rw₅ :
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
pos :
  ∀ (hax : a ∈ x.support),
    Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
      ((x : (a : α) → M) a : M)
neg neg₁ :
  ∀ (hax : a ∉ x.support),
    Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
      ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)

Tactic:
classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

Premises used: Finsupp.mapDomain, Finset.sum_eq_zero, Finsupp.sum, Finsupp.support, if_pos, Finsupp.single_apply, Finsupp.sum_apply, add_zero, if_neg, DFunLike.coe, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
x : β
hx : x ∈ image f s.support
⊢ ∃ (a : α), ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) a : M) (0 : M) ∧ f a = x

Tactic:
simp only [mem_image, mem_support_iff, Ne] at hx

Premises used: Finsupp.mem_support_iff, Finset.mem_image, Ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
x : β
hx : ∃ (a : α), ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) a : M) (0 : M) ∧ f a = x
rcases :
  ∀ (hx_w : α) (hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)),
    f hx_w ∈ (mapDomain f s).support
⊢ x ∈ (mapDomain f s).support

Tactic:
rcases hx with ⟨hx_w, hx_h_left, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
simp : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : β) → M) (f hx_w) : M) (0 : M)
⊢ f hx_w ∈ (mapDomain f s).support

Tactic:
simp only [mem_support_iff, Ne]

Premises used: Finsupp.mem_support_iff, Ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left rw : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
rw₁ : hx_w ∈ (↑s.support : Set α)
rw₂ : (↑s.support : Set α) ⊆ (↑s.support : Set α)
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : β) → M) (f hx_w) : M) (0 : M)

Tactic:
rw [mapDomain_apply' (↑s.support : Set _) _ _ hf]

Premises used: Finsupp.mapDomain_apply'
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)

Tactic:
hx_h_left
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)

Tactic:
exact hx_h_left
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left simp_rw : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ hx_w ∈ (↑s.support : Set α)

Tactic:
simp_rw [mem_coe, mem_support_iff, Ne]

Premises used: Finsupp.mem_support_iff, Ne, Finset.mem_coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ (↑s.support : Set α) ⊆ (↑s.support : Set α)

Tactic:
Subset.refl _

Premises used: Finset.Subset.refl, Set.Subset
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ (↑s.support : Set α) ⊆ (↑s.support : Set α)

Tactic:
exact Subset.refl _

Premises used: Finset.Subset.refl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
hf : Injective f
s : α →₀ M
⊢ (mapDomain f s).support = image f s.support

Tactic:
mapDomain_support_of_injOn s hf.injOn

Premises used: Finsupp.mapDomain_support_of_injOn, Function.Injective.injOn
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
h_zero : ∀ (b : β), h b 0 = 1
h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂
⊢ (mapDomain f s).prod h = s.prod fun (a : α) (m : M) ↦ h (f a) m

Tactic:
(prod_sum_index h_zero h_add).trans <| prod_congr fun _ _ => prod_single_index (h_zero _)

Premises used: Finsupp.prod_congr, Finsupp.mapDomain, Finsupp.prod_sum_index, Finsupp.prod_single_index, Eq.trans
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : α → β
s : α →₀ M
h : β → M →+ N
⊢ Eq.{u_6 + 1} (α := N) ((mapDomain f s).sum fun (b : β) (m : M) ↦ (h b : (a : M) → N) m)
    (s.sum fun (a : α) (m : M) ↦ (h (f a) : (a : M) → N) m)

Tactic:
sum_mapDomain_index (fun b => (h b).map_zero) (fun b _ _ => (h b).map_add _ _)

Premises used: AddMonoidHom.map_zero, Finsupp.sum_mapDomain_index, AddMonoidHom.map_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
v : α →₀ M
h :
  ∀ (a : β),
    Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
⊢ embDomain f v = mapDomain (⇑f : (a : α) → β) v

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
pos :
  ∀ (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a),
    Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
neg :
  ∀ (h : a ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
    Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)

Tactic:
by_cases h : a ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
pos :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
      ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)

Tactic:
rcases h with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : α
pos : Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
pos₁ pos₂ : Eq.{u_5 + 1} (α := M) ((v : (a : α) → M) a : M) ((v : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) ((f : (a : α) → β) a : β) : M)

Tactic:
rw [mapDomain_apply f.injective, embDomain_apply_self]

Premises used: Finsupp.mapDomain_apply, Finsupp.embDomain_apply_self, Function.Embedding.injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h neg neg₁ : a ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)

Tactic:
rw [mapDomain_notin_range, embDomain_notin_range]

Premises used: Finsupp.embDomain_notin_range, Finsupp.mapDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ a ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)

Tactic:
assumption
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
rw :
  prod (mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) s) h =
    s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
rw₁ :
  (embDomain { toFun := f, inj' := hf : α ↪ β } s).prod h =
    s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
rw₂ rw₃ :
  Eq.{u_6 + 1} (α := N) (s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b)
    (s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b)
⊢ (mapDomain f s).prod h = s.prod fun (a : α) (b : M) ↦ h (f a) b

Tactic:
rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]

Premises used: Finsupp.prod_embDomain, Finsupp.embDomain_eq_mapDomain, Function.Embedding.coeFn_mk
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ v₁ = v₂

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
rw rw₁ : Eq.{u_5 + 1} (α := M) ((mapDomain f v₂ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)

Tactic:
rw [eq]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)

Tactic:
have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
h :
  ∀ (this : Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)),
    Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
h₁ h₂ h₃ h₄ :
  ∀ (this : Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)),
    Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)

Tactic:
rwa [mapDomain_apply hf, mapDomain_apply hf] at this

Premises used: Finsupp.mapDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
h : mapDomain f (mapDomain (surjInv hf) x) = x
⊢ ∃ (a : α →₀ M), mapDomain f a = x

Tactic:
use mapDomain (surjInv hf) x

Premises used: Finsupp.mapDomain, Function.surjInv
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
h : mapDomain (f ∘ surjInv hf) x = x
h₁ : mapDomain id x = x
h₂ h₃ : x = x
⊢ mapDomain f (mapDomain (surjInv hf) x) = x

Tactic:
rw [← mapDomain_comp, (rightInverse_surjInv hf).id, mapDomain_id]

Premises used: Function.RightInverse.id, Finsupp.mapDomain_id, Function.rightInverse_surjInv, Finsupp.mapDomain_comp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : α → β
g : M →+ N
H :
  ∀ (x : α) (x_1 : M) (a : β),
    Eq.{u_6 + 1} (α := N)
      (((((AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)).comp (singleAddHom x) : (a : M) → β →₀ N) x_1 :
              β →₀ N) :
            (a : β) → N)
          a :
        N)
      (((((AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)).comp (singleAddHom x) : (a : M) → β →₀ N) x_1 :
              β →₀ N) :
            (a : β) → N)
          a :
        N)
⊢ AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g) =
    AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
a : β
⊢ Eq.{u_6 + 1} (α := N)
    (((((AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)).comp (singleAddHom x) : (a : M) → β →₀ N) x_1 :
            β →₀ N) :
          (a : β) → N)
        a :
      N)
    (((((AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)).comp (singleAddHom x) : (a : M) → β →₀ N) x_1 :
            β →₀ N) :
          (a : β) → N)
        a :
      N)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : α → β
v : α →₀ M
g : M → N
h0 : g 0 = 0
hadd : ∀ (x y : M), g (x + y) = g x + g y
⊢ mapDomain f (mapRange g h0 v) = mapRange g h0 (mapDomain f v)

Tactic:
let g' : M →+ N :=
    { toFun := g
      map_zero' := h0
      map_add' := hadd }
  DFunLike.congr_fun (mapDomain.addMonoidHom_comp_mapRange f g') v

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.mapDomain, Finsupp.sum, AddMonoidHom.mk, ZeroHom.mk, Finsupp.onFinset, Finsupp.mapRange, Finsupp.mapDomain.addMonoidHom_comp_mapRange, Finset.sum
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
rw : (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = f.sum g + g i a
⊢ (f.update i a).sum g + g i ((f : (a : ι) → α) i) = f.sum g + g i a

Tactic:
rw [update_eq_erase_add_single, sum_add_index' hg hgg]

Premises used: Finsupp.sum_add_index', Finsupp.update_eq_erase_add_single
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
rw : (f.update i ((f : (a : ι) → α) i)).sum g + g i a
| f.sum g + g i a

Tactic:
rw [← Finsupp.update_self f i]

Premises used: Finsupp.update_self
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
conv_rhs :
  (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = (f.update i ((f : (a : ι) → α) i)).sum g + g i a
⊢ (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = f.sum g + g i a

Tactic:
conv_rhs => rw [← Finsupp.update_self f i]

Premises used: Finsupp.update_self
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
rw :
  (erase i f).sum g + (sum (single i a) g + g i ((f : (a : ι) → α) i)) =
    (erase i f).sum g + (sum (single i ((f : (a : ι) → α) i)) g + g i a)
⊢ (erase i f).sum g + sum (single i a) g + g i ((f : (a : ι) → α) i) = (f.update i ((f : (a : ι) → α) i)).sum g + g i a

Tactic:
rw [update_eq_erase_add_single, sum_add_index' hg hgg, add_assoc, add_assoc]

Premises used: add_assoc, Finsupp.sum_add_index', Finsupp.update_eq_erase_add_single
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
e_a : sum (single i a) g + g i ((f : (a : ι) → α) i) = sum (single i ((f : (a : ι) → α) i)) g + g i a
⊢ (erase i f).sum g + (sum (single i a) g + g i ((f : (a : ι) → α) i)) =
    (erase i f).sum g + (sum (single i ((f : (a : ι) → α) i)) g + g i a)

Tactic:
congr 1
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : AddZeroClass α
inst_1 : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
e_a : g i ((f : (a : ι) → α) i) + sum (single i a) g = sum (single i ((f : (a : ι) → α) i)) g + g i a
e_a₁ : g i ((f : (a : ι) → α) i) + g i a = sum (single i ((f : (a : ι) → α) i)) g + g i a
e_a₂ e_a₃ : g i ((f : (a : ι) → α) i) + g i a = g i ((f : (a : ι) → α) i) + g i a
⊢ sum (single i a) g + g i ((f : (a : ι) → α) i) = sum (single i ((f : (a : ι) → α) i)) g + g i a

Tactic:
rw [add_comm, sum_single_index (hg _), sum_single_index (hg _)]

Premises used: Finsupp.sum_single_index, add_comm