case inl
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ blockDiag (diagonal d) k i i = diagonal (fun i => d (i, k)) i i

case inr
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ blockDiag (diagonal d) k i j = diagonal (fun i => d (i, k)) i j
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
⊢ blockDiag (diagonal d) k i j = diagonal (fun i => d (i, k)) i j
obtain rfl | hij := Decidable.eq_or_ne i j
no goals
case inl
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ blockDiag (diagonal d) k i i = diagonal (fun i => d (i, k)) i i
rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j
case inr
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ blockDiag (diagonal d) k i j = diagonal (fun i => d (i, k)) i j
rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
no goals
l : Type ?u.178877
m : Type u_2
n : Type ?u.178883
o : Type u_1
p : Type ?u.178889
q : Type ?u.178892
m' : o → Type ?u.178897
n' : o → Type ?u.178902
p' : o → Type ?u.178907
R : Type ?u.178910
S : Type ?u.178913
α : Type u_3
β : Type ?u.178919
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j
exact Prod.fst_eq_iff.mpr