case h
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
⊢ ↑(erase a (single a b)) s = ↑0 s
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
⊢ erase a (single a b) = 0
ext s
case pos
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ ↑(erase a (single a b)) s = ↑0 s

case neg
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ ↑(erase a (single a b)) s = ↑0 s
case h
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
⊢ ↑(erase a (single a b)) s = ↑0 s
by_cases hs : s = a
case pos
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ 0 = ↑0 a
case pos
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ ↑(erase a (single a b)) s = ↑0 s
rw [hs, erase_same]
no goals
case pos
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ 0 = ↑0 a
rfl
case neg
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ ↑(single a b) s = ↑0 s
case neg
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ ↑(erase a (single a b)) s = ↑0 s
rw [erase_ne hs]
no goals
case neg
α : Type u_1
β : Type ?u.165062
γ : Type ?u.165065
ι : Type ?u.165068
M : Type u_2
M' : Type ?u.165074
N : Type ?u.165077
P : Type ?u.165080
G : Type ?u.165083
H : Type ?u.165086
R : Type ?u.165089
S : Type ?u.165092
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ ↑(single a b) s = ↑0 s
exact single_eq_of_ne (Ne.symm hs)