mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case refine_3
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ (Multiset.map f (Multiset.map (fun i ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map f (Multiset.map (fun i ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_12
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ (equivMapDomain f l) x = (mapDomain (⇑f) l) x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
⊢ embDomain f (comapDomain (⇑f) g ⋯) = g

Tactic:
ext b

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b
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
a✝ : α
⊢ (comapDomain (⇑f) (embDomain f l) ⋯) a✝ = l a✝

Tactic:
simp

Goal state after:
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)
a✝ : α
⊢ (comapDomain f (v₁ + v₂) hv₁₂) a✝ = (comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: case isTrue
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
h✝ : p a✝
⊢ f a✝ + 0 = f a✝

Tactic:
simp

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

Goal state before:
pp: case isFalse
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
h✝ : ¬p a✝
⊢ 0 + f a✝ = f a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ (insert 0 ↑f.frange).Finite

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f : α →₀ M
hf : ∀ x ∈ f.support, p x
⊢ ∀ x ∈ support 0, p x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ n ^ (Multiset.map f s.val).card ≤ n ^ #s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0

Tactic:
simp

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
inst✝ : Zero M
f : α × β →₀ M
a : α
⊢ ∀ (a_1 : β), a_1 ∈ filterMap (fun x ↦ if x.1 = a then some x.2 else none) f.support ⋯ ↔ f (a, a_1) ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ 0 ^ 2 ≤ (∑ i ∈ s, f i) * 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α →₀ β →₀ M
a : α
b : β
⊢ (f.uncurry.curry a) b = (f a) b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α × β →₀ M
a : α
b : β
⊢ f.curry.uncurry (a, b) = f (a, b)

Tactic:
simp

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

Tactic:
simp

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
inst✝ : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ ∀ (a : α ⊕ β), a ∈ f.support.disjSum g.support ↔ Sum.elim (⇑f) (⇑g) a ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : α
⊢ (sumElim 0 0) (Sum.inl val✝) = 0 (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
val✝ : β
⊢ (sumElim 0 0) (Sum.inr val✝) = 0 (Sum.inr val✝)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : α
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inl val✝) = c (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
val✝ : β
⊢ ((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯)) (Sum.inr val✝) = c (Sum.inr val✝)

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : α
⊢ ((a + b).sumElim (c + d)) (Sum.inl val✝) = (a.sumElim c + b.sumElim d) (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val✝ : β
⊢ ((a + b).sumElim (c + d)) (Sum.inr val✝) = (a.sumElim c + b.sumElim d) (Sum.inr val✝)

Tactic:
simp

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

Goal state before:
pp: case inl
α✝ : 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 γ
f : α ⊕ β →₀ γ
a : α
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) (Sum.inl a) =
    f (Sum.inl a)

Tactic:
simp

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

Goal state before:
pp: case inr
α✝ : 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 γ
f : α ⊕ β →₀ γ
b : β
⊢ ((fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f)) (Sum.inr b) =
    f (Sum.inr b)

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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

Goal state before:
pp: 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✝

Tactic:
simp

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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (a_1 : α) (b : P a_1), ⟨a_1, b⟩ ∈ f.support ∧ a_1 = a → ¬∃ a_2 ∈ g.support, ↑a_2 = a

Tactic:
Subtype.exists

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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄ (a_1 : α) (b : P a_1),
    ⟨a_1, b⟩ ∈ f.support ∧ a_1 = a → ¬∃ a_2, ∃ (h : ¬P a_2), ⟨a_2, ⋯⟩ ∈ g.support ∧ a_2 = a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
s : Set α
M : Type u_12
inst✝ : AddCommMonoid M
a : ↑s
x : M
⊢ ↑((restrictSupportEquiv s M).symm (single a x)) = single (↑a) x

Tactic:
simp

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
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
⊢ ∀ (a : ι), a ∈ l.splitSupport ↔ g a (l.split a) ≠ 0

Tactic:
by
    intro i
    rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]

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 α✝
α : Type u_15
ιs : η → Type u_16
inst✝ : AddMonoid α
f g : (j : η) × ιs j →₀ α
x✝ : η
a✝ : ιs x✝
⊢ (sigmaFinsuppEquivPiFinsupp.toFun (f + g) x✝) a✝ =
    ((sigmaFinsuppEquivPiFinsupp.toFun f + sigmaFinsuppEquivPiFinsupp.toFun g) x✝) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
inst✝² : CommMonoid N
inst✝¹ : MulDistribMulAction M N
ι : Sort u_4
inst✝ : Finite ι
f : ι → N
r : M
val✝ : Fintype (PLift ι)
⊢ Function.mulSupport (?m.44 ∘ PLift.down) ⊆ ↑Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Fintype G
b : N
g : G
⊢ ∀ (i : G), i ∈ univ ↔ g * i ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: case nil
M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : MulOneClass N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
m : M
⊢ m ^ [].length • [].prod = (map (fun x ↦ m • x) []).prod

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
a : α
⊢ (mapDomain (fun x ↦ g • x) 0) a = 0 a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_3
G : Type u_5
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ (g • f) a = f (g⁻¹ • a)

Tactic:
by
  conv_lhs => rw [← smul_inv_smul g a]
  exact mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)

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

Goal state before:
pp: α : Type u_1
R : Type u_6
x✝ : Semiring R
c : R
a : α
b : R
⊢ c • single a b = single a (c * b)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: case empty
M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : CommMonoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
b : ι → M
f : ι → N
⊢ ∏ i ∈ ∅, b i • f i = (∏ i ∈ ∅, b i) • ∏ i ∈ ∅, f i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : AddMonoid N
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction R N
a : α
k : R
m : M
⊢ (↑(singleAddHom a)).toFun (k • m) = (MonoidHom.id R) k • (↑(singleAddHom a)).toFun m

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
x✝ : M
⊢ (lapply a ∘ₗ lsingle a) x✝ = LinearMap.id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
a✝ : α
⊢ (comapDomain f (x + y) ⋯) a✝ = (comapDomain f x ⋯ + comapDomain f y ⋯) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
a✝ : α
⊢ (comapDomain f (c • x) ⋯) a✝ = ((RingHom.id R) c • comapDomain f x ⋯) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: α✝ : Type u_1
M✝ : Type u_2
N : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹⁴ : Semiring R✝
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R₂ N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R₃ P
σ₁₂ : R✝ →+* R₂
σ₂₁ : R₂ →+* R✝
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R✝ →+* R₃
σ₃₁ : R₃ →+* R✝
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : α × β →₀ M
a✝¹ : α
a✝ : β
⊢ ((curryAddEquiv.toFun (c • f)) a✝¹) a✝ = (((RingHom.id R) c • curryAddEquiv.toFun f) a✝¹) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
⊢ (mapRange.addMonoidHom ↑f) (g • 0) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
⊢ lapply j ∘ₗ g ∘ₗ lsingle i • f m = ((RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (single i m)) j

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑1), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ = (1 x✝) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) = l i • single i 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : End (End R M) M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑(x✝² * x✝¹)), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ =
    (({ toFun := ⇑(mapRange.addMonoidHom ↑x✝²), map_add' := ⋯, map_smul' := ⋯ } *
          { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ })
        x✝)
      a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑0), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ = (0 x✝) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : End (End R M) M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑(x✝² + x✝¹)), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ =
    (({ toFun := ⇑(mapRange.addMonoidHom ↑x✝²), map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ })
        x✝)
      a✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x✝¹ x✝ : M
