mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ f.toFinsupp.support ↔ a✝ ∈ f.support

Tactic:
simp

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

Goal state before:
pp: case pos
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
⊢ (mapRange f hf (single i b)) i = (single i (f i b)) i

Tactic:
simp

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

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
η : Type u_7
inst✝³ : Fintype η
ιs✝ : η → Type u_8
inst✝² : Zero α
M : Type u_9
ιs : η → Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : (j : η) × ιs j →₀ M
x✝ : η
a✝ : ιs x✝
⊢ (sigmaFinsuppAddEquivPiFinsupp.toFun (c • f) x✝) a✝ =
    (((RingHom.id R) c • sigmaFinsuppAddEquivPiFinsupp.toFun f) x✝) a✝

Tactic:
simp

Goal state after:
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
a✝ : ι
⊢ a✝ ∈ (erase i f).support ↔ a✝ ∈ f.support.erase i

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : v i = 0
⊢ f i 0 = 1

Tactic:
hf

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
a✝ : i ∈ Finset.univ
hi : v i = 0
⊢ 1 = 1
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
a✝ : Subtype p
⊢ a✝ ∈ (subtypeDomain p f).support ↔ a✝ ∈ Finset.subtype p f.support

Tactic:
simp

Goal state after:
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
a✝ : ι
⊢ a✝ ∈ (-f).support ↔ a✝ ∈ f.support

Tactic:
simp

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

Goal state before:
pp: case refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sx.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

Tactic:
intro i H1 H2
        rw [Finset.mem_inter] at H2
        simp only [Multiset.mem_toFinset] at H1 H2
        convert! map_zero (φ i)
        exact (hy i).resolve_left (mt (And.intro H1) H2)

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f : Π₀ (i : ι), β i
⊢ f.support = f.support ∧ ∀ i ∈ f.support, f i = f i

Tactic:
simp

Goal state after:
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:
by
  ext
  rw [zero_apply, comapDomain_apply, zero_apply]

Goal state after:
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
x✝ : Π₀ (i : ι), β i
i✝ : ι
⊢ ((addMonoidHom fun i ↦ (f i).comp (f₂ i)) x✝) i✝ = (((addMonoidHom f).comp (addMonoidHom f₂)) x✝) i✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i ↦ id) ⋯ x = x

Tactic:
simp

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

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ ∀ (i : ι), id 0 = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i ↦ id) ⋯ x = x

Tactic:
simp

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

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ ∀ (i : ι), id 0 = 0

Tactic:
simp

Goal state after:
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
x✝ : Π₀ (i : ι), β i
i✝ : ι
⊢ ((addEquiv fun i ↦ (f i).trans (f₂ i)) x✝) i✝ = (((addEquiv f).trans (addEquiv f₂)) x✝) i✝

Tactic:
simp

Goal state after:
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 →+ γ
x✝¹ : ι
x✝ : β x✝¹
⊢ ((fun F i ↦ F.comp (singleAddHom β i)) (sumAddHom x) x✝¹) x✝ = (x x✝¹) x✝

Tactic:
simp

Goal state after:
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) →+ γ
x✝¹ : ι
x✝ : β x✝¹
⊢ ((sumAddHom ((fun F i ↦ F.comp (singleAddHom β i)) ψ)).comp (singleAddHom β x✝¹)) x✝ =
    (ψ.comp (singleAddHom β x✝¹)) x✝

Tactic:
simp

Goal state after:
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 →+ γ
x✝¹ : ι
x✝ : β x✝¹
⊢ ((sumAddHom (F + G)).comp (singleAddHom β x✝¹)) x✝ = ((sumAddHom F + sumAddHom G).comp (singleAddHom β x✝¹)) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
f : (i : ι) → β i →+ γ
i : ι
x : β i
⊢ (liftAddHom f) (single i x) = (f i) x

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
f : (i : ι) → β i →+ γ
i : ι
⊢ (liftAddHom f).comp (singleAddHom β i) = f i

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
s : Set (Dual R M)
x : M
φ : M →ₗ[R] R
⊢ x ∈ φ.ker ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)

Tactic:
simp

Goal state after:
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 : ι
x✝ : M i
⊢ (lapply i ∘ₗ lsingle i) x✝ = LinearMap.id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case ha
ι : 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
c : R
f✝ : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
a✝¹ : f a = 0
a✝ : b ≠ 0
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
    (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
      c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)

