case h
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
⊢ erase a (f + f') = erase a f + erase a f'
ext s
case pos
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : s = a
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s

case neg
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : ¬s = a
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
case h
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
by_cases hs : s = a
no goals
case neg
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : ¬s = a
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
no goals
case pos
α : Type u_1
β : Type ?u.310309
γ : Type ?u.310312
ι : Type ?u.310315
M : Type u_2
M' : Type ?u.310321
N : Type ?u.310324
P : Type ?u.310327
G : Type ?u.310330
H : Type ?u.310333
R : Type ?u.310336
S : Type ?u.310339
inst✝ : AddZeroClass M
a : α
f f' : α →₀ M
s : α
hs : s = a
⊢ ↑(erase a (f + f')) s = ↑(erase a f + erase a f') s
rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]