awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : M
rw :
  Membership.mem (γ := Submodule R M) (span R (Set.range v)) x ↔
    ∃ (x_1 : α →₀ R),
      ∑ i : α,
          HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((Finsupp.equivFunOnFinite : (a : α →₀ R) → α → R) x_1 i : R) (v i) =
        x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x ↔ ∃ (c : α → R), ∑ i : α, c i • v i = x

Tactic:
rw [Finsupp.equivFunOnFinite.surjective.exists]

Premises used: Function.Surjective.exists, Finsupp.equivFunOnFinite, Equiv.surjective
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : M
simp :
  (∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) ↦ a • v i) = x) ↔
    ∃ (x_1 : α →₀ R), ∑ x : α, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((x_1 : (a : α) → R) x : R) (v x) = x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x ↔
    ∃ (x_1 : α →₀ R),
      ∑ i : α,
          HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((Finsupp.equivFunOnFinite : (a : α →₀ R) → α → R) x_1 i : R) (v i) =
        x

Tactic:
simp only [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply]

Premises used: Finsupp.equivFunOnFinite_apply, Finsupp.mem_span_range_iff_exists_finsupp
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : M
⊢ (∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) ↦ a • v i) = x) ↔
    ∃ (x_1 : α →₀ R), ∑ x : α, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((x_1 : (a : α) → R) x : R) (v x) = x

Tactic:
exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _

Premises used: Finsupp.sum_fintype, Eq.congr_left, exists_congr, zero_smul, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
x : M
⊢ (∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) ↦ a • v i) = x) ↔
    ∃ (x_1 : α →₀ R), ∑ x : α, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((x_1 : (a : α) → R) x : R) (v x) = x

Tactic:
exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _

Premises used: Finsupp.sum_fintype, Eq.congr_left, exists_congr, zero_smul, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
simp_rw :
  LE.le (α := Submodule R M) ⊤ (span R (Set.range v)) ↔
    ∀ (x : M), Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range v)) ↔ ∀ (x : M), ∃ (c : α → R), ∑ i : α, c i • v i = x

Tactic:
simp_rw [← mem_span_range_iff_exists_fun]

Premises used: Submodule.mem_span_range_iff_exists_fun
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range v)) ↔
    ∀ (x : M), Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
⟨fun h x => h trivial, fun h x _ => h x⟩

Premises used: trivial, Iff.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Fintype α
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : α → M
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range v)) ↔
    ∀ (x : M), Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
exact ⟨fun h x => h trivial, fun h x _ => h x⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) x ↔
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x

Tactic:
⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩

Premises used: Membership.mem, Iff.intro, Submodule.span, Set.image, _private.0.Submodule.mem_span_image_iff_exists_fun.match_1
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
refine_1 :
  ∀ (h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x
refine_2 :
  (∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x) →
    ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s) (c : ↥t → R) (hx : ∑ i : ↥t, c i • v (↑i : α) = x),
      Membership.mem (γ := Submodule R M) (span R (v '' s)) x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) x ↔
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x
refine_1 :
  ∀ (l : α →₀ R) (hl : Membership.mem (γ := Submodule R (α →₀ R)) (Finsupp.supported R R s) l)
    (hx : (Finsupp.linearCombination R v : (a : α →₀ R) → M) l = x),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x

Tactic:
obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h

Premises used: Iff.mp, Finsupp.mem_span_image_iff_linearCombination
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (Finsupp.supported R R s) l
hx : (Finsupp.linearCombination R v : (a : α →₀ R) → M) l = x
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x

Tactic:
⟨l.support, hl, l ∘ (↑), ?_⟩

Premises used: Finsupp.support, Function.comp, And.intro, Exists.intro, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (Finsupp.supported R R s) l
hx : (Finsupp.linearCombination R v : (a : α →₀ R) → M) l = x
refine_1 :
  ∑ i : ↥l.support,
      HSMul.hSMul.{u_3, u_2, u_2} (α := R) (((⇑l : (a : α) → R) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ l.support)) i)
        (v (↑i : α)) =
    x
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x