⊢ (f (single i (x✝¹ + x✝))) i = (f (single i x✝¹)) i + (f (single i x✝)) i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x✝¹ : End (End R M) M
x✝ : M
⊢ ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ })
        ((↑↑(ringHomEndFinsupp ι)).toFun x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
x : ι →₀ M
j : ι
⊢ (lsingle i ∘ₗ lapply j • f x) i = (f x) j

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F G : α → M →ₛₗ[σ] N
x : α
y : M
⊢ ({ toFun := fun d ↦ d.sum fun i ↦ ⇑((F + G) i), map_add' := ⋯, map_smul' := ⋯ } ∘ₛₗ lsingle x) y =
    (({ toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := fun d ↦ d.sum fun i ↦ ⇑(G i), map_add' := ⋯, map_smul' := ⋯ }) ∘ₛₗ
        lsingle x)
      y

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : S
G : α → M →ₛₗ[σ] N
x : α
y : M
⊢ ({ toFun := fun d ↦ d.sum fun i ↦ ⇑((F • G) i), map_add' := ⋯, map_smul' := ⋯ } ∘ₛₗ lsingle x) y =
    (((RingHom.id S) F • { toFun := fun d ↦ d.sum fun i ↦ ⇑(G i), map_add' := ⋯, map_smul' := ⋯ }) ∘ₛₗ lsingle x) y

Tactic:
simp

Goal state after: