awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
l : M →₀ R
hl : Membership.mem (γ := Submodule R (M →₀ R)) (supported R R s) l
⊢ ∃ (f : M → R) (t : Finset M),
    (↑t : Set M) ⊆ _root_.id '' s ∧
      Function.support f ⊆ (↑t : Set M) ∧
        Eq (α := M) (∑ a ∈ t, f a • a : M) ((linearCombination R _root_.id : (a : M →₀ R) → M) l : M)

Tactic:
exact ⟨l, l.support, by simpa [linearCombination, Finsupp.sum] using hl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : M → R
t : Finset M
hts : (↑t : Set M) ⊆ s
⊢ Membership.mem (γ := Submodule R M) (span R s) (∑ a ∈ t, n a • a)

Tactic:
sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hts hx

Premises used: Submodule.span, Submodule.subset_span, sum_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : M → R
t : Finset M
hts : (↑t : Set M) ⊆ s
⊢ Membership.mem (γ := Submodule R M) (span R s) (∑ a ∈ t, n a • a)

Tactic:
exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hts hx

Premises used: Submodule.span, Submodule.subset_span, sum_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
x : M
rw :
  (∃ (f : M → R) (t : Finset M),
      (↑t : Set M) ⊆ (↑s : Set M) ∧ Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = x) →
    ∃ (f : M → R), Function.support f ⊆ (↑s : Set M) ∧ ∑ a ∈ s, f a • a = x
⊢ Membership.mem (γ := Submodule R M) (span R (↑s : Set M)) x →
    ∃ (f : M → R), Function.support f ⊆ (↑s : Set M) ∧ ∑ a ∈ s, f a • a = x

Tactic:
rw [mem_span_iff_exists_finset_subset]

Premises used: Submodule.mem_span_iff_exists_finset_subset
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
f : M → R
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
⊢ ∃ (f_1 : M → R), Function.support f_1 ⊆ (↑s : Set M) ∧ Eq (α := M) (∑ a ∈ s, f_1 a • a) (∑ a ∈ t, f a • a)

Tactic:
⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩

Premises used: HasSubset.Subset.trans, Finset.sum_subset, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
f : M → R
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
refine : ∀ x ∈ s, x ∉ t → f x • x = 0
⊢ ∃ (f_1 : M → R), Function.support f_1 ⊆ (↑s : Set M) ∧ Eq (α := M) (∑ a ∈ s, f_1 a • a) (∑ a ∈ t, f a • a)

Tactic:
refine ⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
f : M → R
t : Finset M
hts : (↑t : Set M) ⊆ (↑s : Set M)
hf : Function.support f ⊆ (↑t : Set M)
⊢ ∀ x ∈ s, x ∉ t → f x • x = 0

