English
Under the equivalence between constants-syntax and variables-syntax provided by constantsVarsEquivLeft, the realizations line up: the left-hand side realized via the equivalence equals the right-hand side realization of t.
Русский
При эквивалентности между константной и переменной формalisations, задаваемой constantsVarsEquivLeft, реализации согласованы: левая часть через эквивалентность равна реализации t справа.
LaTeX
$$$ (constantsVarsEquivLeft\; t).realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs) = t.realize (Sum.elim v xs) $$$
Lean4
theorem realize_constantsVarsEquivLeft [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M] {n}
{t : L[[α]].Term (β ⊕ (Fin n))} {v : β → M} {xs : Fin n → M} :
(constantsVarsEquivLeft t).realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs) = t.realize (Sum.elim v xs) :=
by
simp only [constantsVarsEquivLeft, realize_relabel, Equiv.coe_trans, Function.comp_apply, constantsVarsEquiv_apply,
relabelEquiv_symm_apply]
refine _root_.trans ?_ realize_constantsToVars
congr 1; funext x
rcases x with (a | (b | i)) <;> simp
