case a.mk.h.mk
R : Type ?u.19536
α : Type u_9
α' : Type ?u.19542
β : Type u_10
β' : Type ?u.19548
γ : Type u_11
γ' : Type ?u.19554
l : Type u_1
m : Type u_3
n : Type u_5
p : Type u_7
q : Type ?u.19569
r : Type ?u.19572
l' : Type u_2
m' : Type u_4
n' : Type u_6
p' : Type u_8
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) (i, i') (j, j') =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N) (i, i') (j, j')
R : Type ?u.19536
α : Type u_9
α' : Type ?u.19542
β : Type u_10
β' : Type ?u.19548
γ : Type u_11
γ' : Type ?u.19554
l : Type u_1
m : Type u_3
n : Type u_5
p : Type u_7
q : Type ?u.19569
r : Type ?u.19572
l' : Type u_2
m' : Type u_4
n' : Type u_6
p' : Type u_8
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N)
ext (⟨i, i'⟩⟨j, j'⟩)
no goals
case a.mk.h.mk
R : Type ?u.19536
α : Type u_9
α' : Type ?u.19542
β : Type u_10
β' : Type ?u.19548
γ : Type u_11
γ' : Type ?u.19554
l : Type u_1
m : Type u_3
n : Type u_5
p : Type u_7
q : Type ?u.19569
r : Type ?u.19572
l' : Type u_2
m' : Type u_4
n' : Type u_6
p' : Type u_8
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f (↑(reindex el em) M) (↑(reindex en ep) N) (i, i') (j, j') =
    ↑(reindex (Equiv.prodCongr el en) (Equiv.prodCongr em ep)) (kroneckerMap f M N) (i, i') (j, j')
rfl