∀ {X : Type u_1} {inst : TopologicalSpace X} {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  {inst_1 : NormedAddCommGroup E} {inst_2 : NormedSpace ℝ E} {inst_3 : FiniteDimensional ℝ E}
  {inst_4 : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type u} {topSpaceM : TopologicalSpace M}
  {chartedSpace : ChartedSpace H M} {isManifold : IsManifold I k M} {compactSpace : CompactSpace M}
  {boundaryless : BoundarylessManifold I M} {f : M → X} {hf : Continuous f} {M_1 : Type u}
  {topSpaceM_1 : TopologicalSpace M_1} {chartedSpace_1 : ChartedSpace H M_1} {isManifold_1 : IsManifold I k M_1}
  {compactSpace_1 : CompactSpace M_1} {boundaryless_1 : BoundarylessManifold I M_1} {f_1 : M_1 → X}
  {hf_1 : Continuous f_1},
  { M := M, topSpaceM := topSpaceM, chartedSpace := chartedSpace, isManifold := isManifold,
        compactSpace := compactSpace, boundaryless := boundaryless, f := f, hf := hf } =
      { M := M_1, topSpaceM := topSpaceM_1, chartedSpace := chartedSpace_1, isManifold := isManifold_1,
        compactSpace := compactSpace_1, boundaryless := boundaryless_1, f := f_1, hf := hf_1 } →
    M = M_1 ∧ topSpaceM ≍ topSpaceM_1 ∧ chartedSpace ≍ chartedSpace_1 ∧ f ≍ f_1