case a.mk.h.mk
l : Type ?u.153048
m : Type u_4
n : Type u_1
o : Type u_2
p : Type u_5
q : Type ?u.153063
m' : o → Type ?u.153068
n' : o → Type ?u.153073
p' : o → Type ?u.153078
R : Type ?u.153081
S : Type ?u.153084
α : Type u_3
β : Type ?u.153090
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ blockDiagonal (fun k => M k ⬝ N k) (i, k) (j, k') = (blockDiagonal M ⬝ blockDiagonal N) (i, k) (j, k')
l : Type ?u.153048
m : Type u_4
n : Type u_1
o : Type u_2
p : Type u_5
q : Type ?u.153063
m' : o → Type ?u.153068
n' : o → Type ?u.153073
p' : o → Type ?u.153078
R : Type ?u.153081
S : Type ?u.153084
α : Type u_3
β : Type ?u.153090
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
⊢ (blockDiagonal fun k => M k ⬝ N k) = blockDiagonal M ⬝ blockDiagonal N
ext (⟨i, k⟩ ⟨j, k'⟩)
case a.mk.h.mk
l : Type ?u.153048
m : Type u_4
n : Type u_1
o : Type u_2
p : Type u_5
q : Type ?u.153063
m' : o → Type ?u.153068
n' : o → Type ?u.153073
p' : o → Type ?u.153078
R : Type ?u.153081
S : Type ?u.153084
α : Type u_3
β : Type ?u.153090
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0) =
    ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
case a.mk.h.mk
l : Type ?u.153048
m : Type u_4
n : Type u_1
o : Type u_2
p : Type u_5
q : Type ?u.153063
m' : o → Type ?u.153068
n' : o → Type ?u.153073
p' : o → Type ?u.153078
R : Type ?u.153081
S : Type ?u.153084
α : Type u_3
β : Type ?u.153090
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ blockDiagonal (fun k => M k ⬝ N k) (i, k) (j, k') = (blockDiagonal M ⬝ blockDiagonal N) (i, k) (j, k')
simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]
no goals
case a.mk.h.mk
l : Type ?u.153048
m : Type u_4
n : Type u_1
o : Type u_2
p : Type u_5
q : Type ?u.153063
m' : o → Type ?u.153068
n' : o → Type ?u.153073
p' : o → Type ?u.153078
R : Type ?u.153081
S : Type ?u.153084
α : Type u_3
β : Type ?u.153090
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
⊢ (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0) =
    ∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0
split_ifs with h <;> simp [h]