Tactic:
simp +contextual [Function.support_subset_iff'.1 hf]

Premises used: Iff.mp, Function.support_subset_iff'
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
f : M → R
⊢ Membership.mem (γ := Submodule R M) (span R (↑s : Set M)) (∑ a ∈ s, f a • a)

Tactic:
sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hx

Premises used: SetLike.coe, Submodule.span, Submodule.subset_span, sum_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
f : M → R
⊢ Membership.mem (γ := Submodule R M) (span R (↑s : Set M)) (∑ a ∈ s, f a • a)

Tactic:
exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hx

Premises used: SetLike.coe, Submodule.span, Submodule.subset_span, sum_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
inst_3 : Fintype (↑s : Type u_2)
x : M
rw :
  Membership.mem (γ := Submodule R M)
    (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x
| Membership.mem (γ := Submodule R M) (span R s) x

Tactic:
rw [← Subtype.range_val (s := s)]

Premises used: Subtype.range_val
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
inst_3 : Fintype (↑s : Type u_2)
x : M
conv_lhs :
  Membership.mem (γ := Submodule R M)
      (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (f : (↑s : Type u_2) → R), ∑ a : (↑s : Type u_2), f a • (↑a : M) = x
⊢ Membership.mem (γ := Submodule R M) (span R s) x ↔
    ∃ (f : (↑s : Type u_2) → R), ∑ a : (↑s : Type u_2), f a • (↑a : M) = x

Tactic:
conv_lhs => rw [← Subtype.range_val (s := s)]

Premises used: Subtype.range_val
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
inst_3 : Fintype (↑s : Type u_2)
x : M
⊢ Membership.mem (γ := Submodule R M)
      (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (f : (↑s : Type u_2) → R), ∑ a : (↑s : Type u_2), f a • (↑a : M) = x

Tactic:
mem_span_range_iff_exists_fun _

Premises used: Submodule.mem_span_range_iff_exists_fun
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
inst_3 : Fintype (↑s : Type u_2)
x : M
⊢ Membership.mem (γ := Submodule R M)
      (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x ↔
    ∃ (f : (↑s : Type u_2) → R), ∑ a : (↑s : Type u_2), f a • (↑a : M) = x

Tactic:
exact mem_span_range_iff_exists_fun _

Premises used: Submodule.mem_span_range_iff_exists_fun
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
x : M
⊢ Membership.mem (γ := Submodule R M) (span R (↑s : Set M)) x ↔ ∃ (f : ↥s → R), ∑ a : ↥s, f a • (↑a : M) = x

Tactic:
mem_span_iff_of_fintype

Premises used: Submodule.mem_span_iff_of_fintype
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
rw : Membership.mem (γ := Submodule R M) (span R (_root_.id '' s)) m
| Membership.mem (γ := Submodule R M) (span R s) m

Tactic:
rw [← Set.image_id s]

Premises used: Set.image_id
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
conv_lhs :
  Membership.mem (γ := Submodule R M) (span R (_root_.id '' s)) m ↔
    ∃ (c : M →₀ R), (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : R) ↦ r • mi) = m
⊢ Membership.mem (γ := Submodule R M) (span R s) m ↔
    ∃ (c : M →₀ R), (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : R) ↦ r • mi) = m

Tactic:
conv_lhs => rw [← Set.image_id s]

Premises used: Set.image_id
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
⊢ Membership.mem (γ := Submodule R M) (span R (_root_.id '' s)) m ↔
    ∃ (c : M →₀ R), (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : R) ↦ r • mi) = m

Tactic:
Finsupp.mem_span_image_iff_linearCombination R (v := _root_.id (α := M))

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, setOf, Finsupp.sum, Set.Subset, Finsupp.mem_span_image_iff_linearCombination, Finset.sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
⊢ Membership.mem (γ := Submodule R M) (span R (_root_.id '' s)) m ↔
    ∃ (c : M →₀ R), (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : R) ↦ r • mi) = m

Tactic:
exact Finsupp.mem_span_image_iff_linearCombination R (v := _root_.id (α := M))

Premises used: Finsupp.mem_span_image_iff_linearCombination
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
⊢ Membership.mem (γ := Submodule R M) (span R s) m ↔
    ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
refine_1 :
  ∀ (h : Membership.mem (γ := Submodule R M) (span R s) m),
    ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m
refine_2 :
  (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) →
    Membership.mem (γ := Submodule R M) (span R s) m
⊢ Membership.mem (γ := Submodule R M) (span R s) m ↔
    ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
s : Set M
h : Membership.mem (γ := Submodule R M) (span R s) m
refine_1 :
  ∀ (c : M →₀ R) (cs : (↑c.support : Set M) ⊆ s)
    (h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)),
    ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)),
      Eq (α := M) (∑ i : Fin n, f i • (↑(g i) : M)) (c.sum fun (mi : M) (r : R) ↦ r • mi)
⊢ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m

Tactic:
rcases mem_span_set.1 h with ⟨c, cs, rfl⟩

Premises used: Submodule.mem_span_set, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
refine_1 :
  ∀ (A : ↥c.support ≃ Fin c.support.card),
    ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)),
      Eq (α := M) (∑ i : Fin n, f i • (↑(g i) : M)) (c.sum fun (mi : M) (r : R) ↦ r • mi)
⊢ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)),
    Eq (α := M) (∑ i : Fin n, f i • (↑(g i) : M)) (c.sum fun (mi : M) (r : R) ↦ r • mi)

