no goals
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι'✝ : Type ?u.9376
inst✝¹ : Fintype ι'✝
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
ι' : Type u_1
q : ι' → P
i : ι'
⊢ ∑ j : ι, toMatrix b q i j = 1
simp