English
Let γ1: Path a1→a2, δ1: Path a2→a3, γ2: Path b1→b2, δ2: Path b2→b3. Then the concatenation of γ1 with γ2, followed by δ1 with δ2, equals the product of the concatenations: (γ1.prod γ2).trans(δ1.prod δ2) = (γ1.trans δ1).prod(γ2.trans δ2).
Русский
Пусть γ1: путь a1→a2, δ1: путь a2→a3, γ2: путь b1→b2, δ2: путь b2→b3. Тогда конкатенация γ1 с γ2, затем δ1 с δ2, равна произведению конкатенаций: (γ1.prod γ2).trans(δ1.prod δ2) = (γ1.trans δ1).prod(γ2.trans δ2).
LaTeX
$$$\bigl(\gamma_1.prod \gamma_2\bigr)\!\coloneqq\, \gamma_1(t) \cdot \gamma_2(t) \quad \text{and}\quad (\gamma_1.trans \delta_1).prod (\gamma_2.trans \delta_2) = \text{...}$ \n$$\bigl(\gamma_1.prod\gamma_2\bigr).trans(\delta_1.prod\delta_2) = (\gamma_1.trans\delta_1).prod(\gamma_2.trans\delta_2).$$$$
Lean4
/-- Path composition commutes with products -/
theorem trans_prod_eq_prod_trans (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃) :
(γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂) := by
ext t <;> unfold Path.trans <;> simp only [Path.coe_mk_mk, Path.prod_coe, Function.comp_apply] <;> split_ifs <;> rfl
