case h
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a a' : α
⊢ ↑(erase a f) a' = ↑(f - single a (↑f a)) a'
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ erase a f = f - single a (↑f a)
ext a'
case h.inl
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ ↑(erase a f) a = ↑(f - single a (↑f a)) a

case h.inr
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a a' : α
h : a ≠ a'
⊢ ↑(erase a f) a' = ↑(f - single a (↑f a)) a'
case h
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a a' : α
⊢ ↑(erase a f) a' = ↑(f - single a (↑f a)) a'
rcases eq_or_ne a a' with (rfl | h)
no goals
case h.inl
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a : α
⊢ ↑(erase a f) a = ↑(f - single a (↑f a)) a
simp
no goals
case h.inr
α : Type u_2
β : Type ?u.560593
γ : Type ?u.560596
ι : Type ?u.560599
M : Type ?u.560602
M' : Type ?u.560605
N : Type ?u.560608
P : Type ?u.560611
G : Type u_1
H : Type ?u.560617
R : Type ?u.560620
S : Type ?u.560623
inst✝ : AddGroup G
f : α →₀ G
a a' : α
h : a ≠ a'
⊢ ↑(erase a f) a' = ↑(f - single a (↑f a)) a'
simp [erase_ne h.symm, single_eq_of_ne h]