-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.mk.injEq : ∀ {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)