awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : α
⊢ (LinearEquiv.symm (lsum S) : (a : (α →₀ M) →ₛₗ[σ] N) → α → M →ₛₗ[σ] N) f x = f ∘ₛₗ lsingle x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_9
f : (X →₀ R) →ₗ[R] M
x : X
⊢ Eq.{u_2 + 1} (α := M) ((AddEquiv.symm (lift M R X) : (a : (X →₀ R) →ₗ[R] M) → X → M) f x : M)
    ((f : (a : X →₀ R) → M) (single x 1) : M)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
X : Type u_9
f : X → M
g : X →₀ R
⊢ Eq.{u_2 + 1} (α := M)
    ((((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) f : (X →₀ R) →ₗ[R] M) : (a : X →₀ R) → M) g : M)
    (g.sum fun (x : X) (r : R) ↦ r • f x : M)

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
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
X : Type u_9
inst_10 : Module S M
inst_11 : SMulCommClass R S M
m : S
x : X → M
dsimp :
  (lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) (m • x) =
    HSMul.hSMul (β := (X →₀ R) →ₗ[R] M) m ((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) x : (X →₀ R) →ₗ[R] M)
⊢ Equiv.toFun (AddEquiv.toEquiv (lift M R X)) (m • x) =
    HSMul.hSMul (α := S) (β := (X →₀ R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) m : S)
      (Equiv.toFun (AddEquiv.toEquiv (lift M R X)) x)

