case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
⊢ range (toDual b) = ⊤
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
inst✝ : _root_.Finite ι
⊢ range (toDual b) = ⊤
cases nonempty_fintype ι
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
⊢ f ∈ range (toDual b)
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
⊢ range (toDual b) = ⊤
refine' eq_top_iff'.2 fun f => _
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
⊢ ∃ y, ↑(toDual b) y = f
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
⊢ f ∈ range (toDual b)
rw [LinearMap.mem_range]
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
⊢ ∃ y, ↑(toDual b) y = f
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
⊢ ∃ y, ↑(toDual b) y = f
let lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f.toFun (b i)
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
i : ι
⊢ ↑(↑(toDual b) (↑(Finsupp.total ι M R ↑b) lin_comb)) (↑b i) = ↑f (↑b i)
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
⊢ ∃ y, ↑(toDual b) y = f
refine' ⟨Finsupp.total ι M R b lin_comb, b.ext fun i => _⟩
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
i : ι
⊢ ↑lin_comb i = ↑f (↑b i)
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
i : ι
⊢ ↑(↑(toDual b) (↑(Finsupp.total ι M R ↑b) lin_comb)) (↑b i) = ↑f (↑b i)
rw [b.toDual_eq_repr _ i, repr_total b]
no goals
case intro
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
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
i : ι
⊢ ↑lin_comb i = ↑f (↑b i)
rfl