case inl
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ blockDiag' (diagonal d) k i i = diagonal (fun i => d { fst := k, snd := i }) i i

case inr
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ blockDiag' (diagonal d) k i j = diagonal (fun i => d { fst := k, snd := i }) i j
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
⊢ blockDiag' (diagonal d) k i j = diagonal (fun i => d { fst := k, snd := i }) i j
obtain rfl | hij := Decidable.eq_or_ne i j
no goals
case inl
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ blockDiag' (diagonal d) k i i = diagonal (fun i => d { fst := k, snd := i }) i i
rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : { fst := k, snd := i } = { fst := k, snd := j }
⊢ i = j
case inr
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ blockDiag' (diagonal d) k i j = diagonal (fun i => d { fst := k, snd := i }) i j
rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]
case refl
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : { fst := k, snd := i } = { fst := k, snd := j }
⊢ i = j
cases h
no goals
case refl
l : Type ?u.250274
m : Type ?u.250277
n : Type ?u.250280
o : Type u_1
p : Type ?u.250286
q : Type ?u.250289
m' : o → Type u_2
n' : o → Type ?u.250299
p' : o → Type ?u.250304
R : Type ?u.250307
S : Type ?u.250310
α : Type u_3
β : Type ?u.250316
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i
rfl