no goals
α : Type u_1
β : Type ?u.148539
γ : Type ?u.148542
ι : Type ?u.148545
M : Type u_2
M' : Type ?u.148551
N : Type ?u.148554
P : Type ?u.148557
G : Type ?u.148560
H : Type ?u.148563
R : Type ?u.148566
S : Type ?u.148569
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update f a (↑f a) = f
classical
  ext
  simp
case h
α : Type u_1
β : Type ?u.148539
γ : Type ?u.148542
ι : Type ?u.148545
M : Type u_2
M' : Type ?u.148551
N : Type ?u.148554
P : Type ?u.148557
G : Type ?u.148560
H : Type ?u.148563
R : Type ?u.148566
S : Type ?u.148569
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update f a (↑f a)) a✝ = ↑f a✝
α : Type u_1
β : Type ?u.148539
γ : Type ?u.148542
ι : Type ?u.148545
M : Type u_2
M' : Type ?u.148551
N : Type ?u.148554
P : Type ?u.148557
G : Type ?u.148560
H : Type ?u.148563
R : Type ?u.148566
S : Type ?u.148569
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update f a (↑f a) = f
ext
no goals
case h
α : Type u_1
β : Type ?u.148539
γ : Type ?u.148542
ι : Type ?u.148545
M : Type u_2
M' : Type ?u.148551
N : Type ?u.148554
P : Type ?u.148557
G : Type ?u.148560
H : Type ?u.148563
R : Type ?u.148566
S : Type ?u.148569
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update f a (↑f a)) a✝ = ↑f a✝
simp