α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ ↑{ support := if b = 0 then erase f.support a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1,
        mem_support_toFun :=
          (_ :
            ∀ (i : α),
              (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0) } =
    fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1
α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ ↑(update f a b) = Function.update (↑f) a b
delta update Function.update
case h
α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
⊢ ↑{ support := if b = 0 then erase f.support a else insert a f.support,
          toFun := fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1,
          mem_support_toFun :=
            (_ :
              ∀ (i : α),
                (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0) }
      x✝ =
    if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝
α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
⊢ ↑{ support := if b = 0 then erase f.support a else insert a f.support,
        toFun := fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1,
        mem_support_toFun :=
          (_ :
            ∀ (i : α),
              (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0) } =
    fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1
ext
case h
α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
⊢ (if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝) = if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝
case h
α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
⊢ ↑{ support := if b = 0 then erase f.support a else insert a f.support,
          toFun := fun a_1 => if h : a_1 = a then (_ : a = a_1) ▸ b else ↑f a_1,
          mem_support_toFun :=
            (_ :
              ∀ (i : α),
                (i ∈ if b = 0 then erase f.support a else insert a f.support) ↔ Function.update (↑f) a b i ≠ 0) }
      x✝ =
    if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝
dsimp
no goals
case h
α : Type u_1
β : Type ?u.147517
γ : Type ?u.147520
ι : Type ?u.147523
M : Type u_2
M' : Type ?u.147529
N : Type ?u.147532
P : Type ?u.147535
G : Type ?u.147538
H : Type ?u.147541
R : Type ?u.147544
S : Type ?u.147547
inst✝¹ : Zero M
f : α →₀ M
a : α
b : M
i : α
inst✝ : DecidableEq α
x✝ : α
⊢ (if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝) = if h : x✝ = a then (_ : a = x✝) ▸ b else ↑f x✝
split_ifs <;> simp