-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.mk.inj : ∀ {X : Type u_1}
  {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_1 : {n : ℕ} → {u : Set (EuclideanSpace ℝ (Fin n))} → IsOpen u → (EuclideanSpace ℝ (Fin n) → X) → Prop}
  {isPlotOn_congr_1 :
    ∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p q : EuclideanSpace ℝ (Fin n) → X},
      Set.EqOn p q u → (isPlotOn_1 hu p ↔ isPlotOn_1 hu q)}
  {isPlot_1 : {n : ℕ} → (EuclideanSpace ℝ (Fin n) → X) → Prop}
  {isPlotOn_univ_1 :
    autoParam (∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X}, isPlotOn_1 ⋯ p ↔ isPlot_1 p)
      DiffeologicalSpace.CorePlotsOn.isPlotOn_univ._autoParam}
  {isPlot_const_1 : ∀ {n : ℕ} (x : X), isPlot_1 fun x_1 => x}
  {isPlotOn_reparam_1 :
    ∀ {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_1 hu p → ContDiffOn ℝ (↑⊤) f v → isPlotOn_1 hv (p ∘ f)}
  {locality_1 :
    ∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p : EuclideanSpace ℝ (Fin n) → X},
      (∀ x ∈ u, ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ isPlotOn_1 hv p) → isPlotOn_1 hu p}
  {dTopology_1 : TopologicalSpace X}
  {isOpen_iff_preimages_plots_1 :
    autoParam
      (∀ {u : Set X},
        TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), isPlot_1 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_1, isPlotOn_congr := isPlotOn_congr_1, isPlot := isPlot_1,
        isPlotOn_univ := isPlotOn_univ_1, isPlot_const := isPlot_const_1, isPlotOn_reparam := isPlotOn_reparam_1,
        locality := locality_1, dTopology := dTopology_1, isOpen_iff_preimages_plots := isOpen_iff_preimages_plots_1 } →
    isPlotOn = isPlotOn_1 ∧ isPlot = isPlot_1 ∧ dTopology = dTopology_1