Lean4
/-- Create a finitely supported function from a total function by taking the default value to
zero. -/
def applyFinsupp (tf : TotalFunction α β) : α →₀ β
where
support := zeroDefaultSupp tf
toFun := tf.zeroDefault.apply
mem_support_toFun := by
intro a
rcases tf with ⟨A, y⟩
simp only [zeroDefaultSupp, List.mem_map, List.mem_filter, exists_and_right, List.mem_toFinset, exists_eq_right,
Sigma.exists, Ne, zeroDefault]
rw [apply_eq_dlookup]
constructor
· rintro ⟨od, hval, hod⟩
have := List.mem_dlookup (List.nodupKeys_dedupKeys A) hval
rw [(_ : List.dlookup a A = od)]
· simpa using hod
· simpa [List.dlookup_dedupKeys]
· intro h
use (A.dlookup a).getD (0 : β)
rw [← List.dlookup_dedupKeys] at h ⊢
simp only [h, ← List.mem_dlookup_iff A.nodupKeys_dedupKeys, not_false_iff, Option.mem_def]
cases haA : List.dlookup a A.dedupKeys
· simp [haA] at h
· simp
