case a.h
l : Type ?u.140829
m : Type u_2
n : Type u_3
o : Type u_4
p : Type ?u.140841
q : Type ?u.140844
m' : o → Type ?u.140849
n' : o → Type ?u.140854
p' : o → Type ?u.140859
R : Type ?u.140862
S : Type ?u.140865
α : Type u_1
β : Type ?u.140871
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ blockDiagonal (M + N) i✝ x✝ = (blockDiagonal M + blockDiagonal N) i✝ x✝
l : Type ?u.140829
m : Type u_2
n : Type u_3
o : Type u_4
p : Type ?u.140841
q : Type ?u.140844
m' : o → Type ?u.140849
n' : o → Type ?u.140854
p' : o → Type ?u.140859
R : Type ?u.140862
S : Type ?u.140865
α : Type u_1
β : Type ?u.140871
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N
ext
case a.h
l : Type ?u.140829
m : Type u_2
n : Type u_3
o : Type u_4
p : Type ?u.140841
q : Type ?u.140844
m' : o → Type ?u.140849
n' : o → Type ?u.140854
p' : o → Type ?u.140859
R : Type ?u.140862
S : Type ?u.140865
α : Type u_1
β : Type ?u.140871
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst + N i✝.snd i✝.fst x✝.fst else 0) =
    (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0) + if i✝.snd = x✝.snd then N i✝.snd i✝.fst x✝.fst else 0
case a.h
l : Type ?u.140829
m : Type u_2
n : Type u_3
o : Type u_4
p : Type ?u.140841
q : Type ?u.140844
m' : o → Type ?u.140849
n' : o → Type ?u.140854
p' : o → Type ?u.140859
R : Type ?u.140862
S : Type ?u.140865
α : Type u_1
β : Type ?u.140871
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ 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.140829
m : Type u_2
n : Type u_3
o : Type u_4
p : Type ?u.140841
q : Type ?u.140844
m' : o → Type ?u.140849
n' : o → Type ?u.140854
p' : o → Type ?u.140859
R : Type ?u.140862
S : Type ?u.140865
α : Type u_1
β : Type ?u.140871
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
x✝ : n × o
⊢ (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst + N i✝.snd i✝.fst x✝.fst else 0) =
    (if i✝.snd = x✝.snd then M i✝.snd i✝.fst x✝.fst else 0) + if i✝.snd = x✝.snd then N i✝.snd i✝.fst x✝.fst else 0
split_ifs <;> simp