Hopf problem: uniformization · special periods 9

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SpecialPeriods.Triangle.basedLoop_subpaths_mo1973_26254 {X : Type u_1} [TopologicalSpace X] {x b : X} (τ : Path b x) (C : Path x x) (a c : ↑unitInterval) : Path.Homotopic.Quotient.mk ((τ.trans C).trans τ.symm) = Path.Homotopic.Quotient.mk ((τ.trans ((C.subpath 0 a).cast ⋯ ⋯)).trans ((C.subpath a c).trans (((C.subpath c 1).cast ⋯ ⋯).trans τ.symm)))