∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)),
  TopologicalSpace.Opens.comap (g.comp f) = (TopologicalSpace.Opens.comap f).comp (TopologicalSpace.Opens.comap g)