awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ { 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 }
have 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' := sorry,
              map_smul' := sorry }
            (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' := sorry, map_smul' := sorry :
                (α →₀ M) →ₛₗ[σ] N }
              { toFun := fun (d : α →₀ M) ↦ d.sum fun (i : α) ↦ (⇑(G i) : (a : M) → N), map_add' := sorry, map_smul' := sorry :
                (α →₀ M) →ₛₗ[σ] N } ∘ₛₗ
            lsingle x :
          (a : M) → N)
        y :
      N)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ { 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 }
have 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' := sorry,
              map_smul' := sorry }
            (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' := sorry, map_smul' := sorry :
                (α →₀ M) →ₛₗ[σ] N } ∘ₛₗ
            lsingle x :
          (a : M) → N)
        y :
      N)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ (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
have 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' := sorry,
                    map_smul' := sorry } :
                  (α →₀ M) →ₛₗ[σ] N))
              F)
            x :
          (a : M) → N)
        y :
      N)
    ((F x : (a : M) → N) y : N)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ (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
have 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' := sorry,
                    map_smul' := sorry } :
                  (α →₀ 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: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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 : α
⊢ comp (σ₂₃ := σ) ((lsum S : (a : α → M →ₛₗ[σ] N) → (α →₀ M) →ₛₗ[σ] N) f) (lsingle i) = f i
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ (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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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 (α := ι →₀ M) (((lcongr e₁ e₂).symm : (a : κ →₀ N) → ι →₀ M) (single k n) : ι →₀ M)
    (single ((e₁.symm : (a : κ) → ι) k) ((e₂.symm : (a : N) → M) n) : ι →₀ M)
have 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)
Tactic: apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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
⊢ (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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)
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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.{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)
have h : Eq.{u_1 + 1} (α := R)
  (((f : (a : M) → α →₀ R)
          (sum (single x 1) fun (x : α) (r : R) ↦
            r •
              sorry.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: dsimp [splittingOfFinsuppSurjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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.{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)
have h : Eq (α := α →₀ R)
  ((f : (a : M) → α →₀ R)
    (sum (single x 1) fun (x : α) (r : R) ↦
      r • sorry.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))))
  (single x 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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)
      (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)
have h : Eq (α := α →₀ R)
  ((f : (a : M) → α →₀ R)
      (sorry.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) :
    α →₀ R)
  (single x 1 : α →₀ R)
Tactic: rw [sum_single_index, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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)
⊢ 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)
have h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
    (sorry.choose (p := fun (a : M) ↦ Eq (α := α →₀ R) ((f : (a : M) → α →₀ R) a : α →₀ R) (single x 1 : α →₀ R))) =
  0
Tactic: rw [sum_single_index, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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 : α
⊢ 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
have h : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LSum (goal)
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)
⊢ mulLeftMap N m = N.mulRightMap m
have 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)
Tactic: ext i n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α) → R) x : R) (v x) = 0
have rw : HSMul.hSMul.{u_5, u_2, u_2} (α := R) 0 (v x) = 0
Tactic: rw [notMem_support_iff.1 hxg, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α) → R) x : R) (v x) = 0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [notMem_support_iff.1 hxg, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
⊢ (linearCombination R (Pi.single (M := fun (a : α) ↦ M) a c) : (a : α →₀ R) → M) f =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : α) → R) a : R) c
have h₀ : ∀ (b : α),
  Ne.{u_5 + 1} (α := R) ((f : (a : α) → R) b : R) (0 : R) →
    b ≠ a →
      HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) ((f : (a : α) → R) b : R)
          (Pi.single (M := fun (a : α) ↦ M) a c b : M) =
        0
Tactic: rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
h₀ :
  ∀ (b : α),
    Ne.{u_5 + 1} (α := R) ((f : (a : α) → R) b : R) (0 : R) →
      b ≠ a →
        HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) ((f : (a : α) → R) b : R)
            (Pi.single (M := fun (a : α) ↦ M) a c b : M) =
          0
