R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d in f.support, ↑(↑(toDual b) (↑f d • ↑b d)) (↑b i) = ↑f i
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ↑(↑(toDual b) (↑(Finsupp.total ι M R ↑b) f)) (↑b i) = ↑f i
rw [Finsupp.total_apply, Finsupp.sum, LinearMap.map_sum, LinearMap.sum_apply]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then ↑f i else 0) = ↑f i
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d in f.support, ↑(↑(toDual b) (↑f d • ↑b d)) (↑b i) = ↑f i
simp_rw [LinearMap.map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole,
  Finset.sum_ite_eq']
case inl
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ ↑f i = ↑f i

case inr
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : ¬i ∈ f.support
⊢ 0 = ↑f i
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then ↑f i else 0) = ↑f i
split_ifs with h
no goals
case inl
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ ↑f i = ↑f i
rfl
no goals
case inr
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : ¬i ∈ f.support
⊢ 0 = ↑f i
rw [Finsupp.not_mem_support_iff.mp h]