English
For any path γ, delayReflRight(0, γ) equals γ concatenated with the constant path at its endpoint y.
Русский
Для любого пути γ, delayReflRight(0, γ) равен γ, далее соединенному с константным путём в точке y.
LaTeX
$$delayReflRight(0, γ) = γ.trans (refl y)$$
Lean4
theorem delayReflRight_zero (γ : Path x y) : delayReflRight 0 γ = γ.trans (Path.refl y) :=
by
ext t
simp only [delayReflRight, trans_apply, Path.coe_mk_mk, refl_apply]
split_ifs with h; swap
on_goal 1 => conv_rhs => rw [← γ.target]
all_goals apply congr_arg γ; ext1; rw [qRight_zero_right]
exacts [if_neg h, if_pos h]