Lean4
/-- Given `f : α ↪ β` and `v : α →₀ M`, `Finsupp.embDomain f v : β →₀ M`
is the finitely supported function whose value at `f a : β` is `v a`.
For a `b : β` outside the range of `f`, it is zero. -/
def embDomain (f : α ↪ β) (v : α →₀ M) : β →₀ M
where
support := v.support.map f
toFun
a₂ :=
haveI := Classical.decEq β
if h : a₂ ∈ v.support.map f then
v
(v.support.choose (fun a₁ => f a₁ = a₂)
(by
rcases Finset.mem_map.1 h with ⟨a, ha, rfl⟩
exact ExistsUnique.intro a ⟨ha, rfl⟩ fun b ⟨_, hb⟩ => f.injective hb))
else 0
mem_support_toFun
a₂ := by
dsimp
split_ifs with h
· simp only [h, true_iff]
rw [← notMem_support_iff, not_not]
classical apply Finset.choose_mem
· simp only [h, not_true_eq_false]