Tactic:
have A : c.support ≃ Fin c.support.card := Finset.equivFin _
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
⊢ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)),
    Eq (α := M) (∑ i : Fin n, f i • (↑(g i) : M)) (c.sum fun (mi : M) (r : R) ↦ r • mi)

Tactic:
⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro, Equiv.symm, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
refine_1 :
  Eq (α := M)
    (∑ i : Fin c.support.card,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((fun (i : Fin c.support.card) ↦
            ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
          i)
        (↑((fun (i : Fin c.support.card) ↦
                Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) ⋯)
              i) :
          M))
    (c.sum fun (mi : M) (r : R) ↦ r • mi)
⊢ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)),
    Eq (α := M) (∑ i : Fin n, f i • (↑(g i) : M)) (c.sum fun (mi : M) (r : R) ↦ r • mi)

Tactic:
refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
refine_1 :
  Eq.{u_2 + 1} (α := M)
    (∑ i : Fin c.support.card,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((fun (i : Fin c.support.card) ↦
            ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
          i)
        (↑((fun (i : Fin c.support.card) ↦
                Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) ⋯)
              i) :
          M))
    (∑ i : ↥c.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((c : (a : M) → R) (↑i : M) : R) (↑i : M))
⊢ Eq (α := M)
    (∑ i : Fin c.support.card,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((fun (i : Fin c.support.card) ↦
            ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
          i)
        (↑((fun (i : Fin c.support.card) ↦
                Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) ⋯)
              i) :
          M))
    (c.sum fun (mi : M) (r : R) ↦ r • mi)

Tactic:
rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]

Premises used: Finsupp.sum, Finsupp.support, Finset.sum_coe_sort
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : Fin c.support.card,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((fun (i : Fin c.support.card) ↦
            ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
          i)
        (↑((fun (i : Fin c.support.card) ↦
                Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) ⋯)
              i) :
          M))
    (∑ i : ↥c.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((c : (a : M) → R) (↑i : M) : R) (↑i : M))

Tactic:
Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)

Premises used: HSMul.hSMul, Equiv.symm, Fintype.sum_equiv, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
c : M →₀ R
cs : (↑c.support : Set M) ⊆ s
h : Membership.mem (γ := Submodule R M) (span R s) (c.sum fun (mi : M) (r : R) ↦ r • mi)
A : ↥c.support ≃ Fin c.support.card
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : Fin c.support.card,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
        ((fun (i : Fin c.support.card) ↦
            ((c : (a : M) → R) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) : R))
          i)
        (↑((fun (i : Fin c.support.card) ↦
                Subtype.mk (p := fun (x : M) ↦ x ∈ s) (↑((A.symm : (a : Fin c.support.card) → ↥c.support) i) : M) ⋯)
              i) :
          M))
    (∑ i : ↥c.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((c : (a : M) → R) (↑i : M) : R) (↑i : M))

Tactic:
exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)

Premises used: HSMul.hSMul, Equiv.symm, Fintype.sum_equiv, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → (↑s : Type u_2)
⊢ Membership.mem (γ := Submodule R M) (span R s) (∑ i : Fin n, f i • (↑(g i) : M))

Tactic:
Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))

Premises used: Submodule.sum_mem, Submodule.span, Submodule.subset_span, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → (↑s : Type u_2)
⊢ Membership.mem (γ := Submodule R M) (span R s) (∑ i : Fin n, f i • (↑(g i) : M))

Tactic:
exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))

