no goals
α : Type u_1
β : Type ?u.149402
γ : Type ?u.149405
ι : Type ?u.149408
M : Type u_2
M' : Type ?u.149414
N : Type ?u.149417
P : Type ?u.149420
G : Type ?u.149423
H : Type ?u.149426
R : Type ?u.149429
S : Type ?u.149432
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update 0 a b = single a b
classical
  ext
  rw [single_eq_update]
  rfl
case h
α : Type u_1
β : Type ?u.149402
γ : Type ?u.149405
ι : Type ?u.149408
M : Type u_2
M' : Type ?u.149414
N : Type ?u.149417
P : Type ?u.149420
G : Type ?u.149423
H : Type ?u.149426
R : Type ?u.149429
S : Type ?u.149432
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update 0 a b) a✝ = ↑(single a b) a✝
α : Type u_1
β : Type ?u.149402
γ : Type ?u.149405
ι : Type ?u.149408
M : Type u_2
M' : Type ?u.149414
N : Type ?u.149417
P : Type ?u.149420
G : Type ?u.149423
H : Type ?u.149426
R : Type ?u.149429
S : Type ?u.149432
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i : α
⊢ update 0 a b = single a b
ext
case h
α : Type u_1
β : Type ?u.149402
γ : Type ?u.149405
ι : Type ?u.149408
M : Type u_2
M' : Type ?u.149414
N : Type ?u.149417
P : Type ?u.149420
G : Type ?u.149423
H : Type ?u.149426
R : Type ?u.149429
S : Type ?u.149432
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update 0 a b) a✝ = Function.update 0 a b a✝
case h
α : Type u_1
β : Type ?u.149402
γ : Type ?u.149405
ι : Type ?u.149408
M : Type u_2
M' : Type ?u.149414
N : Type ?u.149417
P : Type ?u.149420
G : Type ?u.149423
H : Type ?u.149426
R : Type ?u.149429
S : Type ?u.149432
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update 0 a b) a✝ = ↑(single a b) a✝
rw [single_eq_update]
no goals
case h
α : Type u_1
β : Type ?u.149402
γ : Type ?u.149405
ι : Type ?u.149408
M : Type u_2
M' : Type ?u.149414
N : Type ?u.149417
P : Type ?u.149420
G : Type ?u.149423
H : Type ?u.149426
R : Type ?u.149429
S : Type ?u.149432
inst✝ : Zero M
f : α →₀ M
a : α
b : M
i a✝ : α
⊢ ↑(update 0 a b) a✝ = Function.update 0 a b a✝
rfl