∀ {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)