mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Ext

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : MonoidHom.toAdditiveRight f = MonoidHom.toAdditiveRight g
⊢ f = g

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))
this : MonoidHom.toAdditiveRight f = MonoidHom.toAdditiveRight g
x✝¹ : α
x✝ : M
⊢ Additive.toMul (((MonoidHom.toAdditiveRight f).comp (singleAddHom x✝¹)) x✝) =
    Additive.toMul (((MonoidHom.toAdditiveRight g).comp (singleAddHom x✝¹)) x✝)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : Zero M
⊢ zeroHom (ZeroHom.id M) = ZeroHom.id (ι →₀ M)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : Zero M
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (ZeroHom.id M)) x✝) a✝ = ((ZeroHom.id (ι →₀ M)) x✝) a✝
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
⊢ zeroHom (f.comp f₂) = (zeroHom f).comp (zeroHom f₂)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
x✝ : ι →₀ M
a✝ : ι
⊢ ((zeroHom (f.comp f₂)) x✝) a✝ = (((zeroHom f).comp (zeroHom f₂)) x✝) a✝
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
b : M
⊢ ⇑(single a b) = Pi.single a b

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
a : α
b : M
x✝ : α
⊢ (single a b) x✝ = Pi.single a b x✝
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ single a₁ b₁ = single a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 → single a₁ b₁ = single a₂ b₂
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ single a b = 0 ↔ b = 0

Tactic:
by
  classical simp [DFunLike.ext_iff, single_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: M : Type u_8
inst✝ : AddZeroClass M
d : M
⊢ AddEquiv.finsuppUnique.symm d = single () d

Tactic:
ext

Goal state after:
M : Type u_8
inst✝ : AddZeroClass M
d : M
⊢ (AddEquiv.finsuppUnique.symm d) default = (single () d) default
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
⊢ l = single c b ∧ f c = a

Tactic:
constructor

Goal state after:
case h.left
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
⊢ l = single c b

case h.right
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
⊢ f c = a
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
f : N →+ O
g : M →+ N
⊢ addMonoidHom (f.comp g) = (addMonoidHom f).comp (addMonoidHom g)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
f : N →+ O
g : M →+ N
x✝ : ι →₀ M
a✝ : ι
⊢ ((addMonoidHom (f.comp g)) x✝) a✝ = (((addMonoidHom f).comp (addMonoidHom g)) x✝) a✝
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
⊢ addEquiv (AddEquiv.refl M) = AddEquiv.refl (ι →₀ M)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
x✝ : ι →₀ M
a✝ : ι
⊢ ((addEquiv (AddEquiv.refl M)) x✝) a✝ = ((AddEquiv.refl (ι →₀ M)) x✝) a✝
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
e₁ : M ≃+ N
e₂ : N ≃+ O
⊢ addEquiv (e₁.trans e₂) = (addEquiv e₁).trans (addEquiv e₂)

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid O
e₁ : M ≃+ N
e₂ : N ≃+ O
x✝ : ι →₀ M
a✝ : ι
⊢ ((addEquiv (e₁.trans e₂)) x✝) a✝ = (((addEquiv e₁).trans (addEquiv e₂)) x✝) a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ some 0 = 0

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ (some 0) a✝ = 0 a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
f g : Option α →₀ M
⊢ (f + g).some = f.some + g.some

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
f g : Option α →₀ M
a✝ : α
⊢ (f + g).some a✝ = (f.some + g.some) a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
m : M
⊢ (single none m).some = 0

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
m : M
a✝ : α
⊢ (single none m).some a✝ = 0 a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (embDomain Embedding.some f).some = f

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a✝ : α
⊢ (embDomain Embedding.some f).some a✝ = f a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
a : M
⊢ (f.update none a).some = f.some

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
a : M
a✝ : α
⊢ (f.update none a).some a✝ = f.some a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
⊢ (fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P) = P

Tactic:
ext

Goal state after:
case fst
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).1 = P.1

