awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
refine_1 :
  ∀ (S : CompHaus.{u}) (x : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X)
    (f : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X) (hf : Continuous[_, tX] f),
    IsClosed.{u} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      ((⇑{ toFun := f, continuous_toFun := hf :
              ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X } :
          (a : (↑S.toTop : Type u)) → X) ⁻¹'
        Sum.inl ⁻¹' s)
⊢ IsClosed[tX] (Sum.inl ⁻¹' s)

Tactic:
refine UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_
-- 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[tY] (Sum.inr ⁻¹' s)

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

Premises used: IsClosed, Set.preimage, Sum.inr, _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
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)
refine_2 :
  ∀ (S : CompHaus.{v}) (x : ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y)
    (f : (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → Y) (hf : Continuous[_, tY] f),
    IsClosed.{v} (X := (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v))
      ((⇑{ toFun := f, continuous_toFun := hf :
              ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y } :
          (a : (↑S.toTop : Type v)) → Y) ⁻¹'
        Sum.inr ⁻¹' s)
⊢ IsClosed[tY] (Sum.inr ⁻¹' s)

Tactic:
refine UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_
-- 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)
S : CompHaus
x : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X
f : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X
hf : Continuous[_, tX] f
g : ULift.{v, u} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X ⊕ Y := Sum.inl ∘ f ∘ ULift.down
⊢ Continuous[_, instTopologicalSpaceSum] g

Tactic:
have hg : Continuous g := continuous_inl.comp <| hf.comp continuous_uliftDown
-- 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)
S : CompHaus
x : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X
f : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X
hf : Continuous[_, tX] f
g : ULift.{v, u} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X ⊕ Y := Sum.inl ∘ f ∘ ULift.down
hg : Continuous[_, instTopologicalSpaceSum] g
⊢ IsClosed.{u} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
    ((⇑{ toFun := f, continuous_toFun := hf :
            ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X } :
        (a : (↑S.toTop : Type u)) → X) ⁻¹'
      Sum.inl ⁻¹' s)

Tactic:
(h (CompHaus.of (ULift.{v} S)) ⟨g, hg⟩).preimage continuous_uliftUp

Premises used: Set.Mem, ContinuousMap.mk, setOf, ULift, continuous_uliftUp, TopCat.carrier, Set.preimage, IsClosed.preimage, CompHausLike.toTop, CompHaus.of
-- 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)
S : CompHaus
x : ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X
f : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X
hf : Continuous[_, tX] f
g : ULift.{v, u} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → X ⊕ Y := Sum.inl ∘ f ∘ ULift.down
hg : Continuous[_, instTopologicalSpaceSum] g
⊢ IsClosed.{u} (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
    ((⇑{ toFun := f, continuous_toFun := hf :
            ContinuousMap.{u, w} (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) X } :
        (a : (↑S.toTop : Type u)) → X) ⁻¹'
      Sum.inl ⁻¹' s)

Tactic:
exact (h (CompHaus.of (ULift.{v} S)) ⟨g, hg⟩).preimage continuous_uliftUp
-- 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)
S : CompHaus
x : ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y
f : (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → Y
hf : Continuous[_, tY] f
g : ULift.{u, v} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → X ⊕ Y := Sum.inr ∘ f ∘ ULift.down
⊢ Continuous[_, instTopologicalSpaceSum] g

Tactic:
have hg : Continuous g := continuous_inr.comp <| hf.comp continuous_uliftDown
-- 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)
S : CompHaus
x : ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y
f : (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → Y
hf : Continuous[_, tY] f
g : ULift.{u, v} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → X ⊕ Y := Sum.inr ∘ f ∘ ULift.down
hg : Continuous[_, instTopologicalSpaceSum] g
⊢ IsClosed.{v} (X := (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v))
    ((⇑{ toFun := f, continuous_toFun := hf :
            ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y } :
        (a : (↑S.toTop : Type v)) → Y) ⁻¹'
      Sum.inr ⁻¹' s)

Tactic:
(h (CompHaus.of (ULift.{u} S)) ⟨g, hg⟩).preimage continuous_uliftUp

Premises used: Set.Mem, ContinuousMap.mk, setOf, ULift, continuous_uliftUp, TopCat.carrier, Set.preimage, IsClosed.preimage, CompHausLike.toTop, CompHaus.of
-- 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)
S : CompHaus
x : ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y
f : (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → Y
hf : Continuous[_, tY] f
g : ULift.{u, v} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) → X ⊕ Y := Sum.inr ∘ f ∘ ULift.down
hg : Continuous[_, instTopologicalSpaceSum] g
⊢ IsClosed.{v} (X := (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v))
    ((⇑{ toFun := f, continuous_toFun := hf :
            ContinuousMap.{v, x} (↑(S.toTop (P := fun (x : TopCat.{v}) ↦ True)) : Type v) Y } :
        (a : (↑S.toTop : Type v)) → Y) ⁻¹'
      Sum.inr ⁻¹' s)

Tactic:
exact (h (CompHaus.of (ULift.{u} S)) ⟨g, hg⟩).preimage continuous_uliftUp
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type w
Y : Type x
tX : TopologicalSpace X_1
tY : TopologicalSpace Y
ι : Type v
X : ι → Type w
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), UCompactlyGeneratedSpace.{u, w} (X i)
⊢ UCompactlyGeneratedSpace ((i : ι) × X i)

Tactic:
uCompactlyGeneratedSpace_of_isClosed fun _ h ↦ isClosed_sigma_iff.2 fun i ↦
    UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦
      h S ⟨Sigma.mk i ∘ f, continuous_sigmaMk.comp hf⟩

Premises used: Iff.mpr, ContinuousMap.mk, Continuous.comp, _private.0.instUCompactlyGeneratedSpaceSigma.match_1, continuous_sigmaMk, Function.comp, IsClosed, Set.preimage, isClosed_sigma_iff, UCompactlyGeneratedSpace.isClosed, uCompactlyGeneratedSpace_of_isClosed, Sigma.mk, DFunLike.coe
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
⊢ UCompactlyGeneratedSpace X

Tactic:
uCompactlyGeneratedSpace_of_isClosed fun s h ↦
    SequentialSpace.isClosed_of_seq _ fun u p hu hup ↦ ?_

Premises used: SequentialSpace.isClosed_of_seq, uCompactlyGeneratedSpace_of_isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
refine :
  ∀ (s : Set X)
    (h :
      ∀ (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))
    (u : ℕ → X) (p : X) (hu : ∀ (n : ℕ), u n ∈ s) (hup : Tendsto u atTop (𝓝 p)), p ∈ s
⊢ UCompactlyGeneratedSpace X

Tactic:
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦
    SequentialSpace.isClosed_of_seq _ fun u p hu hup ↦ ?_

Premises used: SequentialSpace.isClosed_of_seq, uCompactlyGeneratedSpace_of_isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
change : { down := ∞ } ∈ g ⁻¹' s
⊢ p ∈ s

Tactic:
change ULift.up ∞ ∈ g ⁻¹' s

Premises used: OnePoint.infty, ULift.up
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
rw : Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)
⊢ Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)

Tactic:
rw [← Nat.cofinite_eq_atTop, ← cocompact_eq_cofinite, ← coclosedCompact_eq_cocompact]

Premises used: Filter.coclosedCompact_eq_cocompact, Nat.cofinite_eq_atTop, Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
⊢ Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)

Tactic:
tendsto_coe_infty

Premises used: OnePoint.tendsto_coe_infty
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
⊢ Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)

Tactic:
exact tendsto_coe_infty

Premises used: OnePoint.tendsto_coe_infty
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
⊢ Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)

