no goals
α : Type u_1
β : Type ?u.164124
γ : Type ?u.164127
ι : Type ?u.164130
M : Type u_2
M' : Type ?u.164136
N : Type ?u.164139
P : Type ?u.164142
G : Type ?u.164145
H : Type ?u.164148
R : Type ?u.164151
S : Type ?u.164154
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ ↑(erase a f) a' = ↑f a'
classical simp only [erase, coe_mk, h, ite_false]
no goals
α : Type u_1
β : Type ?u.164124
γ : Type ?u.164127
ι : Type ?u.164130
M : Type u_2
M' : Type ?u.164136
N : Type ?u.164139
P : Type ?u.164142
G : Type ?u.164145
H : Type ?u.164148
R : Type ?u.164151
S : Type ?u.164154
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ ↑(erase a f) a' = ↑f a'
simp only [erase, coe_mk, h, ite_false]