awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain (f.trans g) l : (a : γ) → M) x : M)
    ((equivMapDomain g (equivMapDomain f l) : (a : γ) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : Zero M
f : α ≃ β
g : β ≃ γ
h :
  ∀ (x : α →₀ M) (a : γ),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain (f.trans g) x : (a : γ) → M) a : M)
      (((equivMapDomain g ∘ equivMapDomain f) x : (a : γ) → M) a : M)
⊢ Eq (α := (l : α →₀ M) → γ →₀ M) (equivMapDomain (f.trans g)) (equivMapDomain g ∘ equivMapDomain f)

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a : γ
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain (f.trans g) x : (a : γ) → M) a : M)
    (((equivMapDomain g ∘ equivMapDomain f) x : (a : γ) → M) a : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
a : α
b : M
h :
  ∀ (x : β),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain f (single a b) : (a : β) → M) x : M)
      (((single ((f : (a : α) → β) a) b : β →₀ M) : (a : β) → M) x : M)
⊢ Eq (α := β →₀ M) (equivMapDomain f (single a b)) (single ((f : (a : α) → β) a) b)

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain f (single a b) : (a : β) → M) x : M)
    (((single ((f : (a : α) → β) a) b : β →₀ M) : (a : β) → M) x : M)

Tactic:
simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]

Premises used: Finsupp.equivMapDomain_apply, Finsupp.single_apply, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
a : α
b : M
h :
  ∀ (x : β),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain f (single a b) : (a : β) → M) x : M)
      (((single ((f : (a : α) → β) a) b : β →₀ M) : (a : β) → M) x : M)
⊢ Eq (α := β →₀ M) (equivMapDomain f (single a b)) (single ((f : (a : α) → β) a) b)

Tactic:
classical
    ext x
    simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]

Premises used: Finsupp.equivMapDomain_apply, Finsupp.single_apply, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
h : ∀ (a : β), Eq.{u_5 + 1} (α := M) ((equivMapDomain f 0 : (a : β) → M) a : M) ((0 : (a : β) → M) a : M)
⊢ Eq (α := β →₀ M) (equivMapDomain f 0) 0

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
a : β
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain f 0 : (a : β) → M) a : M) ((0 : (a : β) → M) a : M)

Tactic:
simp only [equivMapDomain_apply, coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Finsupp.equivMapDomain_apply, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : Zero M
inst_1 : CommMonoid N
f : α ≃ β
l : α →₀ M
g : β → M → N
⊢ (equivMapDomain f l).prod g = l.prod fun (a : α) (m : M) ↦ g ((f : (a : α) → β) a) m

Tactic:
simp [prod, equivMapDomain]

Premises used: Finsupp.equivMapDomain, Finsupp.prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α ≃ β
refine_1 : ∀ (f_1 : α →₀ M), equivMapDomain f.symm (equivMapDomain f f_1) = f_1
refine_2 : ∀ (f_1 : β →₀ M), equivMapDomain f (equivMapDomain f.symm f_1) = f_1
⊢ (α →₀ M) ≃ (β →₀ M)

Tactic:
refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f_1 : α ≃ β
f : α →₀ M
refine_1 :
  ∀ (x : α),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain f_1.symm (equivMapDomain f_1 f) : (a : α) → M) x : M)
      ((f : (a : α) → M) x : M)
⊢ equivMapDomain f_1.symm (equivMapDomain f_1 f) = f

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f_1 : α ≃ β
f : β →₀ M
refine_2 :
  ∀ (x : β),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain f_1 (equivMapDomain f_1.symm f) : (a : β) → M) x : M)
      ((f : (a : β) → M) x : M)
⊢ equivMapDomain f_1 (equivMapDomain f_1.symm f) = f

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f_1 : α ≃ β
f : α →₀ M
x : α
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain f_1.symm (equivMapDomain f_1 f) : (a : α) → M) x : M) ((f : (a : α) → M) x : M)

Tactic:
simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply,
      Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_apply, Equiv.symm_symm, Finsupp.equivMapDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f_1 : α ≃ β
f : β →₀ M
x : β
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain f_1 (equivMapDomain f_1.symm f) : (a : β) → M) x : M) ((f : (a : β) → M) x : M)

Tactic:
simp only [equivMapDomain_apply, Equiv.symm_symm, Equiv.symm_apply_apply,
      Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_apply, Equiv.symm_symm, Finsupp.equivMapDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
l : α →₀ M
⊢ (equivCongrLeft f : (a : α →₀ M) → β →₀ M) l = equivMapDomain f l

Tactic:
rfl

Premises used: Finsupp.equivMapDomain, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
⊢ Eq (α := (β →₀ M) ≃ (α →₀ M)) (Equiv.symm (equivCongrLeft f)) (equivCongrLeft f.symm)

Tactic:
rfl

Premises used: Finsupp.equivMapDomain, Equiv.symm, Finsupp.equivCongrLeft, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
R : Type u_10
inst : Zero M
f : α →₀ M
inst_1 : CommSemiring R
g : α → M → ℕ
⊢ Eq.{u_10 + 1} (α := R) (↑(f.prod g) : R) (f.prod fun (a : α) (b : M) ↦ (↑(g a b) : R))

Tactic:
Nat.cast_prod _ _

Premises used: Nat.cast_prod, Finsupp.prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
R : Type u_10
inst : Zero M
f : α →₀ M
inst_1 : AddCommMonoidWithOne R
g : α → M → ℕ
⊢ Eq.{u_10 + 1} (α := R) (↑(f.sum g) : R) (f.sum fun (a : α) (b : M) ↦ (↑(g a b) : R))

Tactic:
Nat.cast_sum _ _

Premises used: Finsupp.sum, Nat.cast_sum
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
R : Type u_10
inst : Zero M
f : α →₀ M
inst_1 : CommRing R
g : α → M → ℤ
⊢ Eq.{u_10 + 1} (α := R) (↑(f.prod g) : R) (f.prod fun (a : α) (b : M) ↦ (↑(g a b) : R))

Tactic:
Int.cast_prod _ _

Premises used: Int.cast_prod, Finsupp.prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
R : Type u_10
inst : Zero M
f : α →₀ M
inst_1 : AddCommGroupWithOne R
g : α → M → ℤ
⊢ Eq.{u_10 + 1} (α := R) (↑(f.sum g) : R) (f.sum fun (a : α) (b : M) ↦ (↑(g a b) : R))

Tactic:
Int.cast_sum _ _

Premises used: Finsupp.sum, Int.cast_sum
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
R : Type u_10
inst : Zero M
f : α →₀ M
inst_1 : DivisionRing R
inst_2 : CharZero R
g : α → M → ℚ
⊢ Eq.{u_10 + 1} (α := R) (↑(f.sum g) : R) (f.sum fun (a : α) (b : M) ↦ (↑(g a b) : R))

Tactic:
cast_sum _ _

Premises used: Finsupp.sum, Rat.cast_sum
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
R : Type u_10
inst : Zero M
f : α →₀ M
inst_1 : Field R
inst_2 : CharZero R
g : α → M → ℚ
⊢ Eq.{u_10 + 1} (α := R) (↑(f.prod g) : R) (f.prod fun (a : α) (b : M) ↦ (↑(g a b) : R))

Tactic:
cast_prod _ _

Premises used: Finsupp.prod, Rat.cast_prod
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h₀ :
  ∀ (b : α),
    Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M) →
      b ≠ a → Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)
h₁ :
  Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) a : M) (0 : M) →
    Eq.{u_5 + 1} (α := M) ((single (f a) 0 : (a : β) → M) (f a) : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)

Tactic:
rw [mapDomain, sum_apply, sum_eq_single a, single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.mapDomain, Finsupp.sum_eq_single, Finsupp.sum_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
h₀ :
  Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M) →
    b ≠ a → Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)
⊢ Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M) →
    b ≠ a → Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)

Tactic:
_
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
h : Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M)
hba : b ≠ a
⊢ Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)

Tactic:
single_eq_of_ne' (hf.ne hba)

Premises used: Finsupp.single_eq_of_ne', Function.Injective.ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
h : Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M)
hba : b ≠ a
⊢ Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)

Tactic:
exact single_eq_of_ne' (hf.ne hba)

Premises used: Finsupp.single_eq_of_ne', Function.Injective.ne
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h : Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) a : M) (0 : M)
h₁ : Eq.{u_5 + 1} (α := M) ((0 : (a : β) → M) (f a) : M) (0 : M)
h₂ : Eq.{u_5 + 1} (α := M) (0 (f a)) 0
h₃ h₄ : Eq.{u_5 + 1} (α := M) 0 0
⊢ Eq.{u_5 + 1} (α := M) ((single (f a) 0 : (a : β) → M) (f a) : M) (0 : M)

Tactic:
rw [single_zero, coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Finsupp.single_zero, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' (↑x.support : Set α)
rw :
  ∀ x_1 ∈ x.support,
    Eq.{u_5 + 1} (α := M) (((single (f x_1) ((x : (a : α) → M) x_1) : β →₀ M) : (a : β) → M) b : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) b : M) (0 : M)

