case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ lookupFinsupp (Finsupp.toAList f) = f
ext a
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a

case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
by_cases h : f a = 0
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ lookup a (Finsupp.toAList f) = none
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
suffices f.toAList.lookup a = none by simp [h, this]
no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
this : lookup a (Finsupp.toAList f) = none
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
simp [h, this]
no goals
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ lookup a (Finsupp.toAList f) = none
simp [lookup_eq_none, h]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ lookup a (Finsupp.toAList f) = some (↑f a)
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
suffices f.toAList.lookup a = some (f a) by simp [h, this]
no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
this : lookup a (Finsupp.toAList f) = some (↑f a)
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
simp [h, this]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ { fst := a, snd := ↑f a } ∈ (Finsupp.toAList f).entries
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ lookup a (Finsupp.toAList f) = some (↑f a)
apply mem_lookup_iff.2
no goals
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ { fst := a, snd := ↑f a } ∈ (Finsupp.toAList f).entries
simpa using h