case a.mk.h.mk
R : Type ?u.13740
α : Type u_1
α' : Type ?u.13746
β : Type u_6
β' : Type ?u.13752
γ : Type u_2
γ' : Type ?u.13758
l : Type u_3
m : Type u_4
n : Type u_5
p : Type ?u.13770
q : Type ?u.13773
r : Type ?u.13776
l' : Type ?u.13779
m' : Type ?u.13782
n' : Type ?u.13785
p' : Type ?u.13788
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b) (i₁, i₂)
      (j₁, j₂)
R : Type ?u.13740
α : Type u_1
α' : Type ?u.13746
β : Type u_6
β' : Type ?u.13752
γ : Type u_2
γ' : Type ?u.13758
l : Type u_3
m : Type u_4
n : Type u_5
p : Type ?u.13770
q : Type ?u.13773
r : Type ?u.13776
l' : Type ?u.13779
m' : Type ?u.13782
n' : Type ?u.13785
p' : Type ?u.13788
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b)
ext (⟨i₁, i₂⟩⟨j₁, j₂⟩)
no goals
case a.mk.h.mk
R : Type ?u.13740
α : Type u_1
α' : Type ?u.13746
β : Type u_6
β' : Type ?u.13752
γ : Type u_2
γ' : Type ?u.13758
l : Type u_3
m : Type u_4
n : Type u_5
p : Type ?u.13770
q : Type ?u.13773
r : Type ?u.13776
l' : Type ?u.13779
m' : Type ?u.13782
n' : Type ?u.13785
p' : Type ?u.13788
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    ↑(reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i => map B fun b => f (a i) b) (i₁, i₂)
      (j₁, j₂)
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]