case a.mk.h.mk
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ blockDiagonal (fun k => diagonal (d k)) (i, k) (j, k') = diagonal (fun ik => d ik.snd ik.fst) (i, k) (j, k')
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
⊢ (blockDiagonal fun k => diagonal (d k)) = diagonal fun ik => d ik.snd ik.fst
ext (⟨i, k⟩⟨j, k'⟩)
case a.mk.h.mk
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
case a.mk.h.mk
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ blockDiagonal (fun k => diagonal (d k)) (i, k) (j, k') = diagonal (fun ik => d ik.snd ik.fst) (i, k) (j, k')
simp only [blockDiagonal_apply, diagonal_apply, Prod.mk.inj_iff, ← ite_and]
case a.mk.h.mk.e_c
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')
case a.mk.h.mk
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
congr 1
no goals
case a.mk.h.mk.e_c
l : Type ?u.136326
m : Type u_1
n : Type ?u.136332
o : Type u_2
p : Type ?u.136338
q : Type ?u.136341
m' : o → Type ?u.136346
n' : o → Type ?u.136351
p' : o → Type ?u.136356
R : Type ?u.136359
S : Type ?u.136362
α : Type u_3
β : Type ?u.136368
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')
rw [and_comm]