awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (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)
rw :
  ∀ (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    IsClosed.{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))
      (preimage (β :=
          (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))
          (Sigma.mk (β :=
            fun
              (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))
            i)
          ((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) ⁻¹'
            s) :
        Set
          (↑(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))
⊢ IsClosed[tX] s

Tactic:
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isClosed_coinduced,
    isClosed_sigma_iff]

Premises used: TopologicalSpace.compactlyGenerated, isClosed_sigma_iff, eq_compactlyGenerated, isClosed_coinduced
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (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)
⊢ ∀ (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    IsClosed.{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))
      (preimage (β :=
          (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))
          (Sigma.mk (β :=
            fun
              (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))
            i)
          ((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) ⁻¹'
            s) :
        Set
          (↑(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))

Tactic:
fun ⟨S, f⟩ ↦ hs S f

Premises used: TopologicalSpace.compactlyGenerated.match_1, _private.0.UCompactlyGeneratedSpace.isClosed.match_1, IsClosed, Set.preimage, Sigma.mk, DFunLike.coe
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (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)
⊢ ∀ (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    IsClosed.{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))
      (preimage (β :=
          (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))
          (Sigma.mk (β :=
            fun
              (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))
            i)
          ((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) ⁻¹'
            s) :
        Set
          (↑(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))

Tactic:
exact fun ⟨S, f⟩ ↦ hs S f
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (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)
rw :
  ∀ (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    IsOpen.{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))
      (preimage (β :=
          (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))
          (Sigma.mk (β :=
            fun
              (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))
            i)
          ((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) ⁻¹'
            s) :
        Set
          (↑(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))
⊢ IsOpen[tX] s

Tactic:
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isOpen_coinduced,
    isOpen_sigma_iff]

Premises used: TopologicalSpace.compactlyGenerated, isOpen_coinduced, eq_compactlyGenerated, isOpen_sigma_iff
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (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)
⊢ ∀ (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    IsOpen.{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))
      (preimage (β :=
          (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))
          (Sigma.mk (β :=
            fun
              (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))
            i)
          ((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) ⁻¹'
            s) :
        Set
          (↑(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))

Tactic:
fun ⟨S, f⟩ ↦ hs S f

Premises used: TopologicalSpace.compactlyGenerated.match_1, _private.0.UCompactlyGeneratedSpace.isClosed.match_1, Set.preimage, IsOpen, Sigma.mk, DFunLike.coe
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
tX : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (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)
⊢ ∀ (i : (S : CompHaus.{u}) × ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X),
    IsOpen.{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))
      (preimage (β :=
          (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))
          (Sigma.mk (β :=
            fun
              (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))
            i)
          ((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) ⁻¹'
            s) :
        Set
          (↑(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))

Tactic:
exact fun ⟨S, f⟩ ↦ hs S f
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
⊢ UCompactlyGeneratedSpace Y

Tactic:
uCompactlyGeneratedSpace_of_isClosed fun s h ↦ ?_

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

Tactic:
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ ?_

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

Tactic:
rw [ht, isClosed_coinduced]

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

Tactic:
UCompactlyGeneratedSpace.isClosed fun _ ⟨g, hg⟩ ↦ h _ ⟨_, hf.comp hg⟩

Premises used: ContinuousMap.mk, Continuous.comp, Function.comp, IsClosed, Set.preimage, _private.0.uCompactlyGeneratedSpace_of_coinduced.match_1, UCompactlyGeneratedSpace.isClosed, DFunLike.coe
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
s : Set Y
h :
  ∀ (S : CompHaus.{u}) (f : ContinuousMap.{u, x} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) Y),
    IsClosed.{u} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      ((⇑f : (a : (↑S.toTop : Type u)) → Y) ⁻¹' s)
⊢ IsClosed[tX] (f ⁻¹' s)

Tactic:
exact UCompactlyGeneratedSpace.isClosed fun _ ⟨g, hg⟩ ↦ h _ ⟨_, hf.comp hg⟩
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
S : Setoid X
inst : UCompactlyGeneratedSpace X
⊢ UCompactlyGeneratedSpace.{u, w} (Quotient S)

Tactic:
uCompactlyGeneratedSpace_of_coinduced continuous_quotient_mk' rfl

Premises used: continuous_quotient_mk', uCompactlyGeneratedSpace_of_coinduced, rfl
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
inst_1 : UCompactlyGeneratedSpace Y
⊢ UCompactlyGeneratedSpace (X ⊕ Y)

Tactic:
uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, uCompactlyGeneratedSpace_of_isClosed, isClosed_sum_iff
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
inst_1 : UCompactlyGeneratedSpace Y
refine_1 :
  ∀ (s : Set (X ⊕ Y))
    (h :
      ∀ (S : CompHaus) (f : C((↑(S.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)), X ⊕ Y)),
        IsClosed (X := (↑(S.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
          ((⇑f : (a : (↑S.toTop : Type (max u v))) → X ⊕ Y) ⁻¹' s)),
    IsClosed[tX] (Sum.inl ⁻¹' s)
refine_2 :
  ∀ (s : Set (X ⊕ Y))
    (h :
      ∀ (S : CompHaus) (f : C((↑(S.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)), X ⊕ Y)),
        IsClosed (X := (↑(S.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
          ((⇑f : (a : (↑S.toTop : Type (max u v))) → X ⊕ Y) ⁻¹' s)),
    IsClosed[tY] (Sum.inr ⁻¹' s)
⊢ UCompactlyGeneratedSpace (X ⊕ Y)

Tactic:
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, uCompactlyGeneratedSpace_of_isClosed, isClosed_sum_iff
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
inst_1 : UCompactlyGeneratedSpace Y
s : Set (X ⊕ Y)
h :
  ∀ (S : CompHaus) (f : C((↑(S.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)), X ⊕ Y)),
    IsClosed (X := (↑(S.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
      ((⇑f : (a : (↑S.toTop : Type (max u v))) → X ⊕ Y) ⁻¹' s)
⊢ IsClosed[tX] (Sum.inl ⁻¹' s)

Tactic:
UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_

Premises used: Sum.inl, IsClosed, Set.preimage, _private.0.uCompactlyGeneratedSpace_of_coinduced.match_1, UCompactlyGeneratedSpace.isClosed, DFunLike.coe