Tactic:
refine ⟨l.support, hl, l ∘ (↑), ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (Finsupp.supported R R s) l
hx : (Finsupp.linearCombination R v : (a : α →₀ R) → M) l = x
refine_1 :
  Eq.{u_2 + 1} (α := M)
    (∑ i : ↥l.support,
        HSMul.hSMul.{u_3, u_2, u_2} (α := R) (((⇑l : (a : α) → R) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ l.support)) i)
          (v (↑i : α)) :
      M)
    ((Finsupp.linearCombination R v : (a : α →₀ R) → M) l : M)
⊢ ∑ i : ↥l.support,
      HSMul.hSMul.{u_3, u_2, u_2} (α := R) (((⇑l : (a : α) → R) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ l.support)) i)
        (v (↑i : α)) =
    x

Tactic:
rw [← hx]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (Finsupp.supported R R s) l
hx : (Finsupp.linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : ↥l.support,
        HSMul.hSMul.{u_3, u_2, u_2} (α := R) (((⇑l : (a : α) → R) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ l.support)) i)
          (v (↑i : α)) :
      M)
    ((Finsupp.linearCombination R v : (a : α →₀ R) → M) l : M)

Tactic:
l.support.sum_coe_sort fun a ↦ l a • v a

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finsupp.support, HSMul.hSMul, DFunLike.coe, Finset.sum_coe_sort, Finset.sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : Membership.mem (γ := Submodule R M) (span R (v '' s)) x
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (Finsupp.supported R R s) l
hx : (Finsupp.linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : ↥l.support,
        HSMul.hSMul.{u_3, u_2, u_2} (α := R) (((⇑l : (a : α) → R) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ l.support)) i)
          (v (↑i : α)) :
      M)
    ((Finsupp.linearCombination R v : (a : α →₀ R) → M) l : M)

Tactic:
exact l.support.sum_coe_sort fun a ↦ l a • v a

Premises used: Finsupp.support, HSMul.hSMul, DFunLike.coe, Finset.sum_coe_sort
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x
t : Finset α
ht : (↑t : Set α) ⊆ s
c : ↥t → R
hx : ∑ i : ↥t, c i • v (↑i : α) = x
refine_2 : Membership.mem (γ := Submodule R M) (span R (v '' s)) (∑ i : ↥t, c i • v (↑i : α))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) x

Tactic:
rw [← hx]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x
t : Finset α
ht : (↑t : Set α) ⊆ s
c : ↥t → R
hx : ∑ i : ↥t, c i • v (↑i : α) = x
a : ↥t
h_1 : Membership.mem (γ := Finset ↥t) Finset.univ a
⊢ v (↑a : α) ∈ v '' s

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
h : ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x
t : Finset α
ht : (↑t : Set α) ⊆ s
c : ↥t → R
hx : ∑ i : ↥t, c i • v (↑i : α) = x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) (∑ i : ↥t, c i • v (↑i : α))

Tactic:
exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

Premises used: Submodule.sum_smul_mem, Submodule.span, Set.image, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
rw :
  Membership.mem (γ := Submodule R M) (span R (Set.range fun (x : (↑(↑s : Set α) : Type u_1)) ↦ v (↑x : α))) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range fun (i : ↥s) ↦ v (↑i : α))) x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (↑s : Set α))) x ↔ ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x

Tactic:
rw [← mem_span_range_iff_exists_fun, image_eq_range]

Premises used: Set.image_eq_range, Submodule.mem_span_range_iff_exists_fun
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range fun (x : (↑(↑s : Set α) : Type u_1)) ↦ v (↑x : α))) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range fun (i : ↥s) ↦ v (↑i : α))) x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
rw : (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (↑s : Set α))) x ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x

Tactic:
rw [Submodule.mem_span_image_finset_iff_exists_fun]

