no goals
α : Type u_1
β : Type ?u.163190
γ : Type ?u.163193
ι : Type ?u.163196
M : Type u_2
M' : Type ?u.163202
N : Type ?u.163205
P : Type ?u.163208
G : Type ?u.163211
H : Type ?u.163214
R : Type ?u.163217
S : Type ?u.163220
inst✝ : Zero M
a : α
f : α →₀ M
⊢ ↑(erase a f) a = 0
classical simp only [erase, coe_mk, ite_true]
no goals
α : Type u_1
β : Type ?u.163190
γ : Type ?u.163193
ι : Type ?u.163196
M : Type u_2
M' : Type ?u.163202
N : Type ?u.163205
P : Type ?u.163208
G : Type ?u.163211
H : Type ?u.163214
R : Type ?u.163217
S : Type ?u.163220
inst✝ : Zero M
a : α
f : α →₀ M
⊢ ↑(erase a f) a = 0
simp only [erase, coe_mk, ite_true]