{X : Type u_1} →
  {P : Sort u} →
    {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} →
                      {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} →
                                        { 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 } =
                                            { 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' } →
                                          (isPlotOn ≍ isPlotOn' → isPlot ≍ isPlot' → dTopology ≍ dTopology' → P) → P