Premises used: Submodule.mem_span_image_finset_iff_exists_fun
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
⊢ (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x

Tactic:
⟨fun ⟨c, hc⟩ ↦ ?_, fun ⟨c, hc⟩ ↦ ?_⟩

Premises used: Finset.univ, Exists, _private.0.Submodule.mem_span_image_finset_iff_exists_fun'.match_2, Iff.intro, HSMul.hSMul, Subtype.val, _private.0.Submodule.mem_span_image_finset_iff_exists_fun'.match_1, Eq, Finset.sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
refine_1 :
  (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) →
    ∀ (c : ↥s → R) (hc : ∑ i : ↥s, c i • v (↑i : α) = x), ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
refine_2 :
  (∃ (c : α → R), ∑ i ∈ s, c i • v i = x) →
    ∀ (c : α → R) (hc : ∑ i ∈ s, c i • v i = x), ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
⊢ (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x

Tactic:
refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun ⟨c, hc⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
c : ↥s → R
hc : ∑ i : ↥s, c i • v (↑i : α) = x
⊢ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x

Tactic:
⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩

Premises used: Membership.mem, dite, Subtype.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
c : ↥s → R
hc : ∑ i : ↥s, c i • v (↑i : α) = x
refine_1 :
  ∑ i ∈ s,
      HSMul.hSMul.{u_3, u_2, u_2} (α := R)
        ((fun (i : α) ↦ (if h : i ∈ s then c (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i h) else 0 : R)) i) (v i) =
    x
⊢ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x

Tactic:
refine ⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
c : ↥s → R
hc : ∑ i : ↥s, c i • v (↑i : α) = x
refine_1 :
  Eq.{u_2 + 1} (α := M)
    (∑ i : ↥s,
      HSMul.hSMul.{u_3, u_2, u_2} (α := R)
        ((fun (i : α) ↦ (if h : i ∈ s then c (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i h) else 0 : R)) (↑i : α))
        (v (↑i : α)))
    (∑ i : ↥s, c i • v (↑i : α))
⊢ ∑ i ∈ s,
      HSMul.hSMul.{u_3, u_2, u_2} (α := R)
        ((fun (i : α) ↦ (if h : i ∈ s then c (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i h) else 0 : R)) i) (v i) =
    x

Tactic:
rw [← hc, ← Finset.sum_coe_sort (s := s)]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
c : ↥s → R
hc : ∑ i : ↥s, c i • v (↑i : α) = x
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : ↥s,
      HSMul.hSMul.{u_3, u_2, u_2} (α := R)
        ((fun (i : α) ↦ (if h : i ∈ s then c (Subtype.mk (p := fun (x : α) ↦ x ∈ s) i h) else 0 : R)) (↑i : α))
        (v (↑i : α)))
    (∑ i : ↥s, c i • v (↑i : α))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x

Tactic:
⟨fun i ↦ c i, ?_⟩

Premises used: Exists.intro, Subtype.val
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
refine_2 : ∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)) = x
⊢ ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x

Tactic:
refine ⟨fun i ↦ c i, ?_⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
h : ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
refine_2 :
  Eq.{u_2 + 1} (α := M) (∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)))
    (∑ i ∈ s, c i • v i)
refine_2₁ refine_2₂ :
  Eq.{u_2 + 1} (α := M) (∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)))
    (∑ i : ↥s, c (↑i : α) • v (↑i : α))
⊢ ∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)) = x

Tactic:
rw [← hc, ← Finset.sum_coe_sort (s := s)]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Finset α
rw rw₁ rw₂ : (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
refine_1 :
  (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) →
    ∀ (c : ↥s → R) (hc : ∑ i : ↥s, c i • v (↑i : α) = x), ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
refine_2 refine_2₁ :
  (∃ (c : α → R), ∑ i ∈ s, c i • v i = x) →
    ∀ (c : α → R) (hc : ∑ i ∈ s, c i • v i = x), ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (↑s : Set α))) x ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x

Tactic:
classical
  rw [Submodule.mem_span_image_finset_iff_exists_fun]
  refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun ⟨c, hc⟩ ↦ ?_⟩
  · refine ⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩
    rw [← hc, ← Finset.sum_coe_sort (s := s)]
    simp
  · refine ⟨fun i ↦ c i, ?_⟩
    rw [← hc, ← Finset.sum_coe_sort (s := s)]