Tactic:
dsimp
-- 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
X : Type u_9
inst_10 : Module S M
inst_11 : SMulCommClass R S M
m : S
x : X → M
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := M) (((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) (m • x) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      ((HSMul.hSMul (β := (X →₀ R) →ₗ[R] M) m ((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) x : (X →₀ R) →ₗ[R] M) ∘ₗ
              lsingle a :
            (a : R) → M)
          1 :
        M)
⊢ (lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) (m • x) =
    HSMul.hSMul (β := (X →₀ R) →ₗ[R] M) m ((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) x : (X →₀ R) →ₗ[R] M)

Tactic:
ext
-- 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
X : Type u_9
inst_10 : Module S M
inst_11 : SMulCommClass R S M
m : S
x : X → M
a : X
⊢ Eq.{u_2 + 1} (α := M) (((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) (m • x) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    ((HSMul.hSMul (β := (X →₀ R) →ₗ[R] M) m ((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) x : (X →₀ R) →ₗ[R] M) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)

Tactic:
simp only [coe_comp, Function.comp_apply, lsingle_apply, lift_apply, Pi.smul_apply,
        sum_single_index, zero_smul, one_smul, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, Finsupp.sum_single_index, Finsupp.lift_apply, one_smul, zero_smul, LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
S : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
X : Type u_9
inst_4 : Module S M
inst_5 : SMulCommClass R S M
f : X → M
x : X →₀ R
⊢ Eq.{u_2 + 1} (α := M)
    ((((llift M R S X : (a : X → M) → (X →₀ R) →ₗ[R] M) f : (X →₀ R) →ₗ[R] M) : (a : X →₀ R) → M) x : M)
    ((((lift M R X : (a : X → M) → (X →₀ R) →ₗ[R] M) f : (X →₀ R) →ₗ[R] M) : (a : X →₀ R) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
S : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
X : Type u_9
inst_4 : Module S M
inst_5 : SMulCommClass R S M
f : (X →₀ R) →ₗ[R] M
x : X
⊢ Eq.{u_2 + 1} (α := M) ((LinearEquiv.symm (llift M R S X) : (a : (X →₀ R) →ₗ[R] M) → X → M) f x : M)
    ((f : (a : X →₀ R) → M) (single x 1) : M)

Tactic:
rfl

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

Tactic:
simpa only [equivMapDomain_eq_mapDomain, domCongr_apply] using (lmapDomain M R e).map_smul

Premises used: Finsupp.domCongr_apply, Finsupp.lmapDomain, Finsupp.equivMapDomain_eq_mapDomain, LinearMap.map_smul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α₁ : Type u_9
α₂ : Type u_10
e : α₁ ≃ α₂
v : α₁ →₀ M
⊢ Eq (α := α₂ →₀ M) ((Finsupp.domLCongr e : (a : α₁ →₀ M) → α₂ →₀ M) v : α₂ →₀ M)
    ((Finsupp.domCongr e : (a : α₁ →₀ M) → α₂ →₀ M) v : α₂ →₀ M)

Tactic:
rfl

Premises used: Finsupp.equivMapDomain, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (α →₀ M) ≃ₗ[R] α →₀ M) (Finsupp.domLCongr (Equiv.refl α)) (LinearEquiv.refl R (α →₀ M))

Tactic:
LinearEquiv.ext fun _ => equivMapDomain_refl _

Premises used: LinearEquiv.ext, Finsupp.equivMapDomain_refl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α₁ : Type u_9
α₂ : Type u_10
α₃ : Type u_11
f : α₁ ≃ α₂
f₂ : α₂ ≃ α₃
⊢ Eq (α := (α₁ →₀ M) ≃ₗ[R] α₃ →₀ M) (Finsupp.domLCongr f ≪≫ₗ Finsupp.domLCongr f₂) (Finsupp.domLCongr (f.trans f₂))

Tactic:
LinearEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm

Premises used: LinearEquiv.ext, Finsupp.equivMapDomain_trans, Eq.symm
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α₁ : Type u_9
α₂ : Type u_10
f : α₁ ≃ α₂
⊢ Eq (α := (α₂ →₀ M) ≃ₗ[R] α₁ →₀ M) (LinearEquiv.symm (Finsupp.domLCongr f)) (Finsupp.domLCongr f.symm)

Tactic:
LinearEquiv.ext fun _ => rfl

Premises used: LinearEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α₁ : Type u_9
α₂ : Type u_10
e : α₁ ≃ α₂
i : α₁
m : M
⊢ Eq (α := α₂ →₀ M) ((Finsupp.domLCongr e : (a : α₁ →₀ M) → α₂ →₀ M) (single i m) : α₂ →₀ M)
    (single ((e : (a : α₁) → α₂) i) m : α₂ →₀ M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
i : ι
m : M
⊢ Eq (α := κ →₀ N) ((lcongr e₁ e₂ : (a : ι →₀ M) → κ →₀ N) (single i m) : κ →₀ N)
    (single ((e₁ : (a : ι) → κ) i) ((e₂ : (a : M) → N) m) : κ →₀ N)

Tactic:
simp [lcongr]

Premises used: Finsupp.lcongr
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
f : ι →₀ M
k : κ
⊢ Eq.{u_3 + 1} (α := N) ((((lcongr e₁ e₂ : (a : ι →₀ M) → κ →₀ N) f : κ →₀ N) : (a : κ) → N) k : N)
    ((e₂ : (a : M) → N) ((f : (a : ι) → M) ((e₁.symm : (a : κ) → ι) k : ι) : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
k : κ
n : N
⊢ Function.Injective (α := ι →₀ M) (β := κ →₀ N) (⇑(lcongr e₁ e₂) : (a : ι →₀ M) → κ →₀ N)

Tactic:
(lcongr e₁ e₂).injective

Premises used: Finsupp.lcongr, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
k : κ
n : N
apply_fun :
  Eq (α := κ →₀ N)
    ((lcongr e₁ e₂ : (a : ι →₀ M) → κ →₀ N) (((lcongr e₁ e₂).symm : (a : κ →₀ N) → ι →₀ M) (single k n)) : κ →₀ N)
    ((lcongr e₁ e₂ : (a : ι →₀ M) → κ →₀ N) (single ((e₁.symm : (a : κ) → ι) k) ((e₂.symm : (a : N) → M) n)) : κ →₀ N)
⊢ Eq (α := ι →₀ M) (((lcongr e₁ e₂).symm : (a : κ →₀ N) → ι →₀ M) (single k n) : ι →₀ M)
    (single ((e₁.symm : (a : κ) → ι) k) ((e₂.symm : (a : N) → M) n) : ι →₀ M)

Tactic:
apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective

Premises used: Finsupp.lcongr, LinearEquiv.injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
k : κ
n : N
⊢ Eq (α := κ →₀ N)
    ((lcongr e₁ e₂ : (a : ι →₀ M) → κ →₀ N) (((lcongr e₁ e₂).symm : (a : κ →₀ N) → ι →₀ M) (single k n)) : κ →₀ N)
    ((lcongr e₁ e₂ : (a : ι →₀ M) → κ →₀ N) (single ((e₁.symm : (a : κ) → ι) k) ((e₂.symm : (a : N) → M) n)) : κ →₀ N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
h :
  ∀ (x : κ →₀ N) (a : ι),
    Eq.{u_2 + 1} (α := M) (((((lcongr e₁ e₂).symm : (a : κ →₀ N) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
      ((((lcongr e₁.symm e₂.symm : (a : κ →₀ N) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
⊢ (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst_6 : RingHomInvPair σ σ_inv
inst_7 : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
x : κ →₀ N
a : ι
⊢ Eq.{u_2 + 1} (α := M) (((((lcongr e₁ e₂).symm : (a : κ →₀ N) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
    ((((lcongr e₁.symm e₂.symm : (a : κ →₀ N) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
β : Type u_5
inst_3 : Zero β
S : Submodule R M
f : ι →₀ β
g : ι → β → M
h : ∀ (c : ι), Ne.{u_5 + 1} (α := β) ((f : (a : ι) → β) c : β) (0 : β) → g c ((f : (a : ι) → β) c) ∈ S
⊢ f.sum g ∈ S

Tactic:
AddSubmonoidClass.finsuppSum_mem S f g h

Premises used: AddSubmonoidClass.finsuppSum_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
h :
  ∀ (x a : α),
    Eq.{u_1 + 1} (α := R)
      ((((f ∘ₗ f.splittingOfFinsuppSurjective s) ∘ₗ lsingle x : (a : R) → α →₀ R) 1 : (a : α) → R) a : R)
      (((id ∘ₗ lsingle x : (a : R) → α →₀ R) 1 : (a : α) → R) a : R)
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
x a : α
h :
  Eq.{u_1 + 1} (α := R)
    (((f : (a : M) → α →₀ R)
            (sum (single x 1) fun (x : α) (r : R) ↦
              r •
                ⋯.choose (p := fun (a : M) ↦
                  Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) :
          (a : α) → R)
        a :
      R)
    ((single x 1 : (a : α) → R) a : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((f ∘ₗ f.splittingOfFinsuppSurjective s) ∘ₗ lsingle x : (a : R) → α →₀ R) 1 : (a : α) → R) a : R)
    (((id ∘ₗ lsingle x : (a : R) → α →₀ R) 1 : (a : α) → R) a : R)

Tactic:
dsimp [splittingOfFinsuppSurjective]

Premises used: LinearMap.splittingOfFinsuppSurjective
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
x a : α
h :
  Eq (α := α →₀ R)
    ((f : (a : M) → α →₀ R)
      (sum (single x 1) fun (x : α) (r : R) ↦
        r • ⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))))
    (single x 1)
⊢ Eq.{u_1 + 1} (α := R)
    (((f : (a : M) → α →₀ R)
            (sum (single x 1) fun (x : α) (r : R) ↦
              r •
                ⋯.choose (p := fun (a : M) ↦
                  Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) :
          (a : α) → R)
        a :
      R)
    ((single x 1 : (a : α) → R) a : R)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
x a : α
h :
  Eq (α := α →₀ R)
    ((f : (a : M) → α →₀ R)
        (⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) :
      α →₀ R)
    (single x 1 : α →₀ R)
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
      (⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) =
    0
⊢ Eq (α := α →₀ R)
    ((f : (a : M) → α →₀ R)
      (sum (single x 1) fun (x : α) (r : R) ↦
        r • ⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))))
    (single x 1)

Tactic:
rw [sum_single_index, one_smul]

Premises used: Finsupp.sum_single_index, one_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
x a : α
⊢ Eq (α := α →₀ R)
    ((f : (a : M) → α →₀ R)
        (⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) :
      α →₀ R)
    (single x 1 : α →₀ R)

Tactic:
(s (Finsupp.single x 1)).choose_spec

Premises used: Exists.choose_spec, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
x a : α
⊢ Eq (α := α →₀ R)
    ((f : (a : M) → α →₀ R)
        (⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) :
      α →₀ R)
    (single x 1 : α →₀ R)

Tactic:
exact (s (Finsupp.single x 1)).choose_spec

Premises used: Exists.choose_spec, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
x a : α
h h₁ : Eq.{u_2 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
      (⋯.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) =
    0

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
⊢ LeftInverse (α := α →₀ R) (β := M) (⇑f : (a : M) → α →₀ R) (⇑(f.splittingOfFinsuppSurjective s) : (a : α →₀ R) → M)

Tactic:
fun g =>
  LinearMap.congr_fun (splittingOfFinsuppSurjective_splits f s) g

Premises used: Function.LeftInverse, LinearMap.congr_fun, LinearMap.splittingOfFinsuppSurjective_splits
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective (α := M) (β := α →₀ R) (⇑f : (a : M) → α →₀ R)
⊢ Injective (α := α →₀ R) (β := M) (⇑(f.splittingOfFinsuppSurjective s) : (a : α →₀ R) → M)

Tactic:
(leftInverse_splittingOfFinsuppSurjective f s).injective

Premises used: Function.LeftInverse.injective, LinearMap.leftInverse_splittingOfFinsuppSurjective
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_4
R₂ : Type u_5
M : Type u_6
M₂ : Type u_7
ι : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
γ : Type u_9
inst_6 : Zero γ
t : ι →₀ γ
g : ι → γ → M →ₛₗ[σ₁₂] M₂
⊢ Eq (α := (a : M) → M₂) (⇑(t.sum g) : (a : M) → M₂) (⇑(t.sum fun (i : ι) (d : γ) ↦ g i d) : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_4
R₂ : Type u_5
M : Type u_6
M₂ : Type u_7
ι : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
γ : Type u_9
inst_6 : Zero γ
t : ι →₀ γ
g : ι → γ → M →ₛₗ[σ₁₂] M₂
b : M
⊢ Eq.{u_7 + 1} (α := M₂) ((t.sum g : (a : M) → M₂) b : M₂) (t.sum fun (i : ι) (d : γ) ↦ (g i d : (a : M) → M₂) b : M₂)

Tactic:
sum_apply _ _ _

Premises used: Finsupp.sum, LinearMap.sum_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
n : Finsupp.{u_5, u_4} ι ↥N
⊢ Eq (α := S) ((mulLeftMap N m : (a : ι →₀ ↥N) → S) n : S) (n.sum fun (i : ι) (n : ↥N) ↦ (↑(m i) : S) * (↑n : S) : S)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
i : ι
n : ↥N
⊢ (mulLeftMap N m : (a : ι →₀ ↥N) → S) (single i n) = (↑(m i) : S) * (↑n : S)

Tactic:
simp [mulLeftMap]

Premises used: Submodule.mulLeftMap
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : IsScalarTower R S S
M N : Submodule R S
ι : Type u_5
n : ι → ↥N
m : Finsupp.{u_5, u_4} ι ↥M
⊢ Eq (α := S) ((M.mulRightMap n : (a : ι →₀ ↥M) → S) m : S) (m.sum fun (i : ι) (m : ↥M) ↦ (↑m : S) * (↑(n i) : S) : S)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MulOpposite.unop, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : IsScalarTower R S S
M N : Submodule R S
ι : Type u_5
n : ι → ↥N
i : ι
m : ↥M
⊢ (M.mulRightMap n : (a : ι →₀ ↥M) → S) (single i m) = (↑m : S) * (↑(n i) : S)

Tactic:
simp [mulRightMap]

Premises used: Submodule.mulRightMap
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : IsScalarTower R S S
inst_5 : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute (↑(m i) : S) (↑n : S)
h :
  ∀ (i : ι) (n : ↥N),
    Eq (α := S) ((mulLeftMap N m ∘ₗ lsingle i : (a : ↥N) → S) n : S)
      ((N.mulRightMap m ∘ₗ lsingle i : (a : ↥N) → S) n : S)
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
ext i n
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : IsScalarTower R S S
inst_5 : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute (↑(m i) : S) (↑n : S)
i : ι
n : ↥N
⊢ Eq (α := S) ((mulLeftMap N m ∘ₗ lsingle i : (a : ↥N) → S) n : S) ((N.mulRightMap m ∘ₗ lsingle i : (a : ↥N) → S) n : S)

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

Premises used: Commute.eq
-- Module: Mathlib.LinearAlgebra.Finsupp.LSum
Goal:
R : Type u_1
inst : Semiring R
S : Type u_5
inst_1 : CommSemiring S
inst_2 : Module R S
inst_3 : SMulCommClass R R S
inst_4 : SMulCommClass R S S
inst_5 : IsScalarTower R S S
M N : Submodule R S
ι : Type u_6
m : ι → ↥M
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
mulLeftMap_eq_mulRightMap_of_commute N m fun _ _ ↦ mul_comm _ _

Premises used: Submodule.mulLeftMap_eq_mulRightMap_of_commute, mul_comm, Subtype.val
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
l : α →₀ R
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R v : (a : α →₀ R) → M) l : M) (l.sum fun (i : α) (a : R) ↦ a • v i : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
l : α →₀ R
s : Finset α
hs : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R (↑s : Set α)) l
x : α
h : x ∈ s
hxg : x ∉ l.support
rw : HSMul.hSMul.{u_5, u_2, u_2} (α := R) 0 (v x) = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 0 0
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α) → R) x : R) (v x) = 0

Tactic:
rw [notMem_support_iff.1 hxg, zero_smul]

Premises used: Finsupp.notMem_support_iff, zero_smul, Iff.mp