no goals
α : Type u_1
β : Type ?u.167346
γ : Type ?u.167349
ι : Type ?u.167352
M : Type u_2
M' : Type ?u.167358
N : Type ?u.167361
P : Type ?u.167364
G : Type ?u.167367
H : Type ?u.167370
R : Type ?u.167373
S : Type ?u.167376
inst✝ : Zero M
a : α
⊢ erase a 0 = 0
classical rw [← support_eq_empty, support_erase, support_zero, erase_empty]
no goals
α : Type u_1
β : Type ?u.167346
γ : Type ?u.167349
ι : Type ?u.167352
M : Type u_2
M' : Type ?u.167358
N : Type ?u.167361
P : Type ?u.167364
G : Type ?u.167367
H : Type ?u.167370
R : Type ?u.167373
S : Type ?u.167376
inst✝ : Zero M
a : α
⊢ erase a 0 = 0
rw [← support_eq_empty, support_erase, support_zero, erase_empty]