case a.h
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
⊢ toBlock (diagonal d) p p = diagonal fun i => d ↑i
ext (i j)
case pos
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j

case neg
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
case a.h
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
by_cases i = j
no goals
case pos
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
simp [h]
no goals
case neg
l : Type ?u.113198
m : Type u_1
n : Type ?u.113204
o : Type ?u.113207
p✝ : Type ?u.113210
q : Type ?u.113213
m' : o → Type ?u.113218
n' : o → Type ?u.113223
p' : o → Type ?u.113228
R : Type ?u.113231
S : Type ?u.113234
α : Type u_2
β : Type ?u.113240
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ toBlock (diagonal d) p p i j = diagonal (fun i => d ↑i) i j
simp [One.one, h, Subtype.val_injective.ne h]