case snd
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
inst✝ : Zero M
P : M × (α →₀ M)
a✝ : α
⊢ ((fun P ↦ (P none, P.some)) ((fun P ↦ (embDomain Embedding.some P.2).update none P.1) P)).2 a✝ = P.2 a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f).some = f

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a✝ : α
⊢ (optionElim y f).some a✝ = f a✝
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ optionElim y f ≠ 0 → f ≠ 0 ∨ y ≠ 0

case mpr
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ f ≠ 0 ∨ y ≠ 0 → optionElim y f ≠ 0
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f k a = (s k).mulIndicator (f k) a

Tactic:
rw [mulIndicator_of_mem (hs hik hi)]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
⊢ s = t

Tactic:
ext

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s t : Set ι
inst✝ : Nontrivial M₀
h : s.indicator 1 = t.indicator 1
x✝ : ι
⊢ x✝ ∈ s ↔ x✝ ∈ t
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : IsReduced M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
⊢ (support fun a ↦ f a ^ n) = support f

Tactic:
ext

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : IsReduced M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x✝ : ι
⊢ (x✝ ∈ support fun a ↦ f a ^ n) ↔ x✝ ∈ support f
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : 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✝³ : AddCommMonoid B
inst✝² : 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✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
⊢ (fun F x ↦ F.comp (singleAddHom x))
      ((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ }) F) =
    F

Tactic:
ext

Goal state after:
α : 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✝³ : AddCommMonoid B
inst✝² : 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✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ((fun F x ↦ F.comp (singleAddHom x))
        ((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ }) F) x✝¹)
      x✝ =
    (F x✝¹) x✝
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : 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✝³ : AddCommMonoid B
inst✝² : 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✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
⊢ (fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ })
      ((fun F x ↦ F.comp (singleAddHom x)) F) =
    F

Tactic:
ext

Goal state after:
α : 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✝³ : AddCommMonoid B
inst✝² : 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✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F : (α →₀ M) →+ N
x✝¹ : α
x✝ : M
⊢ (((fun F ↦ { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ })
            ((fun F x ↦ F.comp (singleAddHom x)) F)).comp
        (singleAddHom x✝¹))
      x✝ =
    (F.comp (singleAddHom x✝¹)) x✝
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : 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✝³ : AddCommMonoid B
inst✝² : 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✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
⊢ { toFun := fun f ↦ f.sum fun x ↦ ⇑((F + G) x), map_zero' := ⋯, map_add' := ⋯ } =
    { toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ } +
      { toFun := fun f ↦ f.sum fun x ↦ ⇑(G x), map_zero' := ⋯, map_add' := ⋯ }

Tactic:
ext

Goal state after:
α : 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✝³ : AddCommMonoid B
inst✝² : 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✝¹ : AddZeroClass M
inst✝ : AddCommMonoid N
F G : α → M →+ N
x✝¹ : α
x✝ : M
⊢ ({ toFun := fun f ↦ f.sum fun x ↦ ⇑((F + G) x), map_zero' := ⋯, map_add' := ⋯ }.comp (singleAddHom x✝¹)) x✝ =
    (({ toFun := fun f ↦ f.sum fun x ↦ ⇑(F x), map_zero' := ⋯, map_add' := ⋯ } +
            { toFun := fun f ↦ f.sum fun x ↦ ⇑(G x), map_zero' := ⋯, map_add' := ⋯ }).comp
        (singleAddHom x✝¹))
      x✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1, f a_1 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) → f a = m ∧ m ≠ 0

case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ f a = m ∧ m ≠ 0 → ∃ a_2, f a_2 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_2 = (a, m)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
⊢ equivMapDomain f 0 = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ (equivMapDomain f 0) a✝ = 0 a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ (addMonoidHom f).comp (mapRange.addMonoidHom g) = (mapRange.addMonoidHom g).comp (addMonoidHom f)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x✝¹ : α
x✝ : M
a✝ : β
⊢ ((((addMonoidHom f).comp (mapRange.addMonoidHom g)).comp (singleAddHom x✝¹)) x✝) a✝ =
    ((((mapRange.addMonoidHom g).comp (addMonoidHom f)).comp (singleAddHom x✝¹)) x✝) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
