awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
R : Type u_3
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ ((c • v).sum fun (a : α) ↦ (⇑(h a) : (a : M) → M₂)) =
    HSMul.hSMul (β := M₂) c (v.sum fun (a : α) ↦ (⇑(h a) : (a : M) → M₂))

Tactic:
sum_smul_index_semilinearMap'

Premises used: Finsupp.sum_smul_index_semilinearMap'
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
rw : m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N)
| HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) m : N)

Tactic:
rw [← sum_single m, map_finsuppSum, smul_sum]

Premises used: map_finsuppSum, Finsupp.smul_sum, Finsupp.sum_single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
conv_rhs :
  Eq.{u_12 + 1} (α := N) ((f : (a : ι →₀ M) → N) (r • m) : N)
    (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N) : N)
⊢ (f : (a : ι →₀ M) → N) (r • m) = HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) m : N)

Tactic:
conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]

Premises used: map_finsuppSum, Finsupp.smul_sum, Finsupp.sum_single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
erw :
  Eq.{u_12 + 1} (α := N) (m.sum fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b)))
    (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N))
⊢ Eq.{u_12 + 1} (α := N) ((f : (a : ι →₀ M) → N) (r • m) : N)
    (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N) : N)

Tactic:
erw [← sum_single (r • m), sum_mapRange_index single_zero, map_finsuppSum]

Premises used: map_finsuppSum, HSMul.hSMul, Finsupp.sum_mapRange_index, Finsupp.sum_single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
e_g :
  Eq (α := ι → M → N) (fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b))) fun (a : ι) (b : M) ↦
    HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N)
⊢ Eq.{u_12 + 1} (α := N) (m.sum fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b)))
    (m.sum fun (a : ι) (b : M) ↦ HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
e_g :
  ∀ (i : ι) (m : M),
    (f : (a : ι →₀ M) → N) (single i (r • m)) = HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single i m) : N)
⊢ Eq (α := ι → M → N) (fun (a : ι) (b : M) ↦ (f : (a : ι →₀ M) → N) (single a (r • b))) fun (a : ι) (b : M) ↦
    HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single a b) : N)

Tactic:
ext i m
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m_1 : ι →₀ M
i : ι
m : M
⊢ (f : (a : ι →₀ M) → N) (single i (r • m)) = HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single i m) : N)

Tactic:
(f.comp <| lsingle i).map_smul_of_tower r m

Premises used: LinearMap.comp, LinearMap.map_smul_of_tower, Finsupp.lsingle, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMulZeroClass R M
inst_16 : DistribSMul R N
inst_17 : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m_1 : ι →₀ M
i : ι
m : M
⊢ (f : (a : ι →₀ M) → N) (single i (r • m)) = HSMul.hSMul (β := N) r ((f : (a : ι →₀ M) → N) (single i m) : N)

Tactic:
exact (f.comp <| lsingle i).map_smul_of_tower r m

Premises used: LinearMap.comp, LinearMap.map_smul_of_tower, Finsupp.lsingle
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMul R M
inst_16 : SMulZeroClass R N
inst_17 : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
h :
  ∀ (i : ι),
    Eq.{u_12 + 1} (α := N) ((((f : (a : M) → ι →₀ N) (r • m) : ι →₀ N) : (a : ι) → N) i : N)
      ((HSMul.hSMul (β := ι →₀ N) r ((f : (a : M) → ι →₀ N) m : ι →₀ N) : (a : ι) → N) i : N)
⊢ (f : (a : M) → ι →₀ N) (r • m) = HSMul.hSMul (β := ι →₀ N) r ((f : (a : M) → ι →₀ N) m : ι →₀ N)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M_1 : Type u_2
N_1 : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S_1 : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S_1
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N_1
inst_7 : Module R₂ N_1
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R_1 →+* R₂
σ_inv : R₂ →+* R_1
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst_10 : Semiring S
inst_11 : AddCommMonoid M
inst_12 : AddCommMonoid N
inst_13 : Module S M
inst_14 : Module S N
inst_15 : SMul R M
inst_16 : SMulZeroClass R N
inst_17 : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
i : ι
⊢ Eq.{u_12 + 1} (α := N) ((((f : (a : M) → ι →₀ N) (r • m) : ι →₀ N) : (a : ι) → N) i : N)
    ((HSMul.hSMul (β := ι →₀ N) r ((f : (a : M) → ι →₀ N) m : ι →₀ N) : (a : ι) → N) i : N)

