English
If l is a list of predicates on α and for every a ∈ α the list of p a has TFAE, then the list of predicates ∀ a, p a has TFAE.
Русский
Для списка предикатов l на α, если для каждого a ∈ α список p a имеет TFAE, то список предикатов ∀ a, p a имеет TFAE.
LaTeX
$$$ (l.map (\p -> \forall 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 :=
forall_tfae [_, _, _] H
```
-/
theorem forall_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 forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁) (p₂ a) (mem_map_of_mem hp₂)
