∀ {M : Type u_2} {N : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {L : Type u_1} [inst_4 : Mul L] [inst_5 : TopologicalSpace L] (cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L),
  Continuous (cme1.trans cme2.toMulEquiv).invFun