∀ {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} [inst_5 : SizeOf X] [inst_6 : SizeOf E] [inst_7 : SizeOf 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),
  sizeOf
      { M := M, topSpaceM := topSpaceM, chartedSpace := chartedSpace, isManifold := isManifold,
        compactSpace := compactSpace, boundaryless := boundaryless, f := f, hf := hf } =
    1 + sizeOf M + sizeOf topSpaceM + sizeOf chartedSpace + sizeOf isManifold + sizeOf compactSpace +
        sizeOf boundaryless +
      sizeOf hf