case mk
l : Type ?u.196229
m : Type ?u.196232
n : Type ?u.196235
o : Type u_4
p : Type ?u.196241
q : Type ?u.196244
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.196259
R : Type ?u.196262
S : Type ?u.196265
α : Type u_3
β : Type ?u.196271
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
jk : (i : o) × n' i
fst✝ : o
snd✝ : m' fst✝
⊢ blockDiagonal' M { fst := fst✝, snd := snd✝ } jk =
    if h : { fst := fst✝, snd := snd✝ }.fst = jk.fst then
      M { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd
        (cast (_ : n' jk.fst = n' { fst := fst✝, snd := snd✝ }.fst) jk.snd)
    else 0
l : Type ?u.196229
m : Type ?u.196232
n : Type ?u.196235
o : Type u_4
p : Type ?u.196241
q : Type ?u.196244
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.196259
R : Type ?u.196262
S : Type ?u.196265
α : Type u_3
β : Type ?u.196271
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
ik : (i : o) × m' i
jk : (i : o) × n' i
⊢ blockDiagonal' M ik jk = if h : ik.fst = jk.fst then M ik.fst ik.snd (cast (_ : n' jk.fst = n' ik.fst) jk.snd) else 0
cases ik
case mk.mk
l : Type ?u.196229
m : Type ?u.196232
n : Type ?u.196235
o : Type u_4
p : Type ?u.196241
q : Type ?u.196244
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.196259
R : Type ?u.196262
S : Type ?u.196265
α : Type u_3
β : Type ?u.196271
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
fst✝¹ : o
snd✝¹ : m' fst✝¹
fst✝ : o
snd✝ : n' fst✝
⊢ blockDiagonal' M { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ } =
    if h : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst then
      M { fst := fst✝¹, snd := snd✝¹ }.fst { fst := fst✝¹, snd := snd✝¹ }.snd
        (cast (_ : n' { fst := fst✝, snd := snd✝ }.fst = n' { fst := fst✝¹, snd := snd✝¹ }.fst)
          { fst := fst✝, snd := snd✝ }.snd)
    else 0
case mk
l : Type ?u.196229
m : Type ?u.196232
n : Type ?u.196235
o : Type u_4
p : Type ?u.196241
q : Type ?u.196244
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.196259
R : Type ?u.196262
S : Type ?u.196265
α : Type u_3
β : Type ?u.196271
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
jk : (i : o) × n' i
fst✝ : o
snd✝ : m' fst✝
⊢ blockDiagonal' M { fst := fst✝, snd := snd✝ } jk =
    if h : { fst := fst✝, snd := snd✝ }.fst = jk.fst then
      M { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd
        (cast (_ : n' jk.fst = n' { fst := fst✝, snd := snd✝ }.fst) jk.snd)
    else 0
cases jk
no goals
case mk.mk
l : Type ?u.196229
m : Type ?u.196232
n : Type ?u.196235
o : Type u_4
p : Type ?u.196241
q : Type ?u.196244
m' : o → Type u_1
n' : o → Type u_2
p' : o → Type ?u.196259
R : Type ?u.196262
S : Type ?u.196265
α : Type u_3
β : Type ?u.196271
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
fst✝¹ : o
snd✝¹ : m' fst✝¹
fst✝ : o
snd✝ : n' fst✝
⊢ blockDiagonal' M { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ } =
    if h : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst then
      M { fst := fst✝¹, snd := snd✝¹ }.fst { fst := fst✝¹, snd := snd✝¹ }.snd
        (cast (_ : n' { fst := fst✝, snd := snd✝ }.fst = n' { fst := fst✝¹, snd := snd✝¹ }.fst)
          { fst := fst✝, snd := snd✝ }.snd)
    else 0
rfl