case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j = ↑(coords b) x j
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) = ↑(coords b) x
ext j
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j = ↑(coord b j) x
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j = ↑(coords b) x j
change _ = b.coord j x
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j =
    ↑(coord b j) (↑(Finset.affineCombination k Finset.univ ↑b₂) fun i => ↑(coord b₂ i) x)
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j = ↑(coord b j) x
conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j =
    ↑(Finset.affineCombination ((fun a => k) x) Finset.univ (↑(coord b j) ∘ ↑b₂)) fun i => ↑(coord b₂ i) x
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j =
    ↑(coord b j) (↑(Finset.affineCombination k Finset.univ ↑b₂) fun i => ↑(coord b₂ i) x)
rw [Finset.map_affineCombination _ _ _ (b₂.sum_coord_apply_eq_one x)]
no goals
case h
ι : 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.37207
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j =
    ↑(Finset.affineCombination ((fun a => k) x) Finset.univ (↑(coord b j) ∘ ↑b₂)) fun i => ↑(coord b₂ i) x
simp [Matrix.vecMul, Matrix.dotProduct, toMatrix_apply, coords]