case h
α : Type u_2
M : Type u_1
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
⊢ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x).support ⊆ Finset.univ

case hf
α : Type u_2
M : Type u_1
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 : α),
    x_1 ∈ Finset.univ →
      ¬x_1 ∈ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x).support →
        (fun i => ↑((fun i => smulRight LinearMap.id (v i)) i)) x_1
            (↑(↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x) x_1) =
          0
α : Type u_2
M : Type u_1
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
⊢ ↑(Finsupp.total α M R v) (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x) = ↑(↑(Fintype.total R S) v) x
apply Finset.sum_subset
no goals
case h
α : Type u_2
M : Type u_1
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
⊢ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x).support ⊆ Finset.univ
exact Finset.subset_univ _
case hf
α : Type u_2
M : Type u_1
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 ∈ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x✝).support
⊢ (fun i => ↑((fun i => smulRight LinearMap.id (v i)) i)) x
      (↑(↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x✝) x) =
    0
case hf
α : Type u_2
M : Type u_1
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 : α),
    x_1 ∈ Finset.univ →
      ¬x_1 ∈ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x).support →
        (fun i => ↑((fun i => smulRight LinearMap.id (v i)) i)) x_1
            (↑(↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x) x_1) =
          0
intro x _ hx
case hf
α : Type u_2
M : Type u_1
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 ∈ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x✝).support
⊢ (fun i => ↑((fun i => smulRight LinearMap.id (v i)) i)) x 0 = 0
case hf
α : Type u_2
M : Type u_1
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 ∈ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x✝).support
⊢ (fun i => ↑((fun i => smulRight LinearMap.id (v i)) i)) x
      (↑(↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x✝) x) =
    0
rw [Finsupp.not_mem_support_iff.mp hx]
no goals
case hf
α : Type u_2
M : Type u_1
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 ∈ (↑(LinearEquiv.symm (linearEquivFunOnFinite R R α)) x✝).support
⊢ (fun i => ↑((fun i => smulRight LinearMap.id (v i)) i)) x 0 = 0
exact zero_smul _ _