Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_4
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots✝¹ : ∀ {n : ℕ} (x : X), (fun x_1 ↦ x) ∈ p₁ n
plot_reparam✝¹ :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
    p ∈ p₁ m → ContDiff ℝ ∞ f → p ∘ f ∈ p₁ 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 ∈ p₁ m) →
      p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots✝ : ∀ {n : ℕ} (x : X), (fun x_1 ↦ x) ∈ p₂ n
plot_reparam✝ :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
    p ∈ p₂ m → ContDiff ℝ ∞ f → p ∘ f ∈ p₂ 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 ∈ p₂ m) →
      p ∈ p₂ n
t₂ : TopologicalSpace X
h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u)
h :
  @IsPlot X
      { plots := p₁, constant_plots := constant_plots✝¹, plot_reparam := plot_reparam✝¹, locality := locality✝¹,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ } =
    @IsPlot X
      { plots := p₂, constant_plots := constant_plots✝, plot_reparam := plot_reparam✝, locality := locality✝,
        dTopology := t₂, isOpen_iff_preimages_plots := h₂ }
⊢ { plots := p₁, constant_plots := constant_plots✝¹, plot_reparam := plot_reparam✝¹, locality := locality✝¹,
      dTopology := t₁, isOpen_iff_preimages_plots := h₁ } =
    { plots := p₂, constant_plots := constant_plots✝, plot_reparam := plot_reparam✝, locality := locality✝,
      dTopology := t₂, isOpen_iff_preimages_plots := h₂ }

Tactic:
congr 1

Goal state after:
case e_dTopology
X : Type u_4
p₁ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots✝¹ : ∀ {n : ℕ} (x : X), (fun x_1 ↦ x) ∈ p₁ n
plot_reparam✝¹ :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
    p ∈ p₁ m → ContDiff ℝ ∞ f → p ∘ f ∈ p₁ 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 ∈ p₁ m) →
      p ∈ p₁ n
t₁ : TopologicalSpace X
h₁ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₁ n, IsOpen (p ⁻¹' u)
p₂ : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
constant_plots✝ : ∀ {n : ℕ} (x : X), (fun x_1 ↦ x) ∈ p₂ n
plot_reparam✝ :
  ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
    p ∈ p₂ m → ContDiff ℝ ∞ f → p ∘ f ∈ p₂ 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 ∈ p₂ m) →
      p ∈ p₂ n
t₂ : TopologicalSpace X
h₂ : ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ p₂ n, IsOpen (p ⁻¹' u)
h :
  @IsPlot X
      { plots := p₁, constant_plots := constant_plots✝¹, plot_reparam := plot_reparam✝¹, locality := locality✝¹,
        dTopology := t₁, isOpen_iff_preimages_plots := h₁ } =
    @IsPlot X
      { plots := p₂, constant_plots := constant_plots✝, plot_reparam := plot_reparam✝, locality := locality✝,
        dTopology := t₂, isOpen_iff_preimages_plots := h₂ }
⊢ t₁ = t₂