Tactic:
hf

Goal state after:
case ha
ι : 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
c : R
f✝ : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
a✝¹ : f a = 0
a✝ : b ≠ 0
hf : (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
    c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)
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 : ι
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✝

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

Goal state after:
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
i : ι
x✝ : M i
⊢ ((fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ })
          ((fun F i ↦ F ∘ₗ lsingle i) F) ∘ₗ
        lsingle i)
      x✝ =
    (F ∘ₗ lsingle i) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
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
i : ι
x : M i
⊢ ((lsum S) F) (single i x) = (F i) x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁶ : Semiring R
β : ι → Type u_7
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i →ₗ[R] β₂ i
f₂ : (i : ι) → β i →ₗ[R] β₁ i
⊢ ∀ (i : ι), ((fun x ↦ (f i) x) ∘ fun x ↦ (f₂ i) x) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β₁ i)
inst✝¹ : (i : ι) → Module R (β₂ i)
inst✝ : DecidableEq ι
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
i : ι
⊢ (h i) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁶ : Semiring R
β : ι → Type u_7
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β i ≃ₗ[R] β₁ i
f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i
⊢ ∀ (i : ι), ((fun x ↦ (f₂ i) x) ∘ fun x ↦ (f i) x) 0 = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f 0 ∈ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
x✝ : ∃ f, (f.sum fun x xi ↦ ↑xi) = x
f : Π₀ (i : ι), ↥(p i)
hf : (f.sum fun x xi ↦ ↑xi) = x
⊢ ∀ (a : ι), a ∈ f.support ↔ ↑(f a) ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
x✝ : ∃ f, (f.sum fun x xi ↦ ↑xi) = x
f : Π₀ (i : ι), ↥(p i)
hf : (f.sum fun x xi ↦ ↑xi) = x
⊢ ∀ (i : ι), { support := f.support, toFun := fun i ↦ ↑(f i), mem_support_toFun := ⋯ } i ∈ p i

Tactic:
simp

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

Goal state before:
pp: case inl.fst
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inl val✝)) 1).1 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inl val✝))
        1).1

Tactic:
simp

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

Goal state before:
pp: case inl.snd
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inl val✝)) 1).2 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inl val✝))
        1).2

Tactic:
simp

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

Goal state before:
pp: case inr.fst
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι'
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inr val✝)) 1).1 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inr val✝))
        1).1

Tactic:
simp

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

Goal state before:
pp: case inr.snd
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι'
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inr val✝)) 1).2 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inr val✝))
        1).2

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)

Goal state after:
ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep (⇑AddSubmonoid.toNatSubmodule ∘ p)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
a✝ : ι
⊢ ((((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
          (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R)) ∘ₗ
        Finsupp.lsingle a✝)
      1 =
    (Finsupp.linearCombination R v ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝² x✝¹ : M
x✝ : Nₗ
⊢ (↑R g ∘ₗ f (x✝² + x✝¹)) x✝ = (↑R g ∘ₗ f x✝² + ↑R g ∘ₗ f x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝² : A
x✝¹ : M
x✝ : Nₗ
⊢ (↑R g ∘ₗ f (x✝² • x✝¹)) x✝ = ((RingHom.id A) x✝² • ↑R g ∘ₗ f x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_2
inst✝⁸ : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid Nₗ
inst✝⁵ : AddCommMonoid Pₗ
inst✝⁴ : AddCommMonoid Qₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ ≃ₗ[R] Qₗ
hf : Surjective ⇑f
⊢ ↑g ∘ₗ ↑g.symm = id

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_2
inst✝¹⁶ : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring R₃
inst✝¹³ : CommSemiring R₄
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : AddCommMonoid Q
inst✝⁸ : Module R M
inst✝⁷ : Module R₂ N
inst✝⁶ : Module R₃ P
inst✝⁵ : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝⁴ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝³ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝² : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝ : RingHomInvPair σ₄₃ σ₃₄
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P ≃ₛₗ[σ₃₄] Q
hf : Surjective ⇑f
⊢ ↑g ∘ₛₗ ↑g.symm = id

Tactic:
simp

Goal state after: