case h
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
⊢ ↑(erase a f) b = ↑f b
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
⊢ erase a f = f
ext b
case pos
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
hab : b = a
⊢ ↑(erase a f) b = ↑f b

case neg
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
hab : ¬b = a
⊢ ↑(erase a f) b = ↑f b
case h
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
⊢ ↑(erase a f) b = ↑f b
by_cases hab : b = a
no goals
case pos
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
hab : b = a
⊢ ↑(erase a f) b = ↑f b
rwa [hab, erase_same, eq_comm, ← not_mem_support_iff]
no goals
case neg
α : Type u_1
β : Type ?u.166602
γ : Type ?u.166605
ι : Type ?u.166608
M : Type u_2
M' : Type ?u.166614
N : Type ?u.166617
P : Type ?u.166620
G : Type ?u.166623
H : Type ?u.166626
R : Type ?u.166629
S : Type ?u.166632
inst✝ : Zero M
f : α →₀ M
a : α
haf : ¬a ∈ f.support
b : α
hab : ¬b = a
⊢ ↑(erase a f) b = ↑f b
rw [erase_ne hab]