English
The preimage under List.TProd.mk of Set.tprod l t equals the dependent product set { i ∈ l }.pi t, i.e., the set of all functions f : ∀ i, α i with f(i) ∈ t(i) for every i ∈ l.
Русский
Обратнообразование по List.TProd.mk от Set.tprod l t равно зависимому произведению { i ∈ l }.pi t; то есть множество всех функций f с f(i) ∈ t(i) для каждого i ∈ l.
LaTeX
$$$(\\mathrm{List.TProd.mk}\\, l)^{-1}'(\\mathrm{Set.tprod}\\ l\\ t) = \\{ f : (\\forall i, \\alpha i) \\mid \\forall i \\in l, f(i) \\in t(i) \\}.$$$
Lean4
theorem mk_preimage_tprod : ∀ (l : List ι) (t : ∀ i, Set (α i)), TProd.mk l ⁻¹' Set.tprod l t = {i | i ∈ l}.pi t
| [], t => by simp [Set.tprod]
| i :: l, t => by
ext f
have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i :=
by
change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ {x | x ∈ l}.pi t
rw [mk_preimage_tprod l t]
-- `simp [Set.TProd, TProd.mk, this]` can close this goal but is slow.
rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prodMk_mem_set_prod_eq]
simp_rw [mem_setOf_eq, mem_cons]
rw [forall_eq_or_imp, and_congr_right_iff]
exact fun _ => h
