case a.mk.h.mk
R : Type u_1
S : Type u_5
T : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_2
n : Type u_3
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 => ↑(leftMulMatrix b) x) (i, k) (j, k')
R : Type u_1
S : Type u_5
T : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_2
n : Type u_3
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) = blockDiagonal fun x_1 => ↑(leftMulMatrix b) x
ext (⟨i, k⟩⟨j, k'⟩)
case a.mk.h.mk
R : Type u_1
S : Type u_5
T : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_2
n : Type u_3
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst =
    if (i, k).snd = (j, k').snd then ↑(leftMulMatrix b) x (i, k).fst (j, k').fst else 0
case a.mk.h.mk
R : Type u_1
S : Type u_5
T : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_2
n : Type u_3
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 => ↑(leftMulMatrix b) x) (i, k) (j, k')
rw [smul_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
no goals
case a.mk.h.mk
R : Type u_1
S : Type u_5
T : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_2
n : Type u_3
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst =
    if (i, k).snd = (j, k').snd then ↑(leftMulMatrix b) x (i, k).fst (j, k').fst else 0
split_ifs with h <;> simp only at h <;> simp [h]