mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase i f).support = f.support.erase i

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
a✝ : ι
⊢ a✝ ∈ (erase i f).support ↔ a✝ ∈ f.support.erase i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
a✝ : Subtype p
⊢ a✝ ∈ (subtypeDomain p f).support ↔ a✝ ∈ Finset.subtype p f.support
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ (-f).support = f.support

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
a✝ : ι
⊢ a✝ ∈ (-f).support ↔ a✝ ∈ f.support
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
⊢ comapDomain h hh 0 = 0

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ (comapDomain h hh 0) i✝ = 0 i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
⊢ comapDomain h hh (f + g) = comapDomain h hh f + comapDomain h hh g

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (f + g)) i✝ = (comapDomain h hh f + comapDomain h hh g) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
⊢ comapDomain' h hh' 0 = 0

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ (comapDomain' h hh' 0) i✝ = 0 i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f + comapDomain' h hh' g) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

Tactic:
by
  ext
  rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)) = x

Tactic:
ext

Goal state after:
case fst
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)).1 = x.1

case snd
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i✝ : ι
⊢ ((extendWith x.1 x.2) none, comapDomain some ⋯ (extendWith x.1 x.2)).2 i✝ = x.2 i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

Tactic:
ext

Goal state after:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf (g₁ + g₂)) i✝ = (mapRange f hf g₁ + mapRange f hf g₂) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
f₂ : (i : ι) → β i →+ β₁ i
⊢ (addMonoidHom fun i ↦ (f i).comp (f₂ i)) = (addMonoidHom f).comp (addMonoidHom f₂)

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
f₂ : (i : ι) → β i →+ β₁ i
x✝ : Π₀ (i : ι), β i
i✝ : ι
⊢ ((addMonoidHom fun i ↦ (f i).comp (f₂ i)) x✝) i✝ = (((addMonoidHom f).comp (addMonoidHom f₂)) x✝) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β i ≃+ β₁ i
f₂ : (i : ι) → β₁ i ≃+ β₂ i
⊢ (addEquiv fun i ↦ (f i).trans (f₂ i)) = (addEquiv f).trans (addEquiv f₂)

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β i ≃+ β₁ i
f₂ : (i : ι) → β₁ i ≃+ β₂ i
x✝ : Π₀ (i : ι), β i
i✝ : ι
⊢ ((addEquiv fun i ↦ (f i).trans (f₂ i)) x✝) i✝ = (((addEquiv f).trans (addEquiv f₂)) x✝) i✝
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
x : (i : ι) → β i →+ γ
⊢ (fun F i ↦ F.comp (singleAddHom β i)) (sumAddHom x) = x

Tactic:
ext

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
x : (i : ι) → β i →+ γ
x✝¹ : ι
x✝ : β x✝¹
⊢ ((fun F i ↦ F.comp (singleAddHom β i)) (sumAddHom x) x✝¹) x✝ = (x x✝¹) x✝
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
⊢ sumAddHom ((fun F i ↦ F.comp (singleAddHom β i)) ψ) = ψ

Tactic:
ext

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
x✝¹ : ι
x✝ : β x✝¹
⊢ ((sumAddHom ((fun F i ↦ F.comp (singleAddHom β i)) ψ)).comp (singleAddHom β x✝¹)) x✝ =
    (ψ.comp (singleAddHom β x✝¹)) x✝
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
F G : (i : ι) → β i →+ γ
⊢ sumAddHom (F + G) = sumAddHom F + sumAddHom G

Tactic:
ext

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
F G : (i : ι) → β i →+ γ
x✝¹ : ι
x✝ : β x✝¹
⊢ ((sumAddHom (F + G)).comp (singleAddHom β x✝¹)) x✝ = ((sumAddHom F + sumAddHom G).comp (singleAddHom β x✝¹)) x✝
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((f - g).sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) =
    (f.sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) - g.sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)
⊢ (f - g).sum h = f.sum h - g.sum h
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
⊢ id.dualMap = id

Tactic:
ext

Goal state after:
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ (id.dualMap x✝¹) x✝ = (id x✝¹) x✝
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
⊢ (refl R M₁).dualMap = refl R (Dual R M₁)

Tactic:
ext