Tactic:
rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]

Premises used: Finsupp.mapDomain, Finset.sum_eq_zero, Finsupp.sum, Finsupp.sum_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' (↑x.support : Set α)
⊢ ∀ x_1 ∈ x.support,
    Eq.{u_5 + 1} (α := M) (((single (f x_1) ((x : (a : α) → M) x_1) : β →₀ M) : (a : β) → M) b : M) (0 : M)

Tactic:
fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha

Premises used: Finsupp.single_eq_of_ne, Eq.rec, Set.mem_image_of_mem, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' (↑x.support : Set α)
⊢ ∀ x_1 ∈ x.support,
    Eq.{u_5 + 1} (α := M) (((single (f x_1) ((x : (a : α) → M) x_1) : β →₀ M) : (a : β) → M) b : M) (0 : M)

Tactic:
exact fun a ha ↦ single_eq_of_ne fun eq => hb <| eq ▸ Set.mem_image_of_mem _ ha
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h grw : a ∉ Set.range f
⊢ a ∉ f '' (↑x.support : Set α)

Tactic:
grw [Set.image_subset_range]

Premises used: Set.image_subset_range
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ Set.range f

Tactic:
h
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ a ∉ Set.range f

Tactic:
exact h
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
⊢ mapDomain id v = v

Tactic:
sum_single _

Premises used: Finsupp.mapDomain, Finsupp.sum_single
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

Tactic:
((sum_sum_index ?_ ?_).trans ?_).symm

Premises used: Finsupp.mapDomain, Eq.symm, Eq.trans, Finsupp.sum_sum_index
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
refine_1 : ∀ (a : β), Eq (α := γ →₀ M) (single (g a) 0) 0
refine_2 : ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = HAdd.hAdd (α := γ →₀ M) (single (g a) b₁) (single (g a) b₂)
refine_3 : (v.sum fun (a : α) (b : M) ↦ sum (single (f a) b) fun (a : β) ↦ single (g a)) = mapDomain (g ∘ f) v
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

Tactic:
refine ((sum_sum_index ?_ ?_).trans ?_).symm

Premises used: Eq.symm, Eq.trans, Finsupp.sum_sum_index
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a : β
⊢ Eq (α := γ →₀ M) (single (g a) 0) 0

Tactic:
single_zero _

Premises used: Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a : β
⊢ Eq (α := γ →₀ M) (single (g a) 0) 0

Tactic:
exact single_zero _

Premises used: Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a : β
⊢ ∀ (b₁ b₂ : M), single (g a) (b₁ + b₂) = HAdd.hAdd (α := γ →₀ M) (single (g a) b₁) (single (g a) b₂)

Tactic:
single_add _

Premises used: Finsupp.single_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a : β
⊢ ∀ (b₁ b₂ : M), single (g a) (b₁ + b₂) = HAdd.hAdd (α := γ →₀ M) (single (g a) b₁) (single (g a) b₂)

Tactic:
exact single_add _

Premises used: Finsupp.single_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ (v.sum fun (a : α) (b : M) ↦ sum (single (f a) b) fun (a : β) ↦ single (g a)) = mapDomain (g ∘ f) v

Tactic:
sum_congr fun _ _ => sum_single_index ?_

Premises used: Finsupp.sum_single_index, Finsupp.mapDomain, Finsupp.sum_congr
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
refine_3 : ∀ x ∈ v.support, Eq (α := γ →₀ M) (single (g (f x)) 0) 0
⊢ (v.sum fun (a : α) (b : M) ↦ sum (single (f a) b) fun (a : β) ↦ single (g a)) = mapDomain (g ∘ f) v

Tactic:
refine sum_congr fun _ _ => sum_single_index ?_

Premises used: Finsupp.sum_congr
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
x : α
h : x ∈ v.support
⊢ Eq (α := γ →₀ M) (single (g (f x)) 0) 0

Tactic:
single_zero _

Premises used: Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
x : α
h : x ∈ v.support
⊢ Eq (α := γ →₀ M) (single (g (f x)) 0) 0

Tactic:
exact single_zero _

Premises used: Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
a : α
b : M
⊢ Eq (α := β →₀ M) (mapDomain f (single a b)) (single (f a) b)

Tactic:
sum_single_index <| single_zero _

Premises used: Finsupp.sum_single_index, Finsupp.mapDomain, Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
⊢ Eq (α := β →₀ M) (mapDomain f 0) 0

Tactic:
sum_zero_index

