mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set α
p : α →₀ M
⊢ p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0

Tactic:
by

Goal state after:
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
p : α →₀ M
⊢ p ∈ supported M R ↑p.support

Tactic:
by

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
⊢ (mapRange.addMonoidHom ↑f) (g • single i m) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (single i m)

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
⊢ supported R R s = span R ((fun i ↦ single i 1) '' s)

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
⊢ single a 1 ∈ span R ((fun x ↦ single x 1) '' s) ↔ a ∈ s

Tactic:
by

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:
by

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:
by

Goal state after:
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
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ restrictDom M R s ∘ₗ (supported M R s).subtype = LinearMap.id

Tactic:
by

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

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:
by

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

Tactic:
by

Goal state after:
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
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)).range ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Surjective ⇑(ringHomEndFinsupp ι)

Tactic:
by

Goal state after:
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
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)).range ≤ ⨆ i, supported M R (s i)

Tactic:
rw [range_le_iff_comap, eq_top_iff]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ ⊤ ≤ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ((c • v).sum fun a ↦ ⇑(h a)) = σ c • v.sum fun a ↦ ⇑(h a)

Tactic:
by

Goal state after:
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
δ : Type u_7
s : δ → Set α
⊢ supported M R (⋃ i, s i) = ⨆ i, supported M R (s i)

Tactic:
by

Goal state after:
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
s t : Set α
⊢ supported M R (s ∪ t) = supported M R s ⊔ supported M R t

Tactic:
by

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✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ f (r • m) = r • f m

Tactic:
by

Goal state after:
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
ι : Type u_7
s : ι → Set α
x : α →₀ M
⊢ x ∈ supported M R (⋂ i, s i) ↔ x ∈ ⨅ i, supported M R (s i)

Tactic:
by

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✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMul R M
inst✝¹ : SMulZeroClass R N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
⊢ f (r • m) = r • f m

Tactic:
by

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 : α → M →ₛₗ[σ] N
c : R
f : α →₀ M
⊢ ((c • f).sum fun i ↦ ⇑(F i)) = σ c • f.sum fun i ↦ ⇑(F i)

Tactic:
by

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
⊢ { toFun := fun d ↦ d.sum fun i ↦ ⇑((F + G) i), map_add' := ⋯, map_smul' := ⋯ } =
    { 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' := ⋯ }

Tactic:
by

Goal state after:
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
s t : Set α
⊢ supported M R (s ∩ t) = supported M R s ⊓ supported M R t

Tactic:
by

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
⊢ { toFun := fun d ↦ d.sum fun i ↦ ⇑((F • G) i), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id S) F • { toFun := fun d ↦ d.sum fun i ↦ ⇑(G i), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
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
s t : Set α
h : Disjoint s t
⊢ supported M R s ⊓ supported M R t = ⊥

Tactic:
by

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 : α → M →ₛₗ[σ] N
⊢ (fun F x ↦ F ∘ₛₗ lsingle x) ((fun F ↦ { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ }) F) = F

Tactic:
by

Goal state after:
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
inst✝ : Nontrivial M
s t : Set α
⊢ Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t

Tactic:
by

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 : (α →₀ M) →ₛₗ[σ] N
⊢ (fun F ↦ { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ }) ((fun F x ↦ F ∘ₛₗ lsingle x) F) = F

Tactic:
by

Goal state after:
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
s t : Set α
h : Codisjoint s t
⊢ ⊤ ≤ supported M R s ⊔ supported M R t

Tactic:
← supported_union,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Codisjoint s t
⊢ ⊤ ≤ supported M R (s ∪ t)
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:
by

Goal state after:
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
s t : Set α
h : Codisjoint s t
⊢ Codisjoint (supported M R s) (supported M R t)

Tactic:
by

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
X : Type u_9
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
⊢ ∀ (m : S) (x : X → M), (lift M R X).toFun (m • x) = (RingHom.id S) m • (lift M R X).toFun x

Tactic:
by

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
α₁ : Type u_9
α₂ : Type u_10
e : α₁ ≃ α₂
⊢ ∀ (c : R) (x : α₁ →₀ M), (Finsupp.domCongr e) (c • x) = c • (Finsupp.domCongr e) x

Tactic:
by

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

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α₁ : Type u_9
α₂ : Type u_10
e : α₁ ≃ α₂
i : α₁
m : M
⊢ (Finsupp.domLCongr e) (single i m) = single (e i) m

Tactic:
by

Goal state after:
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
i : ι
m : M
⊢ (lcongr e₁ e₂) (single i m) = single (e₁ i) (e₂ m)

Tactic:
by

Goal state after:
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
inst✝ : Nontrivial M
s t : Set α
h : supported M R s ⊔ supported M R t = ⊤
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
← supported_union,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : supported M R (s ∪ t) = ⊤
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t
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
k : κ
n : N
⊢ (lcongr e₁ e₂).symm (single k n) = single (e₁.symm k) (e₂.symm n)

Tactic:
by

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

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : SMulCommClass R R S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
i : ι
n : ↥N
⊢ (mulLeftMap N m) (single i n) = ↑(m i) * ↑n

Tactic:
by

Goal state after:
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
inst✝ : Nontrivial M
s t : Set α
⊢ Codisjoint (supported M R s) (supported M R t) ↔ Codisjoint s t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : SMulCommClass R R S
inst✝ : IsScalarTower R S S
M N : Submodule R S
ι : Type u_5
n : ι → ↥N
i : ι
m : ↥M
⊢ (M.mulRightMap n) (single i m) = ↑m * ↑(n i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
by
  ext i n; simp [(hc i n).eq]

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down

Tactic:
by

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
s : Finset (PLift α)
hs : mulSupport (f ∘ PLift.down) ⊆ ↑s
x : PLift α
hx : x ∈ ⋯.toFinset
⊢ x ∈ s

Tactic:
by

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
x : PLift α
h : x ∈ mulSupport fun x ↦ (fun x ↦ 1) x.down
⊢ x ∈ ↑∅

Tactic:
by

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
⊢ ∏ᶠ (x : α), 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
s : Set α
⊢ ↥(supported M R s) ≃ₗ[R] ↑s →₀ M

Tactic:
by

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
by

Goal state after:
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
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ↑s →₀ M
⊢ ↑((supportedEquivFinsupp s).symm f) = f.extendDomain

Tactic:
by

Goal state after:
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
s : Set α
i : ↑s
a : M
⊢ ↑((supportedEquivFinsupp s).symm (single i a)) = single (↑i) a

Tactic:
by

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}

Tactic:
by

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
by

Goal state after:
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
α' : Type u_7
f : α → α'
s : Set α'
⊢ supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
⊢ ∏ᶠ (i : p), f i = if h : p then f h else 1

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
by

Goal state after: