awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
refine_1 :
  ∀ (h : ContinuousGeneratedBy X g) (i₁ : ι) (f₁ : ContinuousMap.{u, v'} (X i₁) Z) (i₂ : ι)
    (f₂ : ContinuousMap.{u, v} (X i₂) Y),
    Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
      match (motive := X i₁ × X i₂ → T) x with
      | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
refine_2 :
  ∀
    (h :
      ∀ (i₁ : ι) (f₁ : ContinuousMap.{u, v'} (X i₁) Z) (i₂ : ι) (f₂ : ContinuousMap.{u, v} (X i₂) Y),
        Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
          match (motive := X i₁ × X i₂ → T) x with
          | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)),
    ContinuousGeneratedBy X g
⊢ ContinuousGeneratedBy X g ↔
    ∀ (i₁ : ι) (f₁ : ContinuousMap.{u, v'} (X i₁) Z) (i₂ : ι) (f₂ : ContinuousMap.{u, v} (X i₂) Y),
      Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
        match (motive := X i₁ × X i₂ → T) x with
        | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)

Tactic:
refine ⟨fun h i₁ f₁ i₂ f₂ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
refine_1 :
  ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)),
    Continuous[inst i, inst_3]
      ((fun (x : X i₁ × X i₂) ↦
          match (motive := X i₁ × X i₂ → T) x with
          | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)) ∘
        (⇑f : (a : X i) → X i₁ × X i₂))
⊢ Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → T) x with
    | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)

Tactic:
rw [IsGeneratedBy.continuous_iff X]

Premises used: Topology.IsGeneratedBy.continuous_iff
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] φ

Tactic:
fun_prop
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
⊢ ContinuousGeneratedBy X (g ∘ φ)

Tactic:
replace h := h.comp (show Continuous φ by fun_prop).continuousGeneratedBy
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
h : ContinuousGeneratedBy X (g ∘ φ)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)), Continuous[inst i, inst_3] ((g ∘ φ) ∘ (⇑f : (a : X i) → X i₁ × X i₂))

Tactic:
rw [continuousGeneratedBy_def] at h

Premises used: Topology.continuousGeneratedBy_def
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
h : ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)), Continuous[inst i, inst_3] ((g ∘ φ) ∘ (⇑f : (a : X i) → X i₁ × X i₂))
⊢ Continuous[inst j, inst_3]
    ((fun (x : X i₁ × X i₂) ↦
        match (motive := X i₁ × X i₂ → T) x with
        | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)) ∘
      (⇑p : (a : X j) → X i₁ × X i₂))

Tactic:
h p
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
i₁ : ι
f₁ : ContinuousMap.{u, v'} (X i₁) Z
i₂ : ι
f₂ : ContinuousMap.{u, v} (X i₂) Y
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun (x : X i₁ × X i₂) ↦
    match (motive := X i₁ × X i₂ → Y × Z) x with
    | (x₁, x₂) => ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
h : ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)), Continuous[inst i, inst_3] ((g ∘ φ) ∘ (⇑f : (a : X i) → X i₁ × X i₂))
⊢ Continuous[inst j, inst_3]
    ((fun (x : X i₁ × X i₂) ↦
        match (motive := X i₁ × X i₂ → T) x with
        | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)) ∘
      (⇑p : (a : X j) → X i₁ × X i₂))

