English
For families γ0, γ1 of paths coordinatewise, the trans of their Pi-construction equals the Pi of the trans: (Path.pi γ0).trans (Path.pi γ1) = Path.pi (i ↦ (γ0 i).trans (γ1 i)).
Русский
Для семейств путей г_0, г_1 по координатам выполняется: (Path.pi γ0).trans (Path.pi γ1) = Path.pi (i ↦ (γ0 i).trans (γ1 i)).
LaTeX
$$$\bigl(\mathrm{Path.pi}\,\gamma_0\bigr).\mathrm{trans}\bigl(\mathrm{Path.pi}\,\gamma_1\bigr) = \mathrm{Path.pi}\;\lambda i.\bigl(\gamma_0(i)\bigr).\mathrm{trans}\bigl(\gamma_1(i)\bigr).$$$
Lean4
/-- Path composition commutes with products -/
theorem trans_pi_eq_pi_trans (γ₀ : ∀ i, Path (as i) (bs i)) (γ₁ : ∀ i, Path (bs i) (cs i)) :
(Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i) :=
by
ext t i
unfold Path.trans
simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]
split_ifs <;> rfl