Goal state after:
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ ((refl R M₁).dualMap x✝¹) x✝ = ((refl R (Dual R M₁)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: case refine_1
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : m ∈ (dualMap f).range
r : Dual R R
hr : (dualMap f) r = m
⊢ r 1 • f = m

Tactic:
ext

Goal state after:
case refine_1
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝¹ : m ∈ (dualMap f).range
r : Dual R R
hr : (dualMap f) r = m
x✝ : M₁
⊢ (r 1 • f) x✝ = m x✝
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: case refine_2
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : ∃ a, a • f = m
r : R
hr : r • f = m
⊢ (dualMap f) (r • id) = m

Tactic:
ext

Goal state after:
case refine_2
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝¹ : ∃ a, a • f = m
r : R
hr : r • f = m
x✝ : M₁
⊢ ((dualMap f) (r • id)) x✝ = m x✝
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
⊢ ↑(evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M)

Tactic:
ext

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
x✝¹ : Dual R M
x✝ : Dual R (Dual R M)
⊢ (↑(evalEquiv R M).symm.dualMap x✝¹) x✝ = ((Dual.eval R (Dual R M)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.ker = f.range.dualAnnihilator

Tactic:
ext

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ x✝ ∈ f.dualMap.ker ↔ x✝ ∈ f.range.dualAnnihilator
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
⊢ lapply i ∘ₗ lsingle i = LinearMap.id

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
x✝ : M i
⊢ (lapply i ∘ₗ lsingle i) x✝ = LinearMap.id x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
⊢ lapply i ∘ₗ lsingle i' = 0

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
x✝ : M i'
⊢ (lapply i ∘ₗ lsingle i') x✝ = 0 x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ x✝ : Π₀ (i : ι), M i
⊢ (equivCongrLeft e).toFun (x✝¹ + x✝) = (equivCongrLeft e).toFun x✝¹ + (equivCongrLeft e).toFun x✝

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ x✝ : Π₀ (i : ι), M i
i✝ : ι'
⊢ ((equivCongrLeft e).toFun (x✝¹ + x✝)) i✝ = ((equivCongrLeft e).toFun x✝¹ + (equivCongrLeft e).toFun x✝) i✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ : R
x✝ : Π₀ (i : ι), M i
⊢ (equivCongrLeft e).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ : R
x✝ : Π₀ (i : ι), M i
i✝ : ι'
⊢ ((equivCongrLeft e).toFun (x✝¹ • x✝)) i✝ = ((RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝) i✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
⊢ __spread✝⁻⁰.toFun (x✝¹ + x✝) = __spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ + x✝)) i✝¹) i✝ = ((__spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝) i✝¹) i✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ : R
x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
⊢ __spread✝⁻⁰.toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • __spread✝⁻⁰.toFun x✝

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ : R
x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ • x✝)) i✝¹) i✝ = (((RingHom.id R) x✝¹ • __spread✝⁻⁰.toFun x✝) i✝¹) i✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ x✝ : Π₀ (i : ι), M i
⊢ equivFunOnFintype.toFun (x✝¹ + x✝) = equivFunOnFintype.toFun x✝¹ + equivFunOnFintype.toFun x✝

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝² x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² + x✝¹) x✝ = (equivFunOnFintype.toFun x✝² + equivFunOnFintype.toFun x✝¹) x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝¹ : R
x✝ : Π₀ (i : ι), M i
⊢ equivFunOnFintype.toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • equivFunOnFintype.toFun x✝

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝² : R
x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² • x✝¹) x✝ = ((RingHom.id R) x✝² • equivFunOnFintype.toFun x✝¹) x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F G : (i : ι) → M i →ₗ[R] N
i : ι
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((F + G) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ lsingle i =
    ({ toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := ⇑(sumAddHom fun i ↦ (G i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      lsingle i

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F G : (i : ι) → M i →ₗ[R] N
i : ι
x✝ : M i
⊢ ({ toFun := ⇑(sumAddHom fun i ↦ ((F + G) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ lsingle i) x✝ =
    (({ toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := ⇑(sumAddHom fun i ↦ (G i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
        lsingle i)
      x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
c : S
F : (i : ι) → M i →ₗ[R] N
i : ι
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((c • F) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ lsingle i =
    ((RingHom.id S) c • { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      lsingle i

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
c : S
F : (i : ι) → M i →ₗ[R] N
i : ι
x✝ : M i
⊢ ({ toFun := ⇑(sumAddHom fun i ↦ ((c • F) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ lsingle i) x✝ =
    (((RingHom.id S) c • { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
        lsingle i)
      x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
⊢ (fun F i ↦ F ∘ₗ lsingle i)
      ((fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) F) =
    F

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
x✝¹ : ι
x✝ : M x✝¹
⊢ ((fun F i ↦ F ∘ₗ lsingle i)
        ((fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) F) x✝¹)
      x✝ =
    (F x✝¹) x✝