Premises used: Submodule.mem_span_image_finset_iff_exists_fun, Finset.sum_coe_sort
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
s : Set α
inst_3 : Fintype (↑s : Type u_1)
rw :
  Membership.mem (γ := Submodule R M) (span R (v '' s)) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range fun (i : (↑s : Type u_1)) ↦ v (↑i : α))) x
rw₁ rw₂ :
  Membership.mem (γ := Submodule R M) (span R (Set.range fun (x : (↑s : Type u_1)) ↦ v (↑x : α))) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range fun (i : (↑s : Type u_1)) ↦ v (↑i : α))) x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) x ↔
    ∃ (c : (↑s : Type u_1) → R), ∑ i : (↑s : Type u_1), c i • v (↑i : α) = x

Tactic:
rw [← mem_span_range_iff_exists_fun, image_eq_range]

Premises used: Set.image_eq_range, 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
w : Set M
x : ↥(span R w)
rw :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
      (⋯.choose (p := fun (l : Finsupp.{u_2, u_1} (↑w : Type u_2) R) ↦
        (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_2) →₀ R) → M) l = (↑x : M))) =
    (↑x : M)
⊢ (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M) (repr R w x) =
    (↑x : M)

Tactic:
rw [Span.repr_def]

Premises used: Span.repr_def
-- 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
w : Set M
x : ↥(span R w)
⊢ (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
      (⋯.choose (p := fun (l : Finsupp.{u_2, u_1} (↑w : Type u_2) R) ↦
        (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_2) →₀ R) → M) l = (↑x : M))) =
    (↑x : M)

Tactic:
((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

Premises used: Exists.choose_spec, Finsupp.mem_span_iff_linearCombination, Iff.mp, 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
w : Set M
x : ↥(span R w)
⊢ (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
      (⋯.choose (p := fun (l : Finsupp.{u_2, u_1} (↑w : Type u_2) R) ↦
        (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_2) →₀ R) → M) l = (↑x : M))) =
    (↑x : M)

Tactic:
exact ((Finsupp.mem_span_iff_linearCombination _ _ _).mp x.2).choose_spec

Premises used: Exists.choose_spec, Finsupp.mem_span_iff_linearCombination, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_4
g : ι → M
l : ι →₀ R
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) ((linearCombination R g : (a : ι →₀ R) → M) l : M) : N)
    ((linearCombination R ((⇑f : (a : M) → N) ∘ g) : (a : ι →₀ R) → N) l : N)

Tactic:
apply_linearCombination _ _ _ _

Premises used: Finsupp.apply_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
s : Set M
x : M
rw :
  (∃ (l : M →₀ R),
      Membership.mem (γ := Submodule R (M →₀ R)) (supported R R s) l ∧
        (linearCombination R _root_.id : (a : M →₀ R) → M) l = x) →
    ∃ (f : M → R) (t : Finset M),
      (↑t : Set M) ⊆ _root_.id '' s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = x
⊢ Membership.mem (γ := Submodule R M) (span R s) x →
    ∃ (f : M → R) (t : Finset M), (↑t : Set M) ⊆ s ∧ Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = x

Tactic:
rw [← s.image_id, mem_span_image_iff_linearCombination]

Premises used: Finsupp.mem_span_image_iff_linearCombination, 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
s : Set M
l : M →₀ R
hl : Membership.mem (γ := Submodule R (M →₀ R)) (supported R R s) l
⊢ (↑l.support : Set M) ⊆ _root_.id '' s ∧
    Function.support.{u_2, u_1} (M := R) (⇑l : (a : M) → R) ⊆ (↑l.support : Set M) ∧
      Eq (α := M) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : M) → R) a : R) a : M)
        ((linearCombination R _root_.id : (a : M →₀ R) → M) l : M)

Tactic:
simpa [linearCombination, Finsupp.sum] using hl

Premises used: Finsupp.sum, Finsupp.linearCombination