Tactic:
exact h p
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : ContinuousMap.{u, v'} (X i₁) Z) (i₂ : ι) (f₂ : ContinuousMap.{u, v} (X i₂) Y),
    Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
      match (motive := X i₁ × X i₂ → T) x with
      | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
i : ι
f : C(X i, Y × Z)
⊢ Continuous[inst i, inst_3] (g ∘ (⇑f : (a : X i) → Y × Z))

Tactic:
(h i (ContinuousMap.snd.comp f) i (ContinuousMap.fst.comp f)).comp
      (Continuous.prodMk continuous_id continuous_id)

Premises used: Continuous.comp, ContinuousMap.comp, ContinuousMap.snd, continuous_id, ContinuousMap.fst, Continuous.prodMk
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : ContinuousMap.{u, v'} (X i₁) Z) (i₂ : ι) (f₂ : ContinuousMap.{u, v} (X i₂) Y),
    Continuous[instTopologicalSpaceProd, inst_3] fun (x : X i₁ × X i₂) ↦
      match (motive := X i₁ × X i₂ → T) x with
      | (x₁, x₂) => g ((f₂ : (a : X i₂) → Y) x₂, (f₁ : (a : X i₁) → Z) x₁)
i : ι
f : C(X i, Y × Z)
⊢ Continuous[inst i, inst_3] (g ∘ (⇑f : (a : X i) → Y × Z))

Tactic:
exact (h i (ContinuousMap.snd.comp f) i (ContinuousMap.fst.comp f)).comp
      (Continuous.prodMk continuous_id continuous_id)

Premises used: Continuous.comp, ContinuousMap.comp, ContinuousMap.snd, continuous_id, ContinuousMap.fst, Continuous.prodMk
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
inst_5 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X (Y × Z) T
⊢ ContinuousGeneratedBy X (Z := ContinuousMapGeneratedBy X Y T) fun (z : Z) ↦
    g.comp (X := X) (mk (X := X) (fun (y : Y) ↦ (y, z)) ⋯)

Tactic:
simpa only [continuousGeneratedBy_iff_uncurry,
          continuousGeneratedBy_dom_prod_iff] using g.prop

Premises used: Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_iff_uncurry, Topology.ContinuousMapGeneratedBy.prop, Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_dom_prod_iff
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
inst_5 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)
⊢ ContinuousGeneratedBy X (Z := T) fun (x : Y × Z) ↦
    (((g : (a : Z) → ContinuousMapGeneratedBy X Y T) x.2 : ContinuousMapGeneratedBy X Y T) : (a : Y) → T) x.1

Tactic:
simpa only [continuousGeneratedBy_iff_uncurry,
          continuousGeneratedBy_dom_prod_iff] using g.prop

Premises used: Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_iff_uncurry, Topology.ContinuousMapGeneratedBy.prop, Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_dom_prod_iff
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
inst_5 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X (Y × Z) T
y : Y
z : Z
⊢ Eq.{v'' + 1} (α := T)
    ((((((curryEquiv (X := X) :
                      (a : ContinuousMapGeneratedBy X (Y × Z) T) →
                        ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T))
                    g :
                  ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)) :
                (a : Z) → ContinuousMapGeneratedBy X Y T)
              z :
            ContinuousMapGeneratedBy X Y T) :
          (a : Y) → T)
        y :
      T)
    ((g : (a : Y × Z) → T) (y, z) : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
inst_5 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)
y : Y
z : Z
⊢ Eq.{v'' + 1} (α := T)
    ((((Equiv.symm (curryEquiv (X := X)) :
                (a : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)) →
                  ContinuousMapGeneratedBy X (Y × Z) T)
              g :
            ContinuousMapGeneratedBy X (Y × Z) T) :
          (a : Y × Z) → T)
        (y, z) :
      T)
    ((((g : (a : Z) → ContinuousMapGeneratedBy X Y T) z : ContinuousMapGeneratedBy X Y T) : (a : Y) → T) y : T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
inst_4 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
y : Y
f : ContinuousMapGeneratedBy X Y Z
⊢ Eq.{v' + 1} (α := Z) ((ev (X := X) : (a : Y × ContinuousMapGeneratedBy X Y Z) → Z) (y, f) : Z)
    ((f : (a : Y) → Z) y : Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Convenient.HomSpace
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst_1 : TopologicalSpace Y
Z : Type v'
inst_2 : TopologicalSpace Z
T : Type v''
inst_3 : TopologicalSpace T
inst_4 : ∀ (i : ι), LocallyCompactSpace.{u} (X i)
inst_5 : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
p : ContinuousMapGeneratedBy X Z T
g : ContinuousMapGeneratedBy X Y Z
⊢ (p.postcomp (X := X) : (a : ContinuousMapGeneratedBy X Y Z) → ContinuousMapGeneratedBy X Y T) g = p.comp (X := X) g

Tactic:
rfl

Premises used: Topology.ContinuousMapGeneratedBy.comp, rfl
-- Module: Mathlib.Topology.Convenient.Localization
Goal:
ι : Type t
X_1 : ι → Type u
inst : (i : ι) → TopologicalSpace (X_1 i)
X Y Z : TopCat
⊢ IsIso (C := ContinuousGeneratedByCat X_1) (X :=
    Functor.obj (toContinuousGeneratedByCat X_1)
      ((Functor.comp (D := GeneratedByTopCat X_1) (toGeneratedByTopCat (X := X_1))
            (GeneratedByTopCat.toTopCat (X := X_1))).obj
        Z))
    (CategoryTheory.Functor.map (toContinuousGeneratedByCat X_1)
      (NatTrans.app (GeneratedByTopCat.adjCounit (X := X_1)) Z))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Convenient.Localization
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
x : TopCat
⊢ morphismPropertyWithGeneratedByTopologyEquiv X (X :=
    (Functor.comp (D := ContinuousGeneratedByCat X) (toContinuousGeneratedByCat X)
          (ContinuousGeneratedByCat.toTopCat X)).obj
      x)
    (NatTrans.app (Adjunction.counit (ContinuousGeneratedByCat.adj (X := X))) x)

Tactic:
constructor
-- Module: Mathlib.Topology.Convenient.Localization
Goal:
ι : Type t
X_1 : ι → Type u
inst : (i : ι) → TopologicalSpace (X_1 i)
X Y Z : TopCat
⊢ IsIso (C := GeneratedByTopCat X_1) (X :=
    Functor.obj (toGeneratedByTopCat (X := X_1))
      ((Functor.comp (D := GeneratedByTopCat X_1) (toGeneratedByTopCat (X := X_1))
            (GeneratedByTopCat.toTopCat (X := X_1))).obj
        Z))
    (CategoryTheory.Functor.map (toGeneratedByTopCat (X := X_1))
      (NatTrans.app (GeneratedByTopCat.adjCounit (X := X_1)) Z))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Convenient.Localization
Goal:
ι : Type t
X : ι → Type u
inst : (i : ι) → TopologicalSpace (X i)
x : TopCat
⊢ morphismPropertyWithGeneratedByTopologyEquiv X (X :=
    (Functor.comp (D := GeneratedByTopCat X) (toGeneratedByTopCat (X := X)) (GeneratedByTopCat.toTopCat (X := X))).obj
      x)
    (NatTrans.app (Adjunction.counit (GeneratedByTopCat.adj (X := X))) x)

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 : ι) (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)
⊢ ∀ (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 : ι) (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)
this :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
continuous_equiv_symm :
  Continuous[instTopologicalSpaceSubtype, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3))
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑U : 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 : ι) (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)
this :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
continuous_equiv_symm :
  ∀ (s : Set (WithGeneratedByTopology X (↑U : Type u_3))),
    IsOpen s →
      IsOpen[instTopologicalSpaceSubtype]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3)) ⁻¹'
          s)
