mathlib-initiative/mathlib-tactics huggingface dataset:
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 →₀ α
x✝ : η
a✝ : ιs x✝
⊢ (((fun f ↦ onFinset (univ.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f).split x✝) a✝ = (f x✝) 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
α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 →₀ α
⊢ sigmaFinsuppEquivPiFinsupp.toFun (f + g) = sigmaFinsuppEquivPiFinsupp.toFun f + sigmaFinsuppEquivPiFinsupp.toFun g

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 α✝
α : 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✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
⊢ embDomain f = mapDomain ⇑f

Tactic:
ext

Goal state after:
case e'_1.e'_4
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : β →₀ M
x✝ : α →₀ M
a✝ : β
⊢ (embDomain f x✝) a✝ = (mapDomain (⇑f) x✝) a✝
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 : mapDomain f x = 0
i : α
⊢ x i = 0 i

Tactic:
replace h := Finsupp.ext_iff.mp h (f i)

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
i : α
h : (mapDomain f x) (f i) = 0 (f i)
⊢ x i = 0 i
Module: Mathlib.Data.Finsupp.SMulWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
a : R
⊢ a • 0 = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
a : R
a✝ : α
⊢ (a • 0) a✝ = 0 a✝
Module: Mathlib.Data.Finsupp.SMulWithZero

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst✝³ : Zero M
inst✝² : SMulZeroClass R M
inst✝¹ : Zero N
inst✝ : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
⊢ mapRange f hf (c • v) = d • mapRange f hf v

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst✝³ : Zero M
inst✝² : SMulZeroClass R M
inst✝¹ : Zero N
inst✝ : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
a✝ : α
⊢ (mapRange f hf (c • v)) a✝ = (d • mapRange f hf v) a✝
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
f f' : α →₀ M
⊢ g • (f + f') = g • f + g • f'

Tactic:
ext

Goal state after:
α : 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
f f' : α →₀ M
a✝ : α
⊢ (g • (f + f')) a✝ = (g • f + g • f') a✝
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support)
⊢ comapDomain f (r • v) hfrv = r • comapDomain f v hfv

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' ↑v.support)
hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support)
a✝ : α
⊢ (comapDomain f (r • v) hfrv) a✝ = (r • comapDomain f v hfv) a✝
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

Goal state after:
α : 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✝
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 a' : α
h : a ≠ a'
⊢ lapply a ∘ₗ lsingle a' = 0

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
x✝ : M
⊢ (lapply a ∘ₗ lsingle a') x✝ = 0 x✝
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

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

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

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

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

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

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

Goal state after:
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✝
Module: Mathlib.LinearAlgebra.Finsupp.Supported

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
l : α →₀ M
h : l ∈ supported M R ∅
⊢ l = 0

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ l a✝ = 0 a✝
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

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

Goal state after:
α : 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 : α
x✝ : M
⊢ ((lsum S) f ∘ₛₗ lsingle i) x✝ = (f i) x✝
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
X : Type u_9
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
m✝ : S
x✝ : X → M
⊢ (lift M R X) (m✝ • x✝) = m✝ • (lift M R X) x✝

Tactic:
ext

Goal state after:
α : 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
X : Type u_9
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
m✝ : S
x✝ : X → M
a✝ : X
⊢ ((lift M R X) (m✝ • x✝) ∘ₗ lsingle a✝) 1 = ((m✝ • (lift M R X) x✝) ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ_inv
inst✝ : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
⊢ (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm

Tactic:
ext

Goal state after:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ_inv
inst✝ : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
x✝ : κ →₀ N
a✝ : ι
⊢ ((lcongr e₁ e₂).symm x✝) a✝ = ((lcongr e₁.symm e₂.symm) x✝) a✝
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
⊢ linearCombination R (⇑f ∘ v) = f ∘ₗ linearCombination R v

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
f : M →ₗ[R] M'
a✝ : α
⊢ (linearCombination R (⇑f ∘ v) ∘ₗ lsingle a✝) 1 = ((f ∘ₗ linearCombination R v) ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
v : α → M
x : M
⊢ x ∈ (linearCombination R v).range ↔ x ∈ span R (Set.range v)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ (linearCombination R v).range → x ∈ span R (Set.range v)

case mpr
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) → x ∈ (linearCombination R v).range
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

Goal state after:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
x✝ : Fin n
⊢ x✝ ∈ ↑(s.attachFin h) ↔ x✝ ∈ Fin.val ⁻¹' ↑s
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
⊢ range val = Iio n

Tactic:
ext

Goal state after:
n x✝ : ℕ
⊢ x✝ ∈ range val ↔ x✝ ∈ Iio n
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
K : Type u_5
M : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
f g : Basis ι R M
h : (fun b i ↦ b.repr.symm (single i 1)) f = (fun b i ↦ b.repr.symm (single i 1)) g
⊢ ↑f.repr.symm = ↑g.repr.symm

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
K : Type u_5
M : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
f g : Basis ι R M
h : (fun b i ↦ b.repr.symm (single i 1)) f = (fun b i ↦ b.repr.symm (single i 1)) g
a✝ : ι
⊢ (↑f.repr.symm ∘ₗ lsingle a✝) 1 = (↑g.repr.symm ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)

Tactic:
ext

Goal state after:
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
a✝ : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1 = (linearCombination R (v' ∘ f) ∘ₗ lsingle a✝) 1
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
i : Fin (m + n)
⊢ i ∈ range (natAdd m) ↔ i ∈ {i | m ≤ ↑i}

Tactic:
constructor

Goal state after:
case mp
m n : ℕ
i : Fin (m + n)
⊢ i ∈ range (natAdd m) → i ∈ {i | m ≤ ↑i}

case mpr
m n : ℕ
i : Fin (m + n)
⊢ i ∈ {i | m ≤ ↑i} → i ∈ range (natAdd m)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: case mpr
m n : ℕ
i : Fin (m + n)
hi : m ≤ ↑i
⊢ natAdd m ⟨↑i - m, ⋯⟩ = i

Tactic:
ext

Goal state after:
case mpr
m n : ℕ
i : Fin (m + n)
hi : m ≤ ↑i
⊢ ↑(natAdd m ⟨↑i - m, ⋯⟩) = ↑i
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

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ici (natAdd m i) ↔ x✝ ∈ Ici i
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

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioi (natAdd m i) ↔ x✝ ∈ Ioi i
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

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Iic (natAdd m i) ↔ x✝ ∈ Iic i
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

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Iio (natAdd m i) ↔ x✝ ∈ Iio i
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

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) ↔ x✝ ∈ Icc i j
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

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ico i j
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

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ioc i j
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

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ioo i j