Hopf problem: toric · diagonal quotient 2

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

theorem Mathoverflow1973.DiagonalQuotient.fundamentalGroup_mapOfEq_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : C(A, B)) (g : C(B, C)) (a : A) (b : B) (c : C) (hf : f a = b) (hg : g b = c) (v : FundamentalGroup A a) : (FundamentalGroup.mapOfEq (g.comp f) ⋯) v = (FundamentalGroup.mapOfEq g hg) ((FundamentalGroup.mapOfEq f hf) v)