English
A technical lemma relating a dummy embedding to a polynomial transformation: (exists t, p(v) = 0) is equivalent to (exists t, p.map (inl ⊗ inr ∘ f) (v ⊗ t) = 0).
Русский
Техническая лемма, связывающая внедрение заглушек с преобразованием полинома: (существует t, p(v)=0) эквивалентно (существует t, p.map (inl ⊗ inr ∘ f) (v ⊗ t) = 0).
LaTeX
$$$$ \\exists t, p(v \\otimes t) = 0 \\;\\iff\\; \\exists t, p.map (inl \\otimes inr \\circ f) (v \\otimes t) = 0 $$$$
Lean4
theorem inject_dummies_lem (f : β → γ) (g : γ → Option β) (inv : ∀ x, g (f x) = some x) (p : Poly (α ⊕ β)) (v : α → ℕ) :
(∃ t, p (v ⊗ t) = 0) ↔ ∃ t, p.map (inl ⊗ inr ∘ f) (v ⊗ t) = 0 :=
by
dsimp; refine ⟨fun t => ?_, fun t => ?_⟩ <;> obtain ⟨t, ht⟩ := t
· have : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t :=
funext fun s => by rcases s with a | b <;> dsimp [(· ∘ ·)]; try rw [inv]; rfl
exact ⟨(0 ::ₒ t) ∘ g, by rwa [this]⟩
· have : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f) := funext fun s => by rcases s with a | b <;> rfl
exact ⟨t ∘ f, by rwa [this]⟩
