awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
S : Type u_4
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
v_1 : α → M
r : S
v : α → M
⊢ Fintype.linearCombination R (r • v) =
    HSMul.hSMul (α := S) (β := (α → R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (Fintype.linearCombination R v)
have h : ∀ (x : α → R),
  Eq.{u_2 + 1} (α := M) ((Fintype.linearCombination R (r • v) : (a : α → R) → M) x : M)
    ((HSMul.hSMul (α := S) (β := (α → R) →ₗ[R] M) ((RingHom.id S : (a : S) → S) r : S) (Fintype.linearCombination R v) :
          (a : α → R) → M)
        x :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x ↔ ∃ (c : α → R), ∑ i : α, c i • v i = x
have 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
Tactic: rw [Finsupp.equivFunOnFinite.surjective.exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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
have 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
Tactic: simp only [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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), ∃ (c : α → R), ∑ i : α, c i • v i = x
have 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
Tactic: simp_rw [← mem_span_range_iff_exists_fun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨t, ht, c, hx⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ ∃ (c : ↥t → R), ∑ i : ↥t, c i • v (↑i : α) = x
have 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
Tactic: obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have 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
Tactic: refine ⟨l.support, hl, l ∘ (↑), ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∑ 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
have 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)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)) x
have refine_2 : Membership.mem (γ := Submodule R M) (span R (v '' s)) (∑ i : ↥t, c i • v (↑i : α))
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 (v '' (↑s : Set α))) x ↔ ∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x
have 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
Tactic: rw [← mem_span_range_iff_exists_fun, image_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 (v '' (↑s : Set α))) x ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
have rw : (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
Tactic: rw [Submodule.mem_span_image_finset_iff_exists_fun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have 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
Tactic: refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun ⟨c, hc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = x) ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
have 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
Tactic: refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun ⟨c, hc⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have 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
Tactic: refine ⟨fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∑ 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
have 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 : α))
Tactic: rw [← hc, ← Finset.sum_coe_sort (s := s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have refine_2 : ∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)) = x
Tactic: refine ⟨fun i ↦ c i, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)) = x
have 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)
Tactic: rw [← hc, ← Finset.sum_coe_sort (s := s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)
⊢ ∑ i : ↥s, HSMul.hSMul.{u_3, u_2, u_2} (α := R) ((fun (i : ↥s) ↦ c (↑i : α)) i) (v (↑i : α)) = x
have 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 : α))
Tactic: rw [← hc, ← Finset.sum_coe_sort (s := s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 (v '' (↑s : Set α))) x ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
have rw : (∃ (c : ↥s → R), ∑ i : ↥s, c i • v (↑i : α) = 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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (↑s : Set α))) x ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
have 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
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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R (v '' (↑s : Set α))) x ↔ ∃ (c : α → R), ∑ i ∈ s, c i • v i = x
have 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
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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)
⊢ 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
have 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
Tactic: rw [← mem_span_range_iff_exists_fun, image_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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
have 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
Tactic: rw [← mem_span_range_iff_exists_fun, image_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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) (repr R w x) =
    (↑x : M)
have rw : (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : { x : M // x ∈ w } →₀ R) → M)
    (sorry.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: rw [Span.repr_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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
have 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
Tactic: rw [← s.image_id, mem_span_image_iff_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 : M → R), Function.support f ⊆ (↑s : Set M) ∧ ∑ a ∈ s, f a • a = x
have 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
Tactic: rw [mem_span_iff_exists_finset_subset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)
have refine : ∀ x ∈ s, x ∉ t → f x • x = 0
Tactic: refine ⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 s) x
have rw : Membership.mem (γ := Submodule R M)
  (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) x
Tactic: rw [← Subtype.range_val (s := s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 s) x ↔
    ∃ (f : (↑s : Type u_2) → R), ∑ a : (↑s : Type u_2), f a • (↑a : M) = x
have 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
Tactic: conv_lhs => rw [← Subtype.range_val (s := s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have rw : Membership.mem (γ := Submodule R M) (span R (_root_.id '' s)) m
Tactic: rw [← Set.image_id s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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 ↔
    ∃ (c : M →₀ R), (↑c.support : Set M) ⊆ s ∧ (c.sum fun (mi : M) (r : R) ↦ r • mi) = m
have 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
Tactic: conv_lhs => rw [← Set.image_id s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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
⊢ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → (↑s : Type u_2)), ∑ i : Fin n, f i • (↑(g i) : M) = m
have 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)
Tactic: rcases mem_span_set.1 h with ⟨c, cs, rfl⟩
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.LinearCombination (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: have A : c.support ≃ Fin c.support.card := Finset.equivFin _