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
s : Set α
h₂ :
  ∀ (z : α →₀ R) (hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z),
    Membership.mem (γ := Submodule R (α →₀ R)) (comap (linearCombination R v) (span R (v '' s))) z
⊢ LE.le (α := Submodule R M) (map (linearCombination R v) (supported R R s)) (span R (v '' s))

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

Premises used: Iff.mpr, Submodule.map_le_iff_le_comap
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
haveI :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))

Tactic:
haveI := Classical.decPred fun x => x ∈ s
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
this : DecidablePred fun (x : α) ↦ x ∈ s
pos :
  ∀ (h : c ∈ s),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
neg :
  ∀ (h : c ∉ s),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))

Tactic:
by_cases h : c ∈ s
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
this : DecidablePred fun (x : α) ↦ x ∈ s
h : c ∈ s
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))

Tactic:
smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))

Premises used: Set.mem_image_of_mem, Submodule.subset_span, 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
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
this : DecidablePred fun (x : α) ↦ x ∈ s
h : c ∈ s
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))

Tactic:
exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))

Premises used: Set.mem_image_of_mem, Submodule.subset_span, 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
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
c : α
this : DecidablePred fun (x : α) ↦ x ∈ s
h : c ∉ s
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s))
    (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) c : R) (v c))

Tactic:
simp [(Finsupp.mem_supported' R _).1 hz _ h]

Premises used: Iff.mp, Finsupp.mem_supported'
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
⊢ ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))

Tactic:
have : ∀ i, z i • v i ∈ span R (v '' s) := by
      intro c
      haveI := Classical.decPred fun x => x ∈ s
      by_cases h : c ∈ s
      · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
      · simp [(Finsupp.mem_supported' R _).1 hz _ h]
-- 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 α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
this :
  ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
h₂ : Membership.mem (γ := Submodule R M) (span R (v '' s)) (z.sum fun (i : α) (a : R) ↦ a • v i)
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (comap (linearCombination R v) (span R (v '' s))) z

Tactic:
rw [mem_comap, linearCombination_apply]

Premises used: Submodule.mem_comap, 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
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
this :
  ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) (z.sum fun (i : α) (a : R) ↦ a • v i)

Tactic:
sum_mem ?_

Premises used: Set.Mem, Finsupp.sum, sum_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
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
this :
  ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
h₂ :
  ∀ c ∈ z.support,
    Membership.mem (γ := Submodule R M) (span R (v '' s)) ((fun (i : α) (a : R) ↦ a • v i) c ((z : (a : α) → R) c))
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) (z.sum fun (i : α) (a : R) ↦ a • v i)

Tactic:
refine sum_mem ?_

Premises used: sum_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
s : Set α
z : α →₀ R
hz : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) z
this :
  ∀ (i : α),
    Membership.mem (γ := Submodule R M) (span R (v '' s))
      (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((z : (a : α) → R) i : R) (v i))
⊢ ∀ c ∈ z.support,
    Membership.mem (γ := Submodule R M) (span R (v '' s)) ((fun (i : α) (a : R) ↦ a • v i) c ((z : (a : α) → R) c))

Tactic:
simp [this]
-- 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
rw :
  Membership.mem (γ := Submodule R M) (map (linearCombination R v) (supported R R s)) x ↔
    ∃ (l : α →₀ R),
      Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l ∧ (linearCombination R v : (a : α →₀ R) → M) l = x
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) x ↔
    ∃ (l : α →₀ R),
      Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l ∧ (linearCombination R v : (a : α →₀ R) → M) l = x

Tactic:
rw [span_image_eq_map_linearCombination]

Premises used: Finsupp.span_image_eq_map_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
v : α → M
s : Set α
x : M
⊢ Membership.mem (γ := Submodule R M) (map (linearCombination R v) (supported R R s)) x ↔
    ∃ (l : α →₀ R),
      Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l ∧ (linearCombination R v : (a : α →₀ R) → M) l = x

