English
If f,g, inv, p, and h are given as in the statement, there exists q such that ∀ v, S v ↔ ∃ t, q(v ⊗ t) = 0.
Русский
Если даны f, g, inv, p и h согласно утверждению, существует q, что ∀ v, S v ⇔ ∃ t, q(v ⊗ t) = 0.
LaTeX
$$$$ \\exists q : Poly (\\alpha ⊕ \\gamma), \\forall v, S v \\iff \\exists t, q(v \\otimes t) = 0 $$$$
Lean4
theorem inject_dummies (f : β → γ) (g : γ → Option β) (inv : ∀ x, g (f x) = some x) (p : Poly (α ⊕ β))
(h : ∀ v, S v ↔ ∃ t, p (v ⊗ t) = 0) : ∃ q : Poly (α ⊕ γ), ∀ v, S v ↔ ∃ t, q (v ⊗ t) = 0 :=
⟨p.map (inl ⊗ inr ∘ f), fun v => (h v).trans <| inject_dummies_lem f g inv _ _⟩