Premises used: Finsupp.mapDomain, Finsupp.sum_zero_index
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f g : α → β
h : ∀ x ∈ v.support, f x = g x
x : α
H : x ∈ v.support
⊢ Eq (α := β →₀ M) ((fun (a : α) ↦ (single (f a) : (b : M) → β →₀ M)) x ((v : (a : α) → M) x))
    ((fun (a : α) ↦ (single (g a) : (b : M) → β →₀ M)) x ((v : (a : α) → M) x))

Tactic:
simp only [h _ H]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
v₁ v₂ : α →₀ M
f : α → β
⊢ mapDomain f (v₁ + v₂) = mapDomain f v₁ + mapDomain f v₂

Tactic:
sum_add_index' (fun _ => single_zero _) fun _ => single_add _

Premises used: Finsupp.mapDomain, Finsupp.sum_add_index', Finsupp.single_add, Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
β : Type u_13
M : Type u_14
inst : AddCommGroup M
v₁ v₂ : α →₀ M
f : α → β
⊢ mapDomain f (v₁ - v₂) = HSub.hSub (α := β →₀ M) (mapDomain f v₁) (mapDomain f v₂)

Tactic:
simp [mapDomain, sum_sub_index]

Premises used: Finsupp.sum_sub_index, Finsupp.mapDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
rw : ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β) : M)
| ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) a : M)

Tactic:
rw [← f.apply_symm_apply a]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
conv_lhs :
  Eq.{u_5 + 1} (α := M)
    ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β) : M)
    ((x : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) a : M)
    ((x : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M)

Tactic:
conv_lhs => rw [← f.apply_symm_apply a]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
⊢ Eq.{u_5 + 1} (α := M)
    ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β) : M)
    ((x : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M)

Tactic:
mapDomain_apply f.injective _ _

Premises used: Finsupp.mapDomain_apply, Equiv.injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
⊢ Eq.{u_5 + 1} (α := M)
    ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β) : M)
    ((x : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M)

Tactic:
exact mapDomain_apply f.injective _ _

Premises used: Finsupp.mapDomain_apply, Equiv.injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : AddCommMonoid M
⊢ Eq (α := (α →₀ M) →+ α →₀ M) (addMonoidHom id) (AddMonoidHom.id (α →₀ M))

Tactic:
AddMonoidHom.ext fun _ => mapDomain_id

Premises used: Finsupp.mapDomain_id, AddMonoidHom.ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
f : β → γ
g : α → β
⊢ Eq (α := (α →₀ M) →+ γ →₀ M) (addMonoidHom (f ∘ g)) (AddMonoidHom.comp (addMonoidHom f) (addMonoidHom g))

Tactic:
AddMonoidHom.ext fun _ => mapDomain_comp

Premises used: AddMonoidHom.ext, Finsupp.mapDomain_comp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
M : Type u_5
inst : AddCommMonoid M
f : α → β
s : Finset ι
v : ι → α →₀ M
⊢ Eq (α := β →₀ M) (mapDomain f (∑ i ∈ s, v i)) (∑ i ∈ s, mapDomain f (v i))

Tactic:
map_sum (mapDomain.addMonoidHom f) _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, map_sum, Finsupp.mapDomain.addMonoidHom, Finset.sum
-- 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 : Zero N
f : α → β
s : α →₀ N
v : α → N → α →₀ M
⊢ mapDomain f (s.sum v) = s.sum fun (a : α) (b : N) ↦ mapDomain f (v a b)

Tactic:
map_finsuppSum (mapDomain.addMonoidHom f : (α →₀ M) →+ β →₀ M) _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finsupp.mapDomain.addMonoidHom, map_finsuppSum, Finset.sum
-- 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
rw rw₁ : image f s.support ⊆ image f s.support
⊢ (s.support.biUnion fun (x : α) ↦ {f x}) ⊆ image f s.support

Tactic:
rw [Finset.biUnion_singleton]

Premises used: Finset.biUnion_singleton
-- 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) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : 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:
rw [mapDomain, sum_apply, sum]

Premises used: Finsupp.mapDomain, Finsupp.sum, Finsupp.sum_apply
-- 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
simp_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)
⊢ 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)

Tactic:
simp_rw [single_apply]

Premises used: Finsupp.single_apply
-- 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
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 :
  ∀ (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) (∑ 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:
by_cases hax : a ∈ x.support

Premises used: Finsupp.support
-- 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
pos :
  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
⊢ 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 [← Finset.add_sum_erase _ _ hax, if_pos rfl]

Premises used: if_pos, Finset.add_sum_erase, rfl