English
If l is a list of sets of α → ℕ and d proves each is Dioph, then the set of v that lies in all S ∈ l is Dioph.
Русский
Если l — список множеств функций α → ℕ и каждое S ∈ l является диофовым, тогда множество всех v, принадлежащих всем S в l, диофово.
LaTeX
$$$$ \\forall l:\\, \\text{List} (\\text{Set}(\\alpha \\to \\mathbb{N})),\\; l.\\text{Forall Dioph} \\to \\text{Dioph} \\{v:\\alpha\\to\\mathbb{N} \\mid l.\\text{Forall} (\\lambda S. v \\in S)\\} $$$$
Lean4
theorem «forall» (l : List (Set <| α → ℕ)) (d : l.Forall Dioph) : Dioph {v | l.Forall fun S : Set (α → ℕ) => v ∈ S} :=
by
suffices
∃ (β : _) (pl : List (Poly (α ⊕ β))),
∀ v, List.Forall (fun S : Set _ => S v) l ↔ ∃ t, List.Forall (fun p : Poly (α ⊕ β) => p (v ⊗ t) = 0) pl
from
let ⟨β, pl, h⟩ := this
⟨β, Poly.sumsq pl, fun v => (h v).trans <| exists_congr fun t => (Poly.sumsq_eq_zero _ _).symm⟩
induction l with
| nil => exact ⟨ULift Empty, [], fun _ => by simp⟩
| cons S l IH =>
obtain ⟨⟨β, p, pe⟩, dl⟩ := (List.forall_cons _ _ _).mp d
exact
let ⟨γ, pl, ple⟩ := IH dl
⟨β ⊕ γ, p.map (inl ⊗ inr ∘ inl) :: pl.map fun q => q.map (inl ⊗ inr ∘ inr), fun v => by
simpa using
Iff.trans (and_congr (pe v) (ple v))
⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
⟨m ⊗ n, by
rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from funext fun s => by rcases s with a | b <;> rfl];
exact hm, by
refine List.Forall.imp (fun q hq => ?_) hn; dsimp [Function.comp_def]
rw [show (fun x : α ⊕ γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n from
funext fun s => by rcases s with a | b <;> rfl];
exact hq⟩,
fun ⟨t, hl, hr⟩ =>
⟨⟨t ∘ inl, by
rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
funext fun s => by rcases s with a | b <;> rfl] at hl⟩,
⟨t ∘ inr, by
refine List.Forall.imp (fun q hq => ?_) hr; dsimp [Function.comp_def] at hq
rwa [show (fun x : α ⊕ γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ t ∘ inr from
funext fun s => by rcases s with a | b <;> rfl] at hq⟩⟩⟩⟩
