{X : Type u_1} →
  {motive : DiffeologicalSpace X → Sort u} →
    ((plots : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)) →
        (constant_plots : ∀ {n : ℕ} (x : X), (fun x_1 => x) ∈ plots n) →
          (plot_reparam :
              ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
                p ∈ plots m → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots n) →
            (locality :
                ∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
                  (∀ (x : EuclideanSpace ℝ (Fin n)),
                      ∃ u,
                        IsOpen u ∧
                          x ∈ u ∧
                            ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
                              (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots m) →
                    p ∈ plots n) →
              (dTopology : TopologicalSpace X) →
                (isOpen_iff_preimages_plots :
                    ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u)) →
                  motive
                    { plots := plots, constant_plots := constant_plots, plot_reparam := plot_reparam,
                      locality := locality, dTopology := dTopology,
                      isOpen_iff_preimages_plots := isOpen_iff_preimages_plots }) →
      (t : DiffeologicalSpace X) → motive t