English
For a list l of predicates and a hypothesis H relating l and existence, the TFAE of ∃-instantiated versions holds.
Русский
Для списка предикатов и гипотезы, связывающей их с существованием, выполняется TFAE для существовательных версий.
LaTeX
$$$ (l.map (\p -> \exists a, p a)).TFAE $$$
Lean4
/-- If `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∃ x, P₁ x) ↔ ... ↔ (∃ x, Pₙ x)`.
Note: in concrete cases, Lean has trouble finding the list `[P₁, ..., Pₙ]` from the list
`[(∃ x, P₁ x), ..., (∃ x, Pₙ x)]`, but simply providing a list of underscores with the right
length makes it happier.
Example:
```lean
example (P₁ P₂ P₃ : ℕ → Prop) (H : ∀ n, [P₁ n, P₂ n, P₃ n].TFAE) :
[∃ n, P₁ n, ∃ n, P₂ n, ∃ n, P₃ n].TFAE :=
exists_tfae [_, _, _] H
```
-/
theorem exists_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) :
(l.map (fun p ↦ ∃ a, p a)).TFAE := by
simp only [TFAE, List.forall_mem_map]
intro p₁ hp₁ p₂ hp₂
exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁) (p₂ a) (mem_map_of_mem hp₂)