Tactic:
apply ((lapply i).comp f).map_smul_of_tower

Premises used: LinearMap.comp, LinearMap.map_smul_of_tower, Finsupp.lapply
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : α → M →ₛₗ[σ] N
c : R
f : α →₀ M
⊢ ((c • f).sum fun (i : α) ↦ (⇑(F i) : (a : M) → N)) =
    HSMul.hSMul.{u_6, u_3, u_3} (α := R₂) (β := N) ((σ : (a : R) → R₂) c : R₂)
      (f.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N))

Tactic:
simp [sum_smul_index', smul_sum]

Premises used: Finsupp.sum_smul_index', Finsupp.smul_sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F G : α → M →ₛₗ[σ] N
h :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((comp (σ₂₃ := σ)
              { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑((F + G) i) : (a : M) → N), map_add' := ⋯,
                map_smul' := ⋯ }
              (lsingle x) :
            (a : M) → N)
          y :
        N)
      ((HAdd.hAdd (α := (α →₀ M) →ₛₗ[σ] N)
                { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯,
                  map_smul' := ⋯ : (α →₀ M) →ₛₗ[σ] N }
                { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := ⋯,
                  map_smul' := ⋯ : (α →₀ M) →ₛₗ[σ] N } ∘ₛₗ
              lsingle x :
            (a : M) → N)
          y :
        N)
⊢ { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑((F + G) i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := (α →₀ M) →ₛₗ[σ] N)
      { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ :
        (α →₀ M) →ₛₗ[σ] N }
      { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ :
        (α →₀ M) →ₛₗ[σ] N }

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F G : α → M →ₛₗ[σ] N
x : α
y : M
⊢ Eq.{u_3 + 1} (α := N)
    ((comp (σ₂₃ := σ)
            { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑((F + G) i) : (a : M) → N), map_add' := ⋯,
              map_smul' := ⋯ }
            (lsingle x) :
          (a : M) → N)
        y :
      N)
    ((HAdd.hAdd (α := (α →₀ M) →ₛₗ[σ] N)
              { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ :
                (α →₀ M) →ₛₗ[σ] N }
              { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ :
                (α →₀ M) →ₛₗ[σ] N } ∘ₛₗ
            lsingle x :
          (a : M) → N)
        y :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : S
G : α → M →ₛₗ[σ] N
h :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((comp (σ₂₃ := σ)
              { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑((F • G) i) : (a : M) → N), map_add' := ⋯,
                map_smul' := ⋯ }
              (lsingle x) :
            (a : M) → N)
          y :
        N)
      ((HSMul.hSMul (α := S) (β := (α →₀ M) →ₛₗ[σ] N) ((RingHom.id S : (a : S) → S) F : S)
                { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := ⋯,
                  map_smul' := ⋯ : (α →₀ M) →ₛₗ[σ] N } ∘ₛₗ
              lsingle x :
            (a : M) → N)
          y :
        N)
⊢ { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑((F • G) i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := S) (β := (α →₀ M) →ₛₗ[σ] N) ((RingHom.id S : (a : S) → S) F : S)
      { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ :
        (α →₀ M) →ₛₗ[σ] N }

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : S
G : α → M →ₛₗ[σ] N
x : α
y : M
⊢ Eq.{u_3 + 1} (α := N)
    ((comp (σ₂₃ := σ)
            { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑((F • G) i) : (a : M) → N), map_add' := ⋯,
              map_smul' := ⋯ }
            (lsingle x) :
          (a : M) → N)
        y :
      N)
    ((HSMul.hSMul (α := S) (β := (α →₀ M) →ₛₗ[σ] N) ((RingHom.id S : (a : S) → S) F : S)
              { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ :
                (α →₀ M) →ₛₗ[σ] N } ∘ₛₗ
            lsingle x :
          (a : M) → N)
        y :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : α → M →ₛₗ[σ] N
h :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      (((fun (F : (α →₀ M) →ₛₗ[σ] N) (x : α) ↦ F ∘ₛₗ lsingle x)
              ((fun (F : α → M →ₛₗ[σ] N) ↦
                  ({ toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯,
                      map_smul' := ⋯ } :
                    (α →₀ M) →ₛₗ[σ] N))
                F)
              x :
            (a : M) → N)
          y :
        N)
      ((F x : (a : M) → N) y : N)
⊢ (fun (F : (α →₀ M) →ₛₗ[σ] N) (x : α) ↦ F ∘ₛₗ lsingle x)
      ((fun (F : α → M →ₛₗ[σ] N) ↦
          ({ toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ } :
            (α →₀ M) →ₛₗ[σ] N))
        F) =
    F

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : α → M →ₛₗ[σ] N
x : α
y : M
⊢ Eq.{u_3 + 1} (α := N)
    (((fun (F : (α →₀ M) →ₛₗ[σ] N) (x : α) ↦ F ∘ₛₗ lsingle x)
            ((fun (F : α → M →ₛₗ[σ] N) ↦
                ({ toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯,
                    map_smul' := ⋯ } :
                  (α →₀ M) →ₛₗ[σ] N))
              F)
            x :
          (a : M) → N)
        y :
      N)
    ((F x : (a : M) → N) y : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : (α →₀ M) →ₛₗ[σ] N
h :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((comp (σ₂₃ := σ)
              ((fun (F : α → M →ₛₗ[σ] N) ↦
                  ({ toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯,
                      map_smul' := ⋯ } :
                    (α →₀ M) →ₛₗ[σ] N))
                ((fun (F : (α →₀ M) →ₛₗ[σ] N) (x : α) ↦ F ∘ₛₗ lsingle x) F))
              (lsingle x) :
            (a : M) → N)
          y :
        N)
      ((F ∘ₛₗ lsingle x : (a : M) → N) y : N)
⊢ (fun (F : α → M →ₛₗ[σ] N) ↦
        ({ toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯, map_smul' := ⋯ } :
          (α →₀ M) →ₛₗ[σ] N))
      ((fun (F : (α →₀ M) →ₛₗ[σ] N) (x : α) ↦ F ∘ₛₗ lsingle x) F) =
    F

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_10 : Module S N
inst_11 : SMulCommClass R₂ S N
F : (α →₀ M) →ₛₗ[σ] N
x : α
y : M
⊢ Eq.{u_3 + 1} (α := N)
    ((comp (σ₂₃ := σ)
            ((fun (F : α → M →ₛₗ[σ] N) ↦
                ({ toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(F i) : (a : M) → N), map_add' := ⋯,
                    map_smul' := ⋯ } :
                  (α →₀ M) →ₛₗ[σ] N))
              ((fun (F : (α →₀ M) →ₛₗ[σ] N) (x : α) ↦ F ∘ₛₗ lsingle x) F))
            (lsingle x) :
          (a : M) → N)
        y :
      N)
    ((F ∘ₛₗ lsingle x : (a : M) → N) y : N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
σ : R →+* R₂
inst_7 : Module S N
inst_8 : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
⊢ Eq (α := (a : α →₀ M) → N)
    (⇑((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f : (α →₀ M) →ₛₗ[σ] N) : (a : α →₀ M) → N) fun (d : α →₀ M) ↦
    d.sum fun (i : α) ↦ (⇑(f i) : (a : M) → N)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
σ : R →+* R₂
inst_7 : Module S N
inst_8 : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
l : α →₀ M
⊢ Eq.{u_3 + 1} (α := N)
    ((((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f : (α →₀ M) →ₛₗ[σ] N) : (a : α →₀ M) → N) l : N)
    (l.sum fun (b : α) ↦ (⇑(f b) : (a : M) → N) : N)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
σ : R →+* R₂
inst_7 : Module S N
inst_8 : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
i : α
m : M
⊢ Eq.{u_3 + 1} (α := N)
    ((((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f : (α →₀ M) →ₛₗ[σ] N) : (a : α →₀ M) → N) (single i m) : N)
    ((f i : (a : M) → N) m : N)

Tactic:
Finsupp.sum_single_index (f i).map_zero

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum_single_index, Finsupp.sum, LinearMap.map_zero, Finset.sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
σ : R →+* R₂
inst_7 : Module S N
inst_8 : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
i : α
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := N)
      ((comp (σ₂₃ := σ) ((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f) (lsingle i) : (a : M) → N) x : N)
      ((f i : (a : M) → N) x : N)
⊢ comp (σ₂₃ := σ) ((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f) (lsingle i) = f i

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : 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_1 : Semiring R₂
inst_2 : Semiring S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
σ : R →+* R₂
inst_7 : Module S N
inst_8 : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
i : α
x : M
⊢ Eq.{u_3 + 1} (α := N)
    ((comp (σ₂₃ := σ) ((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f) (lsingle i) : (a : M) → N) x : N)
    ((f i : (a : M) → N) x : N)

Tactic:
simp