Lean4
/-- The natural map between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`. -/
def sigmaCurry [∀ i j, Zero (δ i j)] (f : Π₀ (i : Σ _, _), δ i.1 i.2) : Π₀ (i) (j), δ i j
where
toFun := fun i ↦
{ toFun := fun j ↦ f ⟨i, j⟩,
support' :=
f.support'.map
(fun ⟨m, hm⟩ ↦
⟨m.filterMap (fun ⟨i', j'⟩ ↦ if h : i' = i then some <| h.rec j' else none), fun j ↦
(hm ⟨i, j⟩).imp_left (fun h ↦ (m.mem_filterMap _).mpr ⟨⟨i, j⟩, h, dif_pos rfl⟩)⟩) }
support' :=
f.support'.map
(fun ⟨m, hm⟩ ↦
⟨m.map Sigma.fst, fun i ↦
Decidable.or_iff_not_imp_left.mpr
(fun h ↦
DFinsupp.ext (fun j ↦ (hm ⟨i, j⟩).resolve_left (fun H ↦ (Multiset.mem_map.not.mp h) ⟨⟨i, j⟩, H, rfl⟩)))⟩)
