English
A technical equality stating that the explicit expression for transAt i f g coincides with the copy of fromLoop i (Path.trans (toLoop i f) (toLoop i g)) under a certain unfolding.
Русский
Техническое равенство: явное выражение transAt i f g совпадает с копией fromLoop i (Path.trans (toLoop i f) (toLoop i g)) при раскрытии.
LaTeX
$$$\\mathrm{Eq}(\\mathrm{transAt}\; i\; f\; g, \\mathrm{copy}(\\mathrm{fromLoop}\; i (\\mathrm{Path.trans}(\\mathrm{toLoop}\; i\; f)(\\mathrm{toLoop}\; i\; g))))$$$
Lean4
@[scoped macro Topology.termπ_]
public meta def _aux_Mathlib_Topology_Homotopy_HomotopyGroup___macroRules_Topology_termπ__1 : Macro✝ := fun
| `(π_) => ``(HomotopyGroup.Pi)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
