case h
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ erase a (single a' b) = single a' b
ext s
case pos
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : s = a
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s

case neg
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : ¬s = a
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
case h
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
by_cases hs : s = a
no goals
case pos
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : s = a
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
rw [hs, erase_same, single_eq_of_ne h.symm]
no goals
case neg
α : Type u_1
β : Type ?u.165853
γ : Type ?u.165856
ι : Type ?u.165859
M : Type u_2
M' : Type ?u.165865
N : Type ?u.165868
P : Type ?u.165871
G : Type ?u.165874
H : Type ?u.165877
R : Type ?u.165880
S : Type ?u.165883
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : ¬s = a
⊢ ↑(erase a (single a' b)) s = ↑(single a' b) s
rw [erase_ne hs]