awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
rw :
  IsCompact (X := X)
      (preimage (β := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
        ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' K)) ↔
    IsCompact K
rw₁ rw₂ : IsCompact K ↔ IsCompact K
⊢ IsCompact (X := 𝐤X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' K) ↔ IsCompact K

Tactic:
rw [isCompact_iff, Equiv.preimage_image]

Premises used: CompactCoherentification.isCompact_iff, Equiv.preimage_image
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ CompactlyCoherentSpace.{u_1} (𝐤X)

Tactic:
.of_isOpen_forall_compactSpace fun U hU ↦ isOpen_iff.mpr fun K hK ↦ ?_

Premises used: Iff.mpr, CompactCoherentification.isOpen_iff, CompactlyCoherentSpace.of_isOpen_forall_compactSpace
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
refine :
  ∀ (U : Set (𝐤X))
    (hU :
      ∀ (K : Type u_1) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → 𝐤X),
        Continuous[_, instTopologicalSpace] f → IsOpen (f ⁻¹' U))
    (K : Set X) (hK : IsCompact K),
    IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' U)
⊢ CompactlyCoherentSpace.{u_1} (𝐤X)

Tactic:
refine .of_isOpen_forall_compactSpace fun U hU ↦ isOpen_iff.mpr fun K hK ↦ ?_
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set (𝐤X)
hU :
  ∀ (K : Type u_1) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → 𝐤X),
    Continuous[_, instTopologicalSpace] f → IsOpen (f ⁻¹' U)
K : Set X
hK : IsCompact K
rw :
  IsOpen[instTopologicalSpaceSubtype]
    ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' U)
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' U)

Tactic:
rw [← preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set (𝐤X)
hU :
  ∀ (K : Type u_1) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → 𝐤X),
    Continuous[_, instTopologicalSpace] f → IsOpen (f ⁻¹' U)
K : Set X
hK : IsCompact K
⊢ CompactSpace.{u_1} (↑K : Type u_1)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set (𝐤X)
hU :
  ∀ (K : Type u_1) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → 𝐤X),
    Continuous[_, instTopologicalSpace] f → IsOpen (f ⁻¹' U)
K : Set X
hK : IsCompact K
this : CompactSpace.{u_1} (↑K : Type u_1)
⊢ IsOpen[instTopologicalSpaceSubtype]
    ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' U)

Tactic:
hU K _ (continuous_rng_of_compactSpace.mpr continuous_subtype_val)

Premises used: Iff.mpr, CompactCoherentification.continuous_rng_of_compactSpace, continuous_subtype_val, Set.Elem
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set (𝐤X)
hU :
  ∀ (K : Type u_1) [inst_2 : TopologicalSpace K] [CompactSpace K] (f : K → 𝐤X),
    Continuous[_, instTopologicalSpace] f → IsOpen (f ⁻¹' U)
K : Set X
hK : IsCompact K
this : CompactSpace.{u_1} (↑K : Type u_1)
⊢ IsOpen[instTopologicalSpaceSubtype]
    ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' U)

Tactic:
exact hU K _ (continuous_rng_of_compactSpace.mpr continuous_subtype_val)

Premises used: Iff.mpr, CompactCoherentification.continuous_rng_of_compactSpace, continuous_subtype_val, Set.Elem
-- Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : T2Space X
⊢ T2Space.{u_1} (𝐤X)

Tactic:
T2Space.of_injective_continuous (f := (CompactCoherentification.mk X).symm)
      (CompactCoherentification.mk X).symm.injective continuous_mk_symm

Premises used: CompactCoherentification.mk, CompactCoherentification.continuous_mk_symm, T2Space.of_injective_continuous, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
inst : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h :
  ∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, t] (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
rw :
  Continuous[_, t]
    (f ∘
      fun
        (x :
          (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
            (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                      ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                  (P := fun (x : TopCat.{u}) ↦ True)) :
              Type u)) ↦
      match (motive :=
        (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
            (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                      ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                  (P := fun (x : TopCat.{u}) ↦ True)) :
              Type u) →
          X)
        x with
      | ⟨⟨fst, i⟩, s⟩ => (i : (a : (↑fst.toTop : Type u)) → X) s)
⊢ Continuous[compactlyGenerated X, t] f

Tactic:
rw [continuous_coinduced_dom]

Premises used: continuous_coinduced_dom
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
inst : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h :
  ∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, t] (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
⊢ Continuous[_, t]
    (f ∘
      fun
        (x :
          (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
            (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                      ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                  (P := fun (x : TopCat.{u}) ↦ True)) :
              Type u)) ↦
      match (motive :=
        (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
            (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                      ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                  (P := fun (x : TopCat.{u}) ↦ True)) :
              Type u) →
          X)
        x with
      | ⟨⟨fst, i⟩, s⟩ => (i : (a : (↑fst.toTop : Type u)) → X) s)

Tactic:
continuity
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
a : t ≤ compactlyGenerated X
a₁ : compactlyGenerated X ≤ t
⊢ t = compactlyGenerated X

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
⊢ t ≤ compactlyGenerated X

Tactic:
UCompactlyGeneratedSpace.le_compactlyGenerated

Premises used: UCompactlyGeneratedSpace.le_compactlyGenerated
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
⊢ t ≤ compactlyGenerated X

Tactic:
exact UCompactlyGeneratedSpace.le_compactlyGenerated

Premises used: UCompactlyGeneratedSpace.le_compactlyGenerated
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
a :
  ∀ (a : CompHaus.{u}) (b : ContinuousMap.{u, w} (↑(a.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, t] fun (a_1 : (↑(a.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
      (b : (a : (↑a.toTop : Type u)) → X) a_1
⊢ compactlyGenerated X ≤ t

Tactic:
simp only [compactlyGenerated, ← continuous_iff_coinduced_le, continuous_sigma_iff,
      Sigma.forall]

Premises used: Sigma.forall, continuous_sigma_iff, TopologicalSpace.compactlyGenerated, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
⊢ ∀ (a : CompHaus.{u}) (b : ContinuousMap.{u, w} (↑(a.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, t] fun (a_1 : (↑(a.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
      (b : (a : (↑a.toTop : Type u)) → X) a_1

Tactic:
fun S f ↦ f.2

Premises used: ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
⊢ ∀ (a : CompHaus.{u}) (b : ContinuousMap.{u, w} (↑(a.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, t] fun (a_1 : (↑(a.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
      (b : (a : (↑a.toTop : Type u)) → X) a_1

Tactic:
exact fun S f ↦ f.2
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst : DiscreteTopology X
rw : ⊥ ≤ compactlyGenerated X
⊢ t ≤ compactlyGenerated X

Tactic:
rw [DiscreteTopology.eq_bot (t := t)]

Premises used: DiscreteTopology.eq_bot
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        Continuous.{u, w} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))) →
      Continuous[t, _] f
this rwa rwa₁ rwa₂ rwa₃ : Continuous[t, compactlyGenerated X] id
⊢ t ≤ compactlyGenerated X

Tactic:
rwa [← continuous_id_iff_le]

Premises used: continuous_id_iff_le
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        Continuous.{u, w} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))) →
      Continuous[t, _] f
suffices : Continuous[t, compactlyGenerated X] id
⊢ t ≤ compactlyGenerated X

Tactic:
suffices Continuous[t, compactlyGenerated.{u} X] (id : X → X) by
      rwa [← continuous_id_iff_le]
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        Continuous.{u, w} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))) →
      Continuous[t, _] f
a :
  ∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, compactlyGenerated X] (id ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
⊢ Continuous[t, compactlyGenerated X] id

Tactic:
apply h (tY := compactlyGenerated.{u} X)
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        Continuous.{u, w} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))) →
      Continuous[t, _] f
S : CompHaus
g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X
f : (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
    (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
              ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
          (P := fun (x : TopCat.{u}) ↦ True)) :
      Type u) →
  X :=
  fun
      (x :
        (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
    match (motive :=
      (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u) →
        X)
      x with
    | ⟨⟨fst, i⟩, s⟩ => (i : (a : (↑fst.toTop : Type u)) → X) s
a :
  ∀ (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, compactlyGenerated X]
      fun
        (a :
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      f
        (Sigma.mk (β :=
          fun
            (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ↦
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)
⊢ Continuous[_, compactlyGenerated X] (id ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))

Tactic:
suffices ∀ (i : (T : CompHaus.{u}) × C(T, X)),
      Continuous[inferInstance, compactlyGenerated X] (fun (a : i.fst) ↦ f ⟨i, a⟩) from this ⟨S, g⟩
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        Continuous.{u, w} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))) →
      Continuous[t, _] f
S : CompHaus
g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X
f : (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
    (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
              ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
          (P := fun (x : TopCat.{u}) ↦ True)) :
      Type u) →
  X :=
  fun
      (x :
        (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
    match (motive :=
      (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u) →
        X)
      x with
    | ⟨⟨fst, i⟩, s⟩ => (i : (a : (↑fst.toTop : Type u)) → X) s
a : Continuous[_, compactlyGenerated X] f
⊢ ∀ (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, compactlyGenerated X]
      fun
        (a :
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      f
        (Sigma.mk (β :=
          fun
            (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ↦
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)

Tactic:
rw [← @continuous_sigma_iff]

Premises used: continuous_sigma_iff
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        Continuous.{u, w} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))) →
      Continuous[t, _] f
S : CompHaus
g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X
f : (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
    (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
              ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
          (P := fun (x : TopCat.{u}) ↦ True)) :
      Type u) →
  X :=
  fun
      (x :
        (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
    match (motive :=
      (i : (T : CompHaus.{u}) × ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X) ×
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    ContinuousMap.{u, w} (↑(T.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u) →
        X)
      x with
    | ⟨⟨fst, i⟩, s⟩ => (i : (a : (↑fst.toTop : Type u)) → X) s
⊢ Continuous[_, compactlyGenerated X] f

Tactic:
apply continuous_coinduced_rng

Premises used: continuous_coinduced_rng
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
f : X → Y
h :
  ∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, tY] (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
apply : Continuous[compactlyGenerated X, tY] f
⊢ Continuous[tX, tY] f

Tactic:
apply continuous_le_dom UCompactlyGeneratedSpace.le_compactlyGenerated

Premises used: continuous_le_dom, UCompactlyGeneratedSpace.le_compactlyGenerated
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
f : X → Y
h :
  ∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, tY] (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
⊢ Continuous[compactlyGenerated X, tY] f

Tactic:
continuous_from_compactlyGenerated f h

Premises used: continuous_from_compactlyGenerated
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
f : X → Y
h :
  ∀ (S : CompHaus.{u}) (g : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    Continuous[_, tY] (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
⊢ Continuous[compactlyGenerated X, tY] f

Tactic:
exact continuous_from_compactlyGenerated f h

Premises used: continuous_from_compactlyGenerated
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (S : CompHaus.{u}) (f : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        IsClosed.{u} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          ((⇑f : (a : (↑S.toTop : Type u)) → X) ⁻¹' s)) →
      IsClosed[tX] s
⊢ UCompactlyGeneratedSpace X

Tactic:
uCompactlyGeneratedSpace_of_continuous_maps fun _ h' ↦
    continuous_iff_isClosed.2 fun _ hs ↦ h _ fun S g ↦ hs.preimage (h' S g)

Premises used: Iff.mpr, uCompactlyGeneratedSpace_of_continuous_maps, continuous_iff_isClosed, Set.preimage, IsClosed.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (S : CompHaus.{u}) (f : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
        IsOpen.{u} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          ((⇑f : (a : (↑S.toTop : Type u)) → X) ⁻¹' s)) →
      IsOpen[tX] s
⊢ UCompactlyGeneratedSpace X

Tactic:
uCompactlyGeneratedSpace_of_continuous_maps fun _ h' ↦
    continuous_def.2 fun _ hs ↦ h _ fun S g ↦ hs.preimage (h' S g)

Premises used: Iff.mpr, uCompactlyGeneratedSpace_of_continuous_maps, Set.preimage, IsOpen.preimage, continuous_def