awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set (↑U : Type u_3)
hV : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val (p := fun (x : Y) ↦ x ∈ U) '' V ⊆ U

Tactic:
simp
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set (↑U : Type u_3)
hV : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) '' V

Tactic:
simp
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set (↑U : Type u_3)
hV : ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
obtain :
  ∀ (V : Set Y) (hV : V ⊆ U)
    (hV :
      ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
        IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)),
    IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] V

Tactic:
obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ U ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩

Premises used: Subtype.val, rfl, Set
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)

Tactic:
continuous_subtype_val.isOpen_preimage _ ?_

Premises used: continuous_subtype_val, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
refine : IsOpen[inst_1] V
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)

Tactic:
refine continuous_subtype_val.isOpen_preimage _ ?_

Premises used: continuous_subtype_val, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
rw : ∀ ⦃i : ι⦄ (f : ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)
⊢ IsOpen[inst_1] V

Tactic:
rw [IsGeneratedBy.isOpen_iff X]

Premises used: Topology.IsGeneratedBy.isOpen_iff
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
i : ι
f : ContinuousMap.{u_2, u_3} (X i) Y
⊢ IsOpen[inst ⟨i, f⟩.fst]
    (Subtype.val (p :=
        fun
          (x :
            X
              (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
                (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))) ↦
        x ∈ (↑(W (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f)) : Set (X ⟨i, f⟩.fst))) ''
      g (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f) ⁻¹'
        Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)

Tactic:
(W ⟨i, f⟩).isOpen.isOpenMap_subtype_val _ (hV ⟨i, f⟩)

Premises used: TopologicalSpace.Opens.isOpen, Sigma.mk, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
i : ι
f : ContinuousMap.{u_2, u_3} (X i) Y
h :
  Eq (α := Set (X i)) ((⇑f : (a : X i) → Y) ⁻¹' V : Set (X i))
    (Subtype.val (p :=
          fun
            (x :
              X
                (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
                  (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))) ↦
          x ∈ (↑(W (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f)) : Set (X ⟨i, f⟩.fst))) ''
        g (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f) ⁻¹'
          Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V :
      Set
        (X
          (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
            (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))))
⊢ IsOpen[inst i] ((⇑f : (a : X i) → Y) ⁻¹' V)

Tactic:
convert! (W ⟨i, f⟩).isOpen.isOpenMap_subtype_val _ (hV ⟨i, f⟩)

Premises used: TopologicalSpace.Opens.isOpen, Sigma.mk, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst_1] U
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Opens (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' U,
      is_open' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑U : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    U.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV_1 : V ⊆ U
hV :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V)
i : ι
f : ContinuousMap.{u_2, u_3} (X i) Y
⊢ Eq (α := Set (X i)) ((⇑f : (a : X i) → Y) ⁻¹' V : Set (X i))
    (Subtype.val (p :=
          fun
            (x :
              X
                (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
                  (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))) ↦
          x ∈ (↑(W (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f)) : Set (X ⟨i, f⟩.fst))) ''
        g (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f) ⁻¹'
          Subtype.val (p := fun (x : Y) ↦ x ∈ U) ⁻¹' V :
      Set
        (X
          (Sigma.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)
            (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y) i f))))

Tactic:
aesop
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst_3 : IsGeneratedBy X Y
F : Type u_4
inst_4 : TopologicalSpace F
f : F → Y
hf : IsOpenEmbedding f
⊢ IsGeneratedBy X F

Tactic:
have := hf.isOpen_range.isGeneratedBy (X := X)
  hf.toIsEmbedding.toHomeomorph.symm.isQuotientMap.isGeneratedBy

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, IsOpen.isGeneratedBy, Topology.IsOpenEmbedding.isOpen_range, Homeomorph.symm, Topology.IsQuotientMap.isGeneratedBy, Topology.IsEmbedding.toHomeomorph, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
⊢ ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)

Tactic:
have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑F : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
continuous_equiv_symm :
  Continuous[instTopologicalSpaceSubtype, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3))
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑F : Type u_3)

Tactic:
constructor
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑F : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
continuous_equiv_symm :
  ∀ (s : Set (WithGeneratedByTopology X (↑F : Type u_3))),
    IsClosed s →
      IsClosed[instTopologicalSpaceSubtype]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3)) ⁻¹'
          s)
⊢ Continuous[instTopologicalSpaceSubtype, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3))

Tactic:
rw [continuous_iff_isClosed]

Premises used: continuous_iff_isClosed
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑F : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X (↑F : Type u_3))),
    IsClosed s →
      IsClosed[instTopologicalSpaceSubtype]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3)) ⁻¹'
          s)

Tactic:
fun _ hV ↦ this _ (fun a ↦ IsClosed.preimage
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)) hV)

Premises used: Iff.mpr, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, Topology.WithGeneratedByTopology.equiv, Set.preimage, IsClosed.preimage, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Topology.Convenient.OpenClosed
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst_3 : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst_1] F
W : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) →
  TopologicalSpace.Closeds (X (a.fst (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y))) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    { carrier := (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y) ⁻¹' F,
      isClosed' := ⋯ }
g : (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) → ↥(W a) → (↑F : Type u_3) :=
  fun (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y) ↦
    F.restrictPreimage (⇑(a.snd (β := fun (i : ι) ↦ ContinuousMap.{u_2, u_3} (X i) Y)) : (a : X a.fst) → Y)
hg :
  ∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y),
    Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set (↑F : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X (↑F : Type u_3))),
    IsClosed s →
      IsClosed[instTopologicalSpaceSubtype]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑F : Type u_3)) → WithGeneratedByTopology X (↑F : Type u_3)) ⁻¹'
          s)

Tactic:
exact fun _ hV ↦ this _ (fun a ↦ IsClosed.preimage
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)) hV)

Premises used: Iff.mpr, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, IsClosed.preimage