∀ {X : Type u_1} [inst : SizeOf X]
  (isPlotOn : {n : ℕ} → {u : Set (EuclideanSpace ℝ (Fin n))} → IsOpen u → (EuclideanSpace ℝ (Fin n) → X) → Prop)
  (isPlotOn_congr :
    ∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p q : EuclideanSpace ℝ (Fin n) → X},
      Set.EqOn p q u → (isPlotOn hu p ↔ isPlotOn hu q))
  (isPlot : {n : ℕ} → (EuclideanSpace ℝ (Fin n) → X) → Prop)
  (isPlotOn_univ :
    autoParam (∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X}, isPlotOn ⋯ p ↔ isPlot p)
      DiffeologicalSpace.CorePlotsOn.isPlotOn_univ._autoParam)
  (isPlot_const : ∀ {n : ℕ} (x : X), isPlot fun x_1 => x)
  (isPlotOn_reparam :
    ∀ {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {v : Set (EuclideanSpace ℝ (Fin m))} {hu : IsOpen u}
      (hv : IsOpen v) {p : EuclideanSpace ℝ (Fin n) → X} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
      Set.MapsTo f v u → isPlotOn hu p → ContDiffOn ℝ (↑⊤) f v → isPlotOn hv (p ∘ f))
  (locality :
    ∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p : EuclideanSpace ℝ (Fin n) → X},
      (∀ x ∈ u, ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ isPlotOn hv p) → isPlotOn hu p)
  (dTopology : TopologicalSpace X)
  (isOpen_iff_preimages_plots :
    autoParam
      (∀ {u : Set X},
        TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), isPlot p → IsOpen (p ⁻¹' u))
      DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots._autoParam),
  sizeOf
      { isPlotOn := isPlotOn, isPlotOn_congr := isPlotOn_congr, isPlot := isPlot, isPlotOn_univ := isPlotOn_univ,
        isPlot_const := isPlot_const, isPlotOn_reparam := isPlotOn_reparam, locality := locality,
        dTopology := dTopology, isOpen_iff_preimages_plots := isOpen_iff_preimages_plots } =
    1 + sizeOf dTopology