no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ lookupFinsupp ∅ = 0
classical
  ext
  simp
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ ↑(lookupFinsupp ∅) a✝ = ↑0 a✝
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ lookupFinsupp ∅ = 0
ext
no goals
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ ↑(lookupFinsupp ∅) a✝ = ↑0 a✝
simp