Lean4
/-- The natural map between `Π₀ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
`curry`. -/
def sigmaUncurry [∀ i j, Zero (δ i j)] [DecidableEq ι] (f : Π₀ (i) (j), δ i j) : Π₀ i : Σ _, _, δ i.1 i.2
where
toFun i := f i.1 i.2
support' :=
f.support'.bind fun s =>
(Trunc.finChoice (fun i : ↥s.val.toFinset => (f i).support')).map fun fs =>
⟨s.val.toFinset.attach.val.bind fun i => (fs i).val.map (Sigma.mk i.val),
by
rintro ⟨i, a⟩
cases s.prop i with
| inl hi =>
cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
| inl ha =>
left; rw [Multiset.mem_bind]
use ⟨i, Multiset.mem_toFinset.mpr hi⟩
constructor
case right => simp [ha]
case left => apply Multiset.mem_attach
| inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]
| inr hi => right; simp [toFun_eq_coe f ▸ hi]⟩
