English
Composition and product commute: composing two pi's is the same as pi of the pointwise compositions.
Русский
Составление и произведение коммутируют: композиция двух pi равно pi по точечным композициям.
LaTeX
$$$\pi γ_0 \;\cdot\; \pi γ_1 = \pi (\gamma_0 \cdot \gamma_1)$$$
Lean4
/-- Composition and products commute.
This is `Path.trans_pi_eq_pi_trans` descended to path homotopy classes. -/
theorem comp_pi_eq_pi_comp (γ₀ : ∀ i, Path.Homotopic.Quotient (as i) (bs i))
(γ₁ : ∀ i, Path.Homotopic.Quotient (bs i) (cs i)) : pi γ₀ ⬝ pi γ₁ = pi fun i ↦ γ₀ i ⬝ γ₁ i := by
induction γ₁ using Quotient.induction_on_pi with
| _ a =>
induction γ₀ using Quotient.induction_on_pi
simp only [pi_lift]
rw [← Path.Homotopic.comp_lift, Path.trans_pi_eq_pi_trans, ← pi_lift]
rfl