Tactic:
simp
-- 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 : Option α → M
f : Finsupp.{u_1, u_5} (Option α) R
rw :
  (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none) +
      f.some.sum fun (a : α) (r : R) ↦ r • v (Option.some a)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none) +
      f.some.sum fun (i : α) (a : R) ↦ a • (v ∘ Option.some) i
⊢ (linearCombination R v : (a : Option α →₀ R) → M) f =
    HAdd.hAdd (β := M) (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none))
      ((linearCombination R (v ∘ Option.some) : (a : α →₀ R) → M) f.some : M)

Tactic:
rw [linearCombination_apply, sum_option_index_smul, linearCombination_apply]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_option_index_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
v : Option α → M
f : Finsupp.{u_1, u_5} (Option α) R
⊢ (HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none) +
      f.some.sum fun (a : α) (r : R) ↦ r • v (Option.some a)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (v none) +
      f.some.sum fun (i : α) (a : R) ↦ a • (v ∘ Option.some) i

Tactic:
simp
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
simp :
  Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
⊢ Eq.{u_2 + 1} (α := M)
    ((linearCombination R A : (a : α →₀ R) → M) ((linearCombination R B : (a : β →₀ R) → α →₀ R) f : α →₀ R) : M)
    ((linearCombination R fun (b : β) ↦ (linearCombination R A : (a : α →₀ R) → M) (B b) : (a : β →₀ R) → M) f : M)

Tactic:
simp only [linearCombination_apply]

