{H : Type u} →
  [inst : TopologicalSpace H] →
    {G : StructureGroupoid H} →
      {M : Type u_5} →
        {M' : Type u_6} →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : TopologicalSpace M'] →
              [inst_3 : ChartedSpace H M] →
                [inst_4 : ChartedSpace H M'] →
                  (toFun : M → M') →
                    (invFun : M' → M) →
                      (left_inv : autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam) →
                        (right_inv : autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam) →
                          (continuous_toFun : autoParam (Continuous toFun) Homeomorph.continuous_toFun._autoParam) →
                            (continuous_invFun :
                                autoParam (Continuous invFun) Homeomorph.continuous_invFun._autoParam) →
                              (∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H),
                                  c ∈ atlas H M →
                                    c' ∈ atlas H M' →
                                      c.symm.trans
                                          ({ toFun := toFun, invFun := invFun, left_inv := left_inv,
                                                  right_inv := right_inv, continuous_toFun := continuous_toFun,
                                                  continuous_invFun := continuous_invFun }.toOpenPartialHomeomorph.trans
                                            c') ∈
                                        G) →
                                Structomorph G M M'