awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
c : R
a : α
⊢ (linearCombination R v : (a : α →₀ R) → M) (single a c) = c • v a

Tactic:
simp [linearCombination_apply, sum_single_index]

Premises used: Finsupp.sum_single_index, Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : α →₀ R
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R 0 : (a : α →₀ R) → M) x : M) (0 : M)

Tactic:
simp [linearCombination_apply]

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (α →₀ R) →ₗ[R] M) (linearCombination R 0) 0

Tactic:
LinearMap.ext (linearCombination_zero_apply R)

Premises used: Finsupp.linearCombination_zero_apply, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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
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
⊢ (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

Tactic:
rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_eq_single, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 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

Tactic:
rw [Pi.single_eq_of_ne hi, smul_zero]

Premises used: smul_zero, Pi.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
⊢ ∀ (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:
exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
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:
simp only [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : M
a : α
f : α →₀ R
inst_3 : DecidableEq α
⊢ 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:
exact fun _ ↦ by simp only [zero_smul]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
v : α → M
f : M →ₗ[R] M'
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')
⊢ linearCombination R ((⇑f : (a : M) → M') ∘ v) = f ∘ₗ linearCombination R v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
v : α → M
f : M →ₗ[R] M'
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:
simp [linearCombination_apply]

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
v : α → M
l : α →₀ R
⊢ Eq.{u_8 + 1} (α := M') ((f : (a : M) → M') ((linearCombination R v : (a : α →₀ R) → M) l : M) : M')
    ((linearCombination R ((⇑f : (a : M) → M') ∘ v) : (a : α →₀ R) → M') l : M')

Tactic:
congr($(linearCombination_linear_comp R f) l).symm

Premises used: congrArg, Finsupp.linearCombination_linear_comp, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
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'
f : M →ₗ[R] M'
l : M →₀ R
⊢ Eq.{u_8 + 1} (α := M') ((f : (a : M) → M') ((linearCombination R _root_.id : (a : M →₀ R) → M) l : M) : M')
    ((linearCombination R (⇑f : (a : M) → M') : (a : M →₀ R) → M') l : M')

Tactic:
apply_linearCombination ..

Premises used: Finsupp.apply_linearCombination
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := M) ((linearCombination R v : (a : α →₀ R) → M) l : M)
    ((linearCombination R v : (a : α →₀ R) → M) l : M)
⊢ (linearCombination R v : (a : α →₀ R) → M) l =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((l : (a : α) → R) default : R) (v default)

Tactic:
rw [← linearCombination_single, ← unique_single l]

Premises used: Finsupp.unique_single, Finsupp.linearCombination_single
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
h : Function.Surjective v
x : M
obtain : ∀ (y : α) (hy : v y = x), ∃ (a : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) a = x
⊢ ∃ (a : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) a = x

Tactic:
obtain ⟨y, hy⟩ := h x
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ (linearCombination R v : (a : α →₀ R) → M) (single y 1) = x

Tactic:
simp [hy]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
h : Function.Surjective v
x : M
y : α
hy : v y = x
⊢ ∃ (a : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) a = x

Tactic:
exact ⟨single y 1, by simp [hy]⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
h : Function.Surjective v
⊢ Eq (α := Submodule R M) (LinearMap.range (linearCombination R v)) ⊤

Tactic:
range_eq_top.2 <| linearCombination_surjective R h

Premises used: Iff.mpr, LinearMap.range_eq_top, Finsupp.linearCombination_surjective
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
R : Type u_5
inst : Semiring R
M : Type u_9
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Function.Surjective (α := M →₀ R) (β := M) (⇑(linearCombination R _root_.id) : (a : M →₀ R) → M)

Tactic:
linearCombination_surjective R Function.surjective_id

Premises used: Function.surjective_id, Finsupp.linearCombination_surjective
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
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
⊢ Eq (α := Submodule R M) (LinearMap.range (linearCombination R v)) (span R (Set.range v))

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
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
h₁ :
  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) (LinearMap.range (linearCombination R v)) x ↔
    Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
hx : Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x
⊢ ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x

Tactic:
rw [LinearMap.mem_range] at hx

Premises used: LinearMap.mem_range
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
hx : ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x
h :
  ∀ (l : α →₀ R) (hl : (linearCombination R v : (a : α →₀ R) → M) l = x),
    Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
rcases hx with ⟨l, hl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v : (a : α →₀ R) → M) l = x
h :
  Membership.mem (α := M) (γ := Submodule R M) (span R (Set.range v)) ((linearCombination R v : (a : α →₀ R) → M) l : M)
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
rw [← hl]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v : (a : α →₀ R) → M) l = x
h : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (l.sum fun (i : α) (a : R) ↦ a • v i)
⊢ Membership.mem (α := M) (γ := Submodule R M) (span R (Set.range v)) ((linearCombination R v : (a : α →₀ R) → M) l : M)

Tactic:
rw [linearCombination_apply]

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) (l.sum fun (i : α) (a : R) ↦ a • v i)

Tactic:
sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))

Premises used: Set.mem_range_self, Set.Mem, Finsupp.sum, Submodule.span, Submodule.subset_span, Set.range, DFunLike.coe, sum_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
l : α →₀ R
hl : (linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) (l.sum fun (i : α) (a : R) ↦ a • v i)

Tactic:
exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))

Premises used: Set.mem_range_self, Submodule.span, Submodule.subset_span, Set.range, sum_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
h : Set.range v ⊆ (↑(LinearMap.range (linearCombination R v)) : Set M)
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x →
    Membership.mem (γ := Submodule R M) (LinearMap.range (linearCombination R v)) x

Tactic:
apply span_le.2

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x_1 x : M
hx : x ∈ Set.range v
h : ∀ (i : α) (hi : v i = x), x ∈ (↑(LinearMap.range (linearCombination R v)) : Set M)
⊢ x ∈ (↑(LinearMap.range (linearCombination R v)) : Set M)

Tactic:
rcases hx with ⟨i, hi⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x_1 x : M
i : α
hi : v i = x
h : ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x
⊢ x ∈ (↑(LinearMap.range (linearCombination R v)) : Set M)

Tactic:
rw [SetLike.mem_coe, LinearMap.mem_range]

Premises used: LinearMap.mem_range, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x_1 x : M
i : α
hi : v i = x
h : (linearCombination R v : (a : α →₀ R) → M) (single i 1) = x
⊢ ∃ (y : α →₀ R), (linearCombination R v : (a : α →₀ R) → M) y = x

Tactic:
use single i 1

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x_1 x : M
i : α
hi : v i = x
⊢ (linearCombination R v : (a : α →₀ R) → M) (single i 1) = x

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
rw :
  Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (LinearMap.range (linearCombination R v)) ⊤
rw₁ rw₂ : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
⊢ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    Function.Surjective (α := α →₀ R) (β := M) (⇑(linearCombination R v) : (a : α →₀ R) → M)

Tactic:
rw [← LinearMap.range_eq_top, range_linearCombination]

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), (g : (a : M) → M') (v i) = v' (f i)
h₁ :
  ∀ (l : α),
    Eq.{u_8 + 1} (α := M') (((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l : (a : R) → M') 1 : M')
      (((g ∘ₗ linearCombination R v) ∘ₗ lsingle l : (a : R) → M') 1 : M')
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v

Tactic:
ext l
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_7
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), (g : (a : M) → M') (v i) = v' (f i)
l : α
⊢ Eq.{u_8 + 1} (α := M') (((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l : (a : R) → M') 1 : M')
    (((g ∘ₗ linearCombination R v) ∘ₗ lsingle l : (a : R) → M') 1 : M')

Tactic:
simp [linearCombination_apply, h]

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α → α'
h :
  ∀ (a : α),
    Eq.{u_8 + 1} (α := M') (((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a : (a : R) → M') 1 : M')
      ((linearCombination R (v' ∘ f) ∘ₗ lsingle a : (a : R) → M') 1 : M')
⊢ Eq (α := (α →₀ R) →ₗ[R] M') (linearCombination R v' ∘ₗ lmapDomain R R f) (linearCombination R (v' ∘ f))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α → α'
a : α
⊢ Eq.{u_8 + 1} (α := M') (((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a : (a : R) → M') 1 : M')
    ((linearCombination R (v' ∘ f) ∘ₗ lsingle a : (a : R) → M') 1 : M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α ↪ α'
l : α →₀ R
⊢ Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (embDomain f l) : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')

Tactic:
simp [linearCombination_apply, Finsupp.sum, support_embDomain, embDomain_apply]

Premises used: Finsupp.embDomain_apply, Finsupp.sum, Finsupp.linearCombination_apply, Finsupp.support_embDomain
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α → α'
l : α →₀ R
⊢ Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (mapDomain f l) : M')
    ((linearCombination R (v' ∘ f) : (a : α →₀ R) → M') l : M')

Tactic:
LinearMap.congr_fun (linearCombination_comp_lmapDomain _ _) l

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, LinearMap.congr_fun, Finsupp.linearCombination_comp_lmapDomain, Finset.sum
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
α' : Type u_7
M' : Type u_8
inst_1 : AddCommMonoid M'
inst_2 : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
rw :
  Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (mapDomain (⇑f : (a : α) → α') l) : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
rw₁ rw₂ :
  Eq.{u_8 + 1} (α := M') ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')
⊢ Eq.{u_8 + 1} (α := M') ((linearCombination R v' : (a : α' →₀ R) → M') (equivMapDomain f l) : M')
    ((linearCombination R (v' ∘ (⇑f : (a : α) → α')) : (a : α →₀ R) → M') l : M')

Tactic:
rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]

Premises used: Finsupp.equivMapDomain_eq_mapDomain, Finsupp.linearCombination_mapDomain
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
rw :
  Eq (α := Submodule R M) (span R s)
    (span R (Set.range (ι := { x : M // x ∈ s }) (Subtype.val (p := fun (x : M) ↦ x ∈ s))))
rw₁ : Eq (α := Submodule R M) (span R s) (span R {x : M | x ∈ s})
rw₂ rw₃ : Eq (α := Submodule R M) (span R s) (span R s)
⊢ Eq (α := Submodule R M) (span R s)
    (LinearMap.range (M := Finsupp.{u_2, u_5} { x : M // x ∈ s } R)
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))

Tactic:
rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, Finsupp.range_linearCombination
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
M : Type u_2
R : Type u_5
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 ↔
    ∃ (l : Finsupp.{u_2, u_5} (↑s : Type u_2) R),
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)) : (a : (↑s : Type u_2) →₀ R) → M) l = x

Tactic:
(SetLike.ext_iff.1 <| span_eq_range_linearCombination _ _) x

Premises used: Set.Mem, setOf, SetLike.ext_iff, Finsupp.span_eq_range_linearCombination, Iff.mp, Set.range
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
x : M
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x ↔
    ∃ (c : α →₀ R), (c.sum fun (i : α) (a : R) ↦ a • v i) = x

Tactic:
simp only [← Finsupp.range_linearCombination, LinearMap.mem_range, linearCombination_apply]

Premises used: Finsupp.linearCombination_apply, Finsupp.range_linearCombination, LinearMap.mem_range
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
h₁ : v '' s ⊆ (↑(map (linearCombination R v) (supported R R s)) : Set M)
h₂ : LE.le (α := Submodule R M) (map (linearCombination R v) (supported R R s)) (span R (v '' s))
⊢ Eq (α := Submodule R M) (span R (v '' s)) (map (linearCombination R v) (supported R R s))

Tactic:
apply span_eq_of_le

Premises used: Submodule.span_eq_of_le
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
x : M
hx : x ∈ v '' s
⊢ ∃ x_1 ∈ s, v x_1 = x

Tactic:
rw [Set.mem_image] at hx

Premises used: Set.mem_image
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
h₁ : ∀ (a : α), a ∈ s ∧ v a = x → x ∈ (↑(map (linearCombination R v) (supported R R s)) : Set M)
⊢ x ∈ (↑(map (linearCombination R v) (supported R R s)) : Set M)

Tactic:
apply Exists.elim hx

Premises used: Exists.elim
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ (linearCombination R v : (a : α →₀ R) → M) (single i 1) = x

Tactic:
simp [hi.2]

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
i : α
hi : i ∈ s ∧ v i = x
⊢ x ∈ (↑(map (linearCombination R v) (supported R R s)) : Set M)

Tactic:
exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : α → M
s : Set α
⊢ LE.le (α := Submodule R M) (map (linearCombination R v) (supported R R s)) (span R (v '' s))

Tactic:
map_le_iff_le_comap.2 fun z hz => ?_

Premises used: Iff.mpr, Set.Mem, Submodule.map_le_iff_le_comap