⊢ (linearCombination R (Pi.single (M := fun (a : α) ↦ M) a c) : (a : α →₀ R) → M) f =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : α) → R) a : R) c
have h₁ : Eq.{u_5 + 1} (α := R) ((f : (a : α) → R) a : R) (0 : R) →
  HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) 0 (Pi.single (M := fun (a : α) ↦ M) a c a : M) = 0
Tactic: rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
i : α
h : Ne.{u_5 + 1} (α := R) ((f : (a : α) → R) i : R) (0 : R)
hi : i ≠ a
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) ((f : (a : α) → R) i : R) (Pi.single (M := fun (a : α) ↦ M) a c i : M) =
    0
have rw : HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) ((f : (a : α) → R) i : R) 0 = 0
Tactic: rw [Pi.single_eq_of_ne hi, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
i : α
h : Ne.{u_5 + 1} (α := R) ((f : (a : α) → R) i : R) (0 : R)
hi : i ≠ a
rw : HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) ((f : (a : α) → R) i : R) 0 = 0
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := R) (β := M) ((f : (a : α) → R) i : R) (Pi.single (M := fun (a : α) ↦ M) a c i : M) =
    0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [Pi.single_eq_of_ne hi, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
v : α → M
f : M →ₗ[R] M'
⊢ linearCombination R ((⇑f : (a : M) → M') ∘ v) = f ∘ₗ linearCombination R v
have h : ∀ (a : α),
  Eq.{u_8 + 1} (α := M') ((linearCombination R ((⇑f : (a : M) → M') ∘ v) ∘ₗ lsingle a : (a : R) → M') 1 : M')
    (((f ∘ₗ linearCombination R v) ∘ₗ lsingle a : (a : R) → M') 1 : M')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Unique α
l : α →₀ R
v : α → M
⊢ (linearCombination R v : (a : α →₀ R) → M) l =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α) → R) default : R) (v default)
have rw : Eq.{u_2 + 1} (α := M) ((linearCombination R v : (a : α →₀ R) → M) l : M)
  ((linearCombination R v : (a : α →₀ R) → M) (single default ((l : (a : α) → R) default) : α →₀ R) : M)
Tactic: rw [← linearCombination_single, ← unique_single l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Unique α
l : α →₀ R
v : α → M
rw :
  Eq.{u_2 + 1} (α := M) ((linearCombination R v : (a : α →₀ R) → M) l : M)
    ((linearCombination R v : (a : α →₀ R) → M) (single default ((l : (a : α) → R) default) : α →₀ R) : M)
⊢ (linearCombination R v : (a : α →₀ R) → M) l =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α) → R) default : R) (v default)
have rw₁ : Eq.{u_2 + 1} (α := M) ((linearCombination R v : (a : α →₀ R) → M) l : M)
  ((linearCombination R v : (a : α →₀ R) → M) l : M)
Tactic: rw [← linearCombination_single, ← unique_single l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
h : Function.Surjective v
x : M
⊢ ∃ (a : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) a = x
have obtain : ∀ (y : α) (hy : v y = x), ∃ (a : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) a = x
Tactic: obtain ⟨y, hy⟩ := h x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Eq (α := Submodule R M) (LinearMap.range (linearCombination R v)) (span R (Set.range v))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
x : M
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
have h : Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x →
  Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
x : M
h :
  Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x →
    Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
have h₁ : Membership.mem (γ := Submodule R M) (span R (Set.range v)) x →
  Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (hypothesis)
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
x : M
hx : Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
have hx₁ : ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x
Tactic: rw [LinearMap.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
x : M
hx : ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
have h : ∀ (l : α →₀ R) (hl : (linearCombination R v : (a : α →₀ R) → M) l = x),
  Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
Tactic: rcases hx with ⟨l, hl⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
x : M
l : α →₀ R
hl : (linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
have h : Membership.mem (α := M) (γ := Submodule R M) (span R (Set.range v)) ((linearCombination R v : (a : α →₀ R) → M) l : M)
Tactic: rw [← hl]