-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply (x : α → R) :
    linearCombination R v ((Finsupp.linearEquivFunOnFinite R R α).symm x) =
      Fintype.linearCombination R S v x

Proof state:
case h
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : α → R
⊢ ((linearEquivFunOnFinite R R α).symm x).support ⊆ Finset.univ

Tactic:
exact Finset.subset_univ _

Result:
no goals

Proof state:
case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : α → R
⊢ ∀ x_1 ∈ Finset.univ,
    x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support →
      (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0

Tactic:
intro x _ hx

Result:
case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x (((linearEquivFunOnFinite R R α).symm x✝) x) = 0

Proof state:
case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x 0 = 0

Tactic:
exact zero_smul _ _

Result:
no goals

Proof state:
case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x (((linearEquivFunOnFinite R R α).symm x✝) x) = 0

Tactic:
rw [Finsupp.not_mem_support_iff.mp hx]

Result:
case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x 0 = 0

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : α → R
⊢ (linearCombination R v) ((linearEquivFunOnFinite R R α).symm x) = ((Fintype.linearCombination R S) v) x

Tactic:
apply Finset.sum_subset

Result:
case h
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : α → R
⊢ ((linearEquivFunOnFinite R R α).symm x).support ⊆ Finset.univ

case hf
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
x : α → R
⊢ ∀ x_1 ∈ Finset.univ,
    x_1 ∉ ((linearEquivFunOnFinite R R α).symm x).support →
      (fun i => ⇑((fun i => LinearMap.id.smulRight (v i)) i)) x_1 (((linearEquivFunOnFinite R R α).symm x) x_1) = 0