Tactic:
have : Filter.Tendsto (@OnePoint.some ℕ) Filter.atTop (𝓝 ∞) := by
    rw [← Nat.cofinite_eq_atTop, ← cocompact_eq_cofinite, ← coclosedCompact_eq_cocompact]
    exact tendsto_coe_infty
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
this : Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)
apply : ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s
apply₁ : IsClosed (g ⁻¹' s)
⊢ { down := ∞ } ∈ g ⁻¹' s

Tactic:
apply IsClosed.mem_of_tendsto _ ((continuous_uliftUp.tendsto ∞).comp this)

Premises used: OnePoint.infty, continuous_uliftUp, IsClosed.mem_of_tendsto, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
this : Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)
simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → g { down := (↑b : OnePoint ℕ) : ULift.{u, 0} (OnePoint ℕ) } ∈ s
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s

Tactic:
simp only [Function.comp_apply, mem_preimage, eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Function.comp_apply, Filter.eventually_atTop, Set.mem_preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
this : Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → g { down := (↑b : OnePoint ℕ) : ULift.{u, 0} (OnePoint ℕ) } ∈ s

Tactic:
⟨0, fun b _ ↦ hu b⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
this : Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → g { down := (↑b : OnePoint ℕ) : ULift.{u, 0} (OnePoint ℕ) } ∈ s

Tactic:
exact ⟨0, fun b _ ↦ hu b⟩
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
this : Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)
⊢ Continuous[_, tX] g

