case a.h
l : Type ?u.212538
m : Type ?u.212541
n : Type ?u.212544
o : Type u_4
p : Type ?u.212550
q : Type ?u.212553
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.212568
R : Type ?u.212571
S : Type ?u.212574
α : Type u_1
β : Type ?u.212580
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' (M + N) i✝ x✝ = (blockDiagonal' M + blockDiagonal' N) i✝ x✝
l : Type ?u.212538
m : Type ?u.212541
n : Type ?u.212544
o : Type u_4
p : Type ?u.212550
q : Type ?u.212553
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.212568
R : Type ?u.212571
S : Type ?u.212574
α : Type u_1
β : Type ?u.212580
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N
ext
case a.h
l : Type ?u.212538
m : Type ?u.212541
n : Type ?u.212544
o : Type u_4
p : Type ?u.212550
q : Type ?u.212553
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.212568
R : Type ?u.212571
S : Type ?u.212574
α : Type u_1
β : Type ?u.212580
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ (if h : i✝.fst = x✝.fst then
      M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) +
        N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)
    else 0) =
    (if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) +
      if h : i✝.fst = x✝.fst then N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0
case a.h
l : Type ?u.212538
m : Type ?u.212541
n : Type ?u.212544
o : Type u_4
p : Type ?u.212550
q : Type ?u.212553
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.212568
R : Type ?u.212571
S : Type ?u.212574
α : Type u_1
β : Type ?u.212580
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ blockDiagonal' (M + N) i✝ x✝ = (blockDiagonal' M + blockDiagonal' N) i✝ x✝
simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]
no goals
case a.h
l : Type ?u.212538
m : Type ?u.212541
n : Type ?u.212544
o : Type u_4
p : Type ?u.212550
q : Type ?u.212553
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.212568
R : Type ?u.212571
S : Type ?u.212574
α : Type u_1
β : Type ?u.212580
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
x✝ : (i : o) × n' i
⊢ (if h : i✝.fst = x✝.fst then
      M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) +
        N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd)
    else 0) =
    (if h : i✝.fst = x✝.fst then M i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0) +
      if h : i✝.fst = x✝.fst then N i✝.fst i✝.snd (cast (_ : n' x✝.fst = n' i✝.fst) x✝.snd) else 0
split_ifs <;> simp