Lean4
/-- Equivalence between dependent functions with finite support `s : Finset ι` and functions
`∀ i, {x : β i // x ≠ 0}`. -/
@[simps]
def subtypeSupportEqEquiv (s : Finset ι) : { f : Π₀ i, β i // f.support = s } ≃ ∀ i : s, { x : β i // x ≠ 0 }
where
toFun
| ⟨f, hf⟩ => fun ⟨i, hi⟩ ↦ ⟨f i, (f.mem_support_toFun i).1 <| hf.symm ▸ hi⟩
invFun
f :=
⟨mk s fun i ↦ (f i).1,
Finset.ext fun i ↦ by
-- TODO: `simp` fails to use `(f _).2` inside `∃ _, _`
calc
i ∈ support (mk s fun i ↦ (f i).1) ↔ ∃ h : i ∈ s, (f ⟨i, h⟩).1 ≠ 0 := by simp
_ ↔ ∃ _ : i ∈ s, True := (exists_congr fun h ↦ (iff_true _).mpr (f _).2)
_ ↔ i ∈ s := by simp⟩
left_inv := by
rintro ⟨f, rfl⟩
ext i
simpa using Eq.symm
right_inv
f := by
ext1
simp; rfl
