case inl.inl
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i j : m
hij : Sum.inl i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0

case inl.inr
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i : m
j : n
hij : Sum.inl i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inr j) = 0

case inr.inl
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i : n
j : m
hij : Sum.inr i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inl j) = 0

case inr.inr
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i j : n
hij : Sum.inr i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 0 D)
rintro (i | i) (j | j) hij
no goals
case inl.inl
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i j : m
hij : Sum.inl i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0
exact ha (ne_of_apply_ne _ hij)
no goals
case inl.inr
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i : m
j : n
hij : Sum.inl i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inr j) = 0
rfl
no goals
case inr.inl
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i : n
j : m
hij : Sum.inr i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inl j) = 0
rfl
no goals
case inr.inr
α : Type u_1
β : Type ?u.22045
R : Type ?u.22048
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i j : n
hij : Sum.inr i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0
exact hd (ne_of_apply_ne _ hij)