l : α →₀ M
⊢ comapDomain (⇑f) (embDomain f l) ⋯ = l

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
l : α →₀ M
a✝ : α
⊢ (comapDomain (⇑f) (embDomain f l) ⋯) a✝ = l a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hif : Set.InjOn f (f ⁻¹' ↑(support 0))
⊢ comapDomain f 0 hif = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hif : Set.InjOn f (f ⁻¹' ↑(support 0))
a✝ : α
⊢ (comapDomain f 0 hif) a✝ = 0 a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
a✝ : α
⊢ (comapDomain f (v₁ + v₂) hv₁₂) a✝ = (comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1.e_v
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ (comapDomain.addMonoidHom ⋯) l = comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯

Tactic:
ext

Goal state after:
case refine_1.e_v
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
a✝ : ℕ
⊢ ((comapDomain.addMonoidHom ⋯) l) a✝ = (comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
⊢ comapDomain f (mapDomain f l) ⋯ = l

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : α →₀ M
a✝ : α
⊢ (comapDomain f (mapDomain f l) ⋯) a✝ = l a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a : α
⊢ filter (fun x ↦ a = x) f = single a (f a)

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (filter (fun x ↦ a = x) f) a✝ = (single a (f a)) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
⊢ ⇑(filter p f) = {x | p x}.indicator ⇑f

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
x✝ : α
⊢ (filter p f) x✝ = {x | p x}.indicator (⇑f) x✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p f + filter (fun x ↦ ¬p x) f = f

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ (filter p f + filter (fun x ↦ ¬p x) f) a✝ = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : 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✝ : AddZeroClass M
x✝¹ x✝ : α × β →₀ M
⊢ curryEquiv.toFun (x✝¹ + x✝) = curryEquiv.toFun x✝¹ + curryEquiv.toFun x✝

Tactic:
ext

Goal state after:
α : 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✝ : AddZeroClass M
x✝¹ x✝ : α × β →₀ M
a✝¹ : α
a✝ : β
⊢ ((curryEquiv.toFun (x✝¹ + x✝)) a✝¹) a✝ = ((curryEquiv.toFun x✝¹ + curryEquiv.toFun x✝) a✝¹) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ comapDomain Sum.inl (f.sumElim g) ⋯ = f

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
a✝ : α
⊢ (comapDomain Sum.inl (f.sumElim g) ⋯) a✝ = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ comapDomain Sum.inr (f.sumElim g) ⋯ = g

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
a✝ : β
⊢ (comapDomain Sum.inr (f.sumElim g) ⋯) a✝ = g a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
⊢ (fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg) = fg

Tactic:
ext

Goal state after:
case fst
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a✝ : α
⊢ ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg)).1 a✝ = fg.1 a✝

case snd
α✝ : 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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a✝ : β
⊢ ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) ((fun fg ↦ fg.1.sumElim fg.2) fg)).2 a✝ = fg.2 a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
⊢ sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝) = sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝

Tactic:
ext

Goal state after:
case fst
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
a✝ : α
⊢ (sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝)).1 a✝ =
    (sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝).1 a✝

case snd
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
a✝ : β
⊢ (sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝)).2 a✝ =
    (sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝).2 a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
⊢ (subtypeDomain P f).extendDomain = f

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a✝ : α
⊢ (subtypeDomain P f).extendDomain a✝ = f a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : 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✝ : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

Tactic:
by
    simp_rw [← equivMapDomain_trans, Equiv.self_trans_symm]
    exact equivMapDomain_refl _

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : 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
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) × ιs j →₀ α
⊢ (fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f.split = f

Tactic:
ext

Goal state after:
α : 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
αs : ι → Type u_12
inst✝² : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst✝¹ : Fintype η
ιs : η → Type u_14
inst✝ : Zero α
f : (j : η) × ιs j →₀ α
a✝ : (j : η) × ιs j
⊢ ((fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f.split) a✝ = f a✝