Premises used: Submodule.sum_mem, Submodule.span, Submodule.subset_span, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
h :
  ∀ (m : M),
    m ∈ (↑(span R s) : Set M) ↔
      Membership.mem (γ := Set M)
        (⋃ (n : ℕ),
          (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) ''
            {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
        m
⊢ (↑(span R s) : Set M) =
    ⋃ (n : ℕ),
      (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s}

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
m : M
h :
  (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) ↔
    ∃ (i : ℕ) (x : Fin i → R × M), (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m
⊢ m ∈ (↑(span R s) : Set M) ↔
    Membership.mem (γ := Set M)
      (⋃ (n : ℕ),
        (fun (f : Fin n → R × M) ↦ ∑ i : Fin n, (f i).1 • (f i).2) '' {f : Fin n → R × M | ∀ (i : Fin n), (f i).2 ∈ s})
      m

Tactic:
simp only [SetLike.mem_coe, mem_iUnion, mem_image, mem_setOf_eq, mem_span_set']

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_setOf_eq, SetLike.mem_coe, Submodule.mem_span_set'
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
m : M
⊢ (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) ↔
    ∃ (i : ℕ) (x : Fin i → R × M), (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m

Tactic:
exists_congr (fun n ↦ ⟨?_, ?_⟩)

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
m : M
h :
  ∀ (n : ℕ),
    (∃ (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) →
      ∃ (x : Fin n → R × M), (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m
h₁ :
  ∀ (n : ℕ),
    (∃ (x : Fin n → R × M), (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m) →
      ∃ (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m
⊢ (∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m) ↔
    ∃ (i : ℕ) (x : Fin i → R × M), (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m

Tactic:
refine exists_congr (fun n ↦ ⟨?_, ?_⟩)

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → (↑s : Type u_2)
⊢ ∃ (x : Fin n → R × M),
    (∀ (i : Fin n), (x i).2 ∈ s) ∧
      Eq.{u_2 + 1} (α := M) (∑ i : Fin n, (x i).1 • (x i).2) (∑ i : Fin n, f i • (↑(g i) : M))

Tactic:
⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩

Premises used: Prod.mk, And.intro, Exists.intro, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : ℕ
f : Fin n → R
g : Fin n → (↑s : Type u_2)
⊢ ∃ (x : Fin n → R × M),
    (∀ (i : Fin n), (x i).2 ∈ s) ∧
      Eq.{u_2 + 1} (α := M) (∑ i : Fin n, (x i).1 • (x i).2) (∑ i : Fin n, f i • (↑(g i) : M))

Tactic:
exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : ℕ
f : Fin n → R × M
hf : ∀ (i : Fin n), (f i).2 ∈ s
⊢ ∃ (f_1 : Fin n → R) (g : Fin n → (↑s : Type u_2)),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin n, f_1 i • (↑(g i) : M)) (∑ i : Fin n, (f i).1 • (f i).2)

Tactic:
⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩

Premises used: Prod.fst, Subtype.mk, Exists.intro, Prod.snd, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
n : ℕ
f : Fin n → R × M
hf : ∀ (i : Fin n), (f i).2 ∈ s
⊢ ∃ (f_1 : Fin n → R) (g : Fin n → (↑s : Type u_2)),
    Eq.{u_2 + 1} (α := M) (∑ i : Fin n, f_1 i • (↑(g i) : M)) (∑ i : Fin n, (f i).1 • (f i).2)

Tactic:
exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
refine_1 :
  Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
    ((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
      linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j)))
    LinearMap.id
refine_2 :
  Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
    ((linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
      linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j)))
    LinearMap.id
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R

Tactic:
refine .ofLinear (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Ring R
inst_6 : AddCommGroup M
inst_7 : Module R M
i : ι
c : ι → R
h₀ : c i = 0
refine_1 :
  ∀ (j k : ι),
    Eq.{u_4 + 1} (α := R)
      (((((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                    linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
                  lsingle j :
                (a : R) → ι →₀ R)
              1 :
            (a : ι) → R)
          k :
        R)
      (((LinearMap.id ∘ₗ lsingle j : (a : R) → ι →₀ R) 1 : (a : ι) → R) k : R)
⊢ Eq (α := (ι →₀ R) →ₗ[R] ι →₀ R)
    ((linearCombination R fun (j : ι) ↦ HAdd.hAdd (α := ι →₀ R) (single j 1) (single i (c j))) ∘ₗ
      linearCombination R fun (j : ι) ↦ HSub.hSub (α := ι →₀ R) (single j 1) (single i (c j)))
    LinearMap.id

Tactic:
ext j k