case a.mk.h.mk
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k => diagonal (d k)) { fst := i, snd := k } { fst := j, snd := k' } =
    diagonal (fun ik => d ik.fst ik.snd) { fst := i, snd := k } { fst := j, snd := k' }
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
⊢ (blockDiagonal' fun k => diagonal (d k)) = diagonal fun ik => d ik.fst ik.snd
ext (⟨i, k⟩⟨j, k'⟩)
case a.mk.h.mk
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ (if h : i = j then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := j, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := j, snd := k' }
case a.mk.h.mk
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ blockDiagonal' (fun k => diagonal (d k)) { fst := i, snd := k } { fst := j, snd := k' } =
    diagonal (fun ik => d ik.fst ik.snd) { fst := i, snd := k } { fst := j, snd := k' }
simp only [blockDiagonal'_apply, diagonal]
case a.mk.h.mk.inl
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := i, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := i, snd := k' }

case a.mk.h.mk.inr
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := j, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := j, snd := k' }
case a.mk.h.mk
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
⊢ (if h : i = j then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := j, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := j, snd := k' }
obtain rfl | hij := Decidable.eq_or_ne i j
no goals
case a.mk.h.mk.inl
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ (if h : i = i then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := i, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := i, snd := k' }
simp
no goals
case a.mk.h.mk.inr
l : Type ?u.205390
m : Type ?u.205393
n : Type ?u.205396
o : Type u_2
p : Type ?u.205402
q : Type ?u.205405
m' : o → Type u_1
n' : o → Type ?u.205415
p' : o → Type ?u.205420
R : Type ?u.205423
S : Type ?u.205426
α : Type u_3
β : Type ?u.205432
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ (if h : i = j then
      ↑of (fun i_1 j => if i_1 = j then d i i_1 else 0) k
        (cast (_ : m' { fst := j, snd := k' }.fst = m' { fst := i, snd := k }.fst) k')
    else 0) =
    ↑of (fun i j => if i = j then d i.fst i.snd else 0) { fst := i, snd := k } { fst := j, snd := k' }
simp [hij]