Tactic:
fun_prop
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
s : Set X
h :
  ∀ (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)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := (⇑(continuousMapMkNat u p hup) : (a : OnePoint ℕ) → X) ∘ ULift.down
this : Tendsto (α := ℕ) OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)

Tactic:
exact h (CompHaus.of (ULift.{u} (OnePoint ℕ))) ⟨g, by fun_prop⟩
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactlyGeneratedSpace X
f : X → Y
h :
  ∀ (K : Type u) [inst_3 : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X),
    Continuous[_, inst] g → Continuous[_, inst_1] (f ∘ g)
⊢ Continuous[inst, inst_1] f

Tactic:
continuous_from_uCompactlyGeneratedSpace f fun K ⟨g, hg⟩ ↦ h K g hg

Premises used: Continuous, Function.comp, continuous_from_uCompactlyGeneratedSpace, TopCat.carrier, CompHausLike.toTop, DFunLike.coe, _private.0.continuous_from_compactlyGeneratedSpace.match_1
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ {Y : Type u} [inst_1 : TopologicalSpace Y] (f : X → Y),
    (∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X),
        Continuous[_, inst] g → Continuous (f ∘ g)) →
      Continuous[inst, _] f
⊢ CompactlyGeneratedSpace X

Tactic:
uCompactlyGeneratedSpace_of_continuous_maps fun f h' ↦ h f fun K _ _ _ g hg ↦
    h' (CompHaus.of K) ⟨g, hg⟩

Premises used: ContinuousMap.mk, uCompactlyGeneratedSpace_of_continuous_maps, CompHaus.of
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
        Continuous[_, inst] f → IsClosed (f ⁻¹' s)) →
      IsClosed[inst] s
⊢ CompactlyGeneratedSpace X

Tactic:
uCompactlyGeneratedSpace_of_isClosed fun s h' ↦ h s fun K _ _ _ f hf ↦ h' (CompHaus.of K) ⟨f, hf⟩

Premises used: ContinuousMap.mk, uCompactlyGeneratedSpace_of_isClosed, CompHaus.of
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
⊢ IsClosed[inst] s

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

Premises used: IsClosed, TopCat.carrier, Set.preimage, UCompactlyGeneratedSpace.isClosed, CompHausLike.toTop, DFunLike.coe, _private.0.continuous_from_compactlyGeneratedSpace.match_1
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst] (s ∩ K)
⊢ IsClosed[inst] s

Tactic:
isClosed' fun K _ _ _ f hf ↦ ?_

Premises used: CompactlyGeneratedSpace.isClosed'
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst] (s ∩ K)
refine :
  ∀ (K : Type u) (x : TopologicalSpace K),
    CompactSpace K → T2Space K → ∀ (f : K → X) (hf : Continuous[_, inst] f), IsClosed (f ⁻¹' s)
⊢ IsClosed[inst] s

Tactic:
refine isClosed' fun K _ _ _ f hf ↦ ?_

Premises used: CompactlyGeneratedSpace.isClosed'
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
rw : IsClosed[x] (f ⁻¹' (s ∩ range f))
⊢ IsClosed[x] (f ⁻¹' s)

Tactic:
rw [← Set.preimage_inter_range]

Premises used: Set.preimage_inter_range