Premises used: Finsupp.linearCombination_apply
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
⊢ Eq.{u_2 + 1} (α := M) (sum (sum 0 fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (sum 0 fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))

Tactic:
simp only [sum_zero_index]

Premises used: Finsupp.sum_zero_index
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f₁ f₂ : β →₀ R
h₁ :
  Eq.{u_2 + 1} (α := M) (sum (f₁.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f₁.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
h₂ :
  Eq.{u_2 + 1} (α := M) (sum (f₂.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f₂.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
⊢ Eq.{u_2 + 1} (α := M) (sum ((f₁ + f₂).sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    ((f₁ + f₂).sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))

Tactic:
simp [sum_add_index, h₁, h₂, add_smul]

Premises used: add_smul, Finsupp.sum_add_index
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
a : β
b : R
⊢ Eq.{u_2 + 1} (α := M) (sum (sum (single a b) fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (sum (single a b) fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))

Tactic:
simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Premises used: Finsupp.sum_single_index, Finsupp.sum_smul_index, Finsupp.smul_sum, SemigroupAction.mul_smul
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
zero :
  Eq.{u_2 + 1} (α := M) (sum (sum 0 fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (sum 0 fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
add :
  ∀ (f₁ f₂ : β →₀ R)
    (h₁ :
      Eq.{u_2 + 1} (α := M) (sum (f₁.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
        (f₁.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i)))
    (h₂ :
      Eq.{u_2 + 1} (α := M) (sum (f₂.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
        (f₂.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))),
    Eq.{u_2 + 1} (α := M) (sum ((f₁ + f₂).sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
      ((f₁ + f₂).sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
single :
  ∀ (a : β) (b : R),
    Eq.{u_2 + 1} (α := M) (sum (sum (Finsupp.single a b) fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
      (sum (Finsupp.single a b) fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
⊢ Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))

Tactic:
induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Premises used: Finsupp.sum_single_index, Finsupp.sum_smul_index, add_smul, Submodule.zero, Finsupp.smul_sum, Finsupp.sum_add_index, Submodule.add, Finsupp.sum_zero_index, SemigroupAction.mul_smul, Finsupp.single
-- 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
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
simp :
  Eq.{u_2 + 1} (α := M) (sum (f.sum fun (i : β) (a : R) ↦ a • B i) fun (i : α) (a : R) ↦ a • A i)
    (f.sum fun (i : β) (a : R) ↦ HSMul.hSMul (β := M) a ((B i).sum fun (i : α) (a : R) ↦ a • A i))
⊢ Eq.{u_2 + 1} (α := M)
    ((linearCombination R A : (a : α →₀ R) → M) ((linearCombination R B : (a : β →₀ R) → α →₀ R) f : α →₀ R) : M)
    ((linearCombination R fun (b : β) ↦ (linearCombination R A : (a : α →₀ R) → M) (B b) : (a : β →₀ R) → M) f : M)

Tactic:
classical
  simp only [linearCombination_apply]
  induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Premises used: Finsupp.sum_single_index, Finsupp.sum_smul_index, Finsupp.linearCombination_apply, add_smul, Submodule.zero, Finsupp.smul_sum, Finsupp.sum_add_index, Submodule.add, Finsupp.sum_zero_index, SemigroupAction.mul_smul, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
α' : Type u_7
v : α → M
inst_4 : Module R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
w : α' → S
h :
  ∀ (a : α × α'),
    Eq.{u_2 + 1} (α := M) (((linearCombination R fun (i : α × α') ↦ w i.2 • v i.1) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      ((((↑R :
                    {S : Type u_6} →
                      {M : Type (max u_1 u_6)} →
                        {M₂ : Type u_2} →
                          [inst : Semiring R] →
                            [inst_7 : Semiring S] →
                              [inst_8 : AddCommMonoid M] →
                                [inst_9 : AddCommMonoid M₂] →
                                  [inst_10 : Module R M] →
                                    [inst_11 : Module R M₂] →
                                      [inst_12 : Module S M] →
                                        [inst_13 : Module S M₂] →
                                          [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (linearCombination S v) ∘ₗ
                mapRange.linearMap (linearCombination R w) ∘ₗ
                  (↑(curryLinearEquiv R) : (α × α' →₀ R) →ₗ[R] α →₀ α' →₀ R)) ∘ₗ
              lsingle a :
            (a : R) → M)
          1 :
        M)
⊢ Eq (α := (α × α' →₀ R) →ₗ[R] M) (linearCombination R fun (i : α × α') ↦ w i.2 • v i.1)
    ((↑R :
          {S : Type u_6} →
            {M : Type (max u_1 u_6)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module R M] →
                          [inst_11 : Module R M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (linearCombination S v) ∘ₗ
      mapRange.linearMap (linearCombination R w) ∘ₗ (↑(curryLinearEquiv R) : (α × α' →₀ R) →ₗ[R] α →₀ α' →₀ R))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
α' : Type u_7
v : α → M
inst_4 : Module R S
inst_5 : Module S M
inst_6 : IsScalarTower R S M
w : α' → S
a : α × α'
⊢ Eq.{u_2 + 1} (α := M) (((linearCombination R fun (i : α × α') ↦ w i.2 • v i.1) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    ((((↑R :
                  {S : Type u_6} →
                    {M : Type (max u_1 u_6)} →
                      {M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_7 : Semiring S] →
                            [inst_8 : AddCommMonoid M] →
                              [inst_9 : AddCommMonoid M₂] →
                                [inst_10 : Module R M] →
                                  [inst_11 : Module R M₂] →
                                    [inst_12 : Module S M] →
                                      [inst_13 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (linearCombination S v) ∘ₗ
              mapRange.linearMap (linearCombination R w) ∘ₗ
                (↑(curryLinearEquiv R) : (α × α' →₀ R) →ₗ[R] α →₀ α' →₀ R)) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)

Tactic:
simp
-- 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
f : Fin 0 → M
h :
  ∀ (i : Fin 0),
    Eq.{u_2 + 1} (α := M) ((linearCombination R f ∘ₗ lsingle i : (a : R) → M) 1 : M)
      ((0 ∘ₗ lsingle i : (a : R) → M) 1 : M)
⊢ Eq (α := (Fin 0 →₀ R) →ₗ[R] M) (linearCombination R f) 0

Tactic:
ext i
-- 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
f : Fin 0 → M
i : Fin 0
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R f ∘ₗ lsingle i : (a : R) → M) 1 : M)
    ((0 ∘ₗ lsingle i : (a : R) → M) 1 : M)

Tactic:
apply finZeroElim i

Premises used: finZeroElim
-- 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 α
rw : LE.le (α := Submodule R M) (span R (v '' s)) (map (linearCombination R v) (supported R R s))
⊢ Eq (α := Submodule R ↥(span R (v '' s))) (LinearMap.range (linearCombinationOn α M R v s)) ⊤

Tactic:
rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
    range_subtype]

Premises used: Submodule.map_top, LinearMap.range_comp, Finsupp.linearCombinationOn, LinearMap.range_le_iff_comap, LinearMap.map_codRestrict, LinearMap.range_eq_map, Submodule.range_subtype
-- 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) (span R (v '' s)) (map (linearCombination R v) (supported R R s))

Tactic:
(span_image_eq_map_linearCombination _ _).le

Premises used: Set.Mem, Finsupp.span_image_eq_map_linearCombination, Eq.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 α
⊢ LE.le (α := Submodule R M) (span R (v '' s)) (map (linearCombination R v) (supported R R s))

Tactic:
exact (span_image_eq_map_linearCombination _ _).le

Premises used: Finsupp.span_image_eq_map_linearCombination, Eq.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 α
h :
  ∀ (a : (↑s : Type u_1)),
    Eq.{u_2 + 1} (α := M) ((linearCombination R (s.restrict (π := fun (a : α) ↦ M) v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      (((Submodule.subtype (span R (v '' s)) ∘ₗ
                linearCombinationOn α M R v s ∘ₗ
                  (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s))) ∘ₗ
              lsingle a :
            (a : R) → M)
          1 :
        M)
⊢ Eq (α := Finsupp.{u_1, u_5} (↑s : Type u_1) R →ₗ[R] M) (linearCombination R (s.restrict (π := fun (a : α) ↦ M) v))
    (Submodule.subtype (span R (v '' s)) ∘ₗ
      linearCombinationOn α M R v s ∘ₗ
        (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s)))

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
v : α → M
s : Set α
a : (↑s : Type u_1)
⊢ Eq.{u_2 + 1} (α := M) ((linearCombination R (s.restrict (π := fun (a : α) ↦ M) v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    (((Submodule.subtype (span R (v '' s)) ∘ₗ
              linearCombinationOn α M R v s ∘ₗ
                (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s))) ∘ₗ
            lsingle a :
          (a : R) → M)
        1 :
      M)

Tactic:
simp [linearCombinationOn]

Premises used: Finsupp.linearCombinationOn
-- 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 h₁ :
  ∀ (a : (↑s : Type u_1)),
    Eq.{u_2 + 1} (α := M) ((linearCombination R (s.restrict (π := fun (a : α) ↦ M) v) ∘ₗ lsingle a : (a : R) → M) 1 : M)
      (((Submodule.subtype (span R (v '' s)) ∘ₗ
                linearCombinationOn α M R v s ∘ₗ
                  (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s))) ∘ₗ
              lsingle a :
            (a : R) → M)
          1 :
        M)
⊢ Eq (α := Finsupp.{u_1, u_5} (↑s : Type u_1) R →ₗ[R] M) (linearCombination R (s.restrict (π := fun (a : α) ↦ M) v))
    (Submodule.subtype (span R (v '' s)) ∘ₗ
      linearCombinationOn α M R v s ∘ₗ
        (↑(LinearEquiv.symm (supportedEquivFinsupp s)) : ((↑s : Type u_1) →₀ R) →ₗ[R] ↥(supported R R s)))

Tactic:
classical ext; simp [linearCombinationOn]

Premises used: Finsupp.linearCombinationOn