mathlib-initiative/mathlib-tactics huggingface dataset:
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; simp

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

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

Tactic:
simp [single_apply, Pi.single_apply, eq_comm]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Disjoint (single f₁ g₁).support (single f₂ g₂).support

Tactic:
· simp [support_single, *]

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) default = (single () d) default

Tactic:
simp [AddEquiv.finsuppUnique]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f : ι →₀ M
⊢ single a (f a) + erase a f = f

Tactic:
by
  rw [← update_eq_single_add_erase, update_self]

Goal state after:
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; simp

Goal state after:
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; simp

Goal state after:
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; simp

Goal state after:
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; simp

Goal state after:
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; simp

Goal state after:
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; simp

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a ↦ r a • f a) a = r a • s.indicator f a

Tactic:
dsimp only [indicator]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a ↦ r a • f a) a = s.indicator r a • f a

Tactic:
dsimp only [indicator]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
n : ℕ
h✝ : Subsingleton R
⊢ abv ↑n ≤ ↑n

pp: case inr
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
n : ℕ
h✝ : Nontrivial R
⊢ abv ↑n ≤ ↑n

Tactic:
· simp [Subsingleton.eq_zero (α := R)]

Goal state after:
case inr
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
n : ℕ
h✝ : Nontrivial R
⊢ abv ↑n ≤ ↑n
Module: Mathlib.Data.Finsupp.Basic

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

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

Tactic:
· obtain ⟨a, rfl⟩ := hb
    rw [embDomain_apply_self, comapDomain_apply]

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

Tactic:
ext; 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
⊢ curryEquiv.toFun (x✝¹ + x✝) = curryEquiv.toFun x✝¹ + curryEquiv.toFun x✝

Tactic:
ext; 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 : β →₀ γ
⊢ comapDomain Sum.inl (f.sumElim g) ⋯ = f

Tactic:
ext; 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 : β →₀ γ
⊢ comapDomain Sum.inr (f.sumElim g) ⋯ = g

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j

Tactic:
rw [prod_insert hs]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x
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 (equivMapDomain e.symm v) = v

Tactic:
simp_rw [← equivMapDomain_trans, Equiv.symm_trans_self]

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✝ : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain (Equiv.refl β) v = v
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ ∏ i ∈ insert a s, f i = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Tactic:
rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]

Goal state after:
ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∏ i ∈ s, f i = ∏ i ∈ s, g i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
h : x = 0
⊢ mapDomain f x = 0

Tactic:
by rw [h, mapDomain_zero]

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 : α
⊢ lapply a ∘ₗ lsingle a = LinearMap.id

Tactic:
ext; 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
⊢ comapDomain f (x + y) ⋯ = comapDomain f x ⋯ + comapDomain f y ⋯

Tactic:
ext; 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
⊢ comapDomain f (c • x) ⋯ = (RingHom.id R) c • comapDomain f x ⋯

Tactic:
ext; 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
⊢ curryAddEquiv.toFun (c • f) = (RingHom.id R) c • curryAddEquiv.toFun f

Tactic:
ext; 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
⊢ { toFun := ⇑(mapRange.addMonoidHom ↑1), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
ext; 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
⊢ { toFun := ⇑(mapRange.addMonoidHom ↑(x✝¹ * x✝)), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := ⇑(mapRange.addMonoidHom ↑x✝), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; 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
⊢ { toFun := ⇑(mapRange.addMonoidHom ↑0), map_add' := ⋯, map_smul' := ⋯ } = 0

Tactic:
ext; 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
⊢ { toFun := ⇑(mapRange.addMonoidHom ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := ⇑(mapRange.addMonoidHom ↑x✝), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; 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
⊢ (fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ })
      ((↑↑(ringHomEndFinsupp ι)).toFun x✝) =
    x✝

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
S : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
i : α
⊢ (lsum S) f ∘ₛₗ lsingle i = f i

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g

Tactic:
by
  cases f; cases g; congr

Goal state after:
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑(s.attachFin h) = Fin.val ⁻¹' ↑s

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1) = 1

Tactic:
simp only [HasFiniteMulSupport]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ (if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1) = 1
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ici (natAdd m i) = Ici i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Ioi (natAdd m i) = Ioi i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Iic (natAdd m i) = Iic i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ natAdd m ⁻¹' Iio (natAdd m i) = Iio i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) = Icc i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) = Ico i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) = Ioc i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) = Ioo i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioo i j = Ioo (natAdd m i) (natAdd m j)

Tactic:
← preimage_natAdd_Ioo_natAdd,

Goal state after:
n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Ioo (natAdd ?m i) (natAdd ?m j) = Ioo (natAdd m i) (natAdd m j)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ici (i.addNat m) = Ici i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) = Ioi i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Iic (i.addNat m) = Iic i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Iio (i.addNat m) = Iio i

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m) = Icc i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ico (i.addNat m) (j.addNat m) = Ico i j

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α' : Type u_7
v : α → M
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
w : α' → S
⊢ (linearCombination R fun i ↦ w i.2 • v i.1) =
    ↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(curryLinearEquiv R)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ioc (i.addNat m) (j.addNat m) = Ioc i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ioo (i.addNat m) (j.addNat m) = Ioo i j

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = (∏ i ∈ Finite.toFinset hf ∪ ?m.37, f i) * ∏ᶠ (i : α), g i

pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ Finset α

Tactic:
finprod_eq_prod_of_mulSupport_toFinset_subset g hg Finset.subset_union_right,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∏ᶠ (i : α), f i * g i = (∏ i ∈ Finite.toFinset hf ∪ ?m.37, f i) * ∏ i ∈ ?m.45 ∪ Finite.toFinset hg, g i

α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ Finset α

α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ Finset α
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

Tactic:
simp only [g.map_finprod_Prop]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Ico (↑a) n).attachFin ⋯ = Ici a

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Ioo (↑a) n).attachFin ⋯ = Ioi a

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Iic ↑a).attachFin ⋯ = Iic a

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Iio ↑a).attachFin ⋯ = Iio a

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ i ∈ s, ∏ i_1 ∈ t, f i i_1 = ∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i

Tactic:
exact Finset.prod_comm

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_7
M : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
h : span R (range v) = span R (range (-v))
⊢ Basis.span ⋯ =
    (Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ : Basis ι R M
v : ι → M
x y : M
inst✝ : Subsingleton R
x✝ : Basis ι R M
b : M ≃ₗ[R] ι →₀ R
⊢ { repr := b } = default

Tactic:
by rw [Subsingleton.elim b]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
⊢ ⇑(Basis.singleton ι R) = 1

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
⊢ v i ≠ 0

Tactic:
intro h
  have := @hv (Finsupp.single i 1 : ι →₀ R) 0 (by simpa using h)
  simp at this

Goal state after: