case a.mk.h.mk
l : Type ?u.115337
m : Type u_1
n : Type ?u.115343
o : Type ?u.115346
p✝ : Type ?u.115349
q✝ : Type ?u.115352
m' : o → Type ?u.115357
n' : o → Type ?u.115362
p' : o → Type ?u.115367
R : Type ?u.115370
S : Type ?u.115373
α : Type u_2
β : Type ?u.115379
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ toBlock (diagonal d) p q { val := i, property := hi } { val := j, property := hj } =
    OfNat.ofNat 0 { val := i, property := hi } { val := j, property := hj }
l : Type ?u.115337
m : Type u_1
n : Type ?u.115343
o : Type ?u.115346
p✝ : Type ?u.115349
q✝ : Type ?u.115352
m' : o → Type ?u.115357
n' : o → Type ?u.115362
p' : o → Type ?u.115367
R : Type ?u.115370
S : Type ?u.115373
α : Type u_2
β : Type ?u.115379
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
⊢ toBlock (diagonal d) p q = 0
ext (⟨i, hi⟩⟨j, hj⟩)
case a.mk.h.mk
l : Type ?u.115337
m : Type u_1
n : Type ?u.115343
o : Type ?u.115346
p✝ : Type ?u.115349
q✝ : Type ?u.115352
m' : o → Type ?u.115357
n' : o → Type ?u.115362
p' : o → Type ?u.115367
R : Type ?u.115370
S : Type ?u.115373
α : Type u_2
β : Type ?u.115379
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ toBlock (diagonal d) p q { val := i, property := hi } { val := j, property := hj } =
    OfNat.ofNat 0 { val := i, property := hi } { val := j, property := hj }
case a.mk.h.mk
l : Type ?u.115337
m : Type u_1
n : Type ?u.115343
o : Type ?u.115346
p✝ : Type ?u.115349
q✝ : Type ?u.115352
m' : o → Type ?u.115357
n' : o → Type ?u.115362
p' : o → Type ?u.115367
R : Type ?u.115370
S : Type ?u.115373
α : Type u_2
β : Type ?u.115379
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ toBlock (diagonal d) p q { val := i, property := hi } { val := j, property := hj } =
    OfNat.ofNat 0 { val := i, property := hi } { val := j, property := hj }
have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩
no goals
case a.mk.h.mk
l : Type ?u.115337
m : Type u_1
n : Type ?u.115343
o : Type ?u.115346
p✝ : Type ?u.115349
q✝ : Type ?u.115352
m' : o → Type ?u.115357
n' : o → Type ?u.115362
p' : o → Type ?u.115367
R : Type ?u.115370
S : Type ?u.115373
α : Type u_2
β : Type ?u.115379
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ toBlock (diagonal d) p q { val := i, property := hi } { val := j, property := hj } =
    OfNat.ofNat 0 { val := i, property := hi } { val := j, property := hj }
simp [diagonal_apply_ne d this]