⊢ Continuous[instTopologicalSpaceSubtype, _]
    (⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
      (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3))

Tactic:
rw [continuous_def]

Premises used: continuous_def
-- 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)
this :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X (↑U : Type u_3))),
    IsOpen s →
      IsOpen[instTopologicalSpaceSubtype]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3)) ⁻¹'
          s)

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

Premises used: Iff.mpr, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, Topology.WithGeneratedByTopology.equiv, Set.preimage, Equiv.symm, Continuous.isOpen_preimage, 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 : ι) (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)
this :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X (↑U : Type u_3))),
    IsOpen s →
      IsOpen[instTopologicalSpaceSubtype]
        ((⇑(Equiv.symm (WithGeneratedByTopology.equiv (X := X))) :
            (a : (↑U : Type u_3)) → WithGeneratedByTopology X (↑U : Type u_3)) ⁻¹'
          s)

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

Premises used: Iff.mpr, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, 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)
suffices :
  ∀ (V : Set (↑U : Type u_3)),
    (∀ (a : (i : ι) × ContinuousMap.{u_2, u_3} (X i) Y), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ IsGeneratedBy.{u_3, u_1, u_2} X (↑U : Type u_3)

Tactic:
suffices ∀ (V : Set U), (∀ a, IsOpen ((g a) ⁻¹' V)) → IsOpen V by
    constructor
    rw [continuous_def]
    exact fun _ hV ↦ this _ (fun a ↦
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)).isOpen_preimage _ hV)