-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem Basis.toMatrix_mul_toMatrix {ι'' : Type*} [Fintype ι'] (b'' : ι'' → M) :
    b.toMatrix b' * b'.toMatrix b'' = b.toMatrix b''

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
i : ι
j : ι''
⊢ (b.toMatrix ⇑b' * b'.toMatrix b'') i j = b.toMatrix b'' i j

Tactic:
simp only [Matrix.mul_apply, Basis.toMatrix_apply, Basis.sum_repr_mul_repr]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝ : DecidableEq ι
this : DecidableEq ι'
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Tactic:
haveI := Classical.decEq ι''

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Tactic:
haveI := Classical.decEq ι

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this : DecidableEq ι
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this : DecidableEq ι
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Tactic:
haveI := Classical.decEq ι'

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝ : DecidableEq ι
this : DecidableEq ι'
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
⊢ b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''

Tactic:
ext i j

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
i : ι
j : ι''
⊢ (b.toMatrix ⇑b' * b'.toMatrix b'') i j = b.toMatrix b'' i j