awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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[tY] s
have rw : IsClosed[tX] (f ⁻¹' s)
Tactic: rw [ht, isClosed_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : UCompactlyGeneratedSpace X
inst_1 : UCompactlyGeneratedSpace Y
⊢ UCompactlyGeneratedSpace (X ⊕ Y)
have 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)
Tactic: refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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)
⊢ UCompactlyGeneratedSpace (X ⊕ Y)
have 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)
Tactic: refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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)
have 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)
Tactic: refine UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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)
have 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)
Tactic: refine UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (hypothesis)
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
⊢ 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)
have hg : Continuous[_, instTopologicalSpaceSum] g
Tactic: have hg : Continuous g := continuous_inl.comp <| hf.comp continuous_uliftDown
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (hypothesis)
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
⊢ 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)
have hg : Continuous[_, instTopologicalSpaceSum] g
Tactic: have hg : Continuous g := continuous_inr.comp <| hf.comp continuous_uliftDown
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst : SequentialSpace X
⊢ UCompactlyGeneratedSpace X
have 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
Tactic: refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦
    SequentialSpace.isClosed_of_seq _ fun u p hu hup ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
⊢ p ∈ s
have change : { down := ∞ } ∈ g ⁻¹' s
Tactic: change ULift.up ∞ ∈ g ⁻¹' s
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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 (𝓝 ∞)
have rw : Tendsto OnePoint.some (coclosedCompact ℕ) (𝓝 ∞)
Tactic: rw [← Nat.cofinite_eq_atTop, ← cocompact_eq_cofinite, ← coclosedCompact_eq_cocompact]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (hypothesis)
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
⊢ { down := ∞ } ∈ g ⁻¹' s
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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 (𝓝 ∞)
⊢ { down := ∞ } ∈ g ⁻¹' s
have apply : ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s
Tactic: apply IsClosed.mem_of_tendsto _ ((continuous_uliftUp.tendsto ∞).comp this)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
⊢ { down := ∞ } ∈ g ⁻¹' s
have apply₁ : IsClosed (g ⁻¹' s)
Tactic: apply IsClosed.mem_of_tendsto _ ((continuous_uliftUp.tendsto ∞).comp this)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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 (𝓝 ∞)
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → g { down := (↑b : OnePoint ℕ) : ULift.{u, 0} (OnePoint ℕ) } ∈ s
Tactic: simp only [Function.comp_apply, mem_preimage, eventually_atTop, ge_iff_le]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
have refine : ∀ (K : Type u) (x : TopologicalSpace K),
  CompactSpace K → T2Space K → ∀ (f : K → X) (hf : Continuous[_, inst] f), IsClosed (f ⁻¹' s)
Tactic: refine isClosed' fun K _ _ _ f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
⊢ IsClosed[x] (f ⁻¹' s)
have rw : IsClosed[x] (f ⁻¹' (s ∩ range f))
Tactic: rw [← Set.preimage_inter_range]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
⊢ IsOpen[inst] s
have refine : ∀ (K : Type u) (x : TopologicalSpace K),
  CompactSpace K → T2Space K → ∀ (f : K → X) (hf : Continuous[_, inst] f), IsOpen (f ⁻¹' s)
Tactic: refine isOpen' fun K _ _ _ f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
⊢ IsOpen[x] (f ⁻¹' s)
have rw : IsOpen[x] (f ⁻¹' (s ∩ range f))
Tactic: rw [← Set.preimage_inter_range]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
⊢ CompactlyGeneratedSpace ((i : ι) × X i)
have refine : ∀ (s : Set ((i : ι) × X i))
  (h :
    ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
      Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s))
  (i : ι) (K : Type v) (x : TopologicalSpace K),
  CompactSpace K →
    T2Space K →
      ∀ (f : K → X i) (hf : Continuous[_, inst_2 i] f), IsClosed (f ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
Tactic: refine compactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sigma_iff.2 fun i ↦
    CompactlyGeneratedSpace.isClosed' fun K _ _ _ f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (hypothesis)
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
s : Set ((i : ι) × X i)
h :
  ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
    Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s)
i : ι
K : Type v
x : TopologicalSpace K
h_1 : CompactSpace K
h_2 : T2Space K
f : K → X i
hf : Continuous[x, inst_2 i] f
g : ULift.{u, v} K → (i : ι) × X i := Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ f ∘ ULift.down
⊢ IsClosed[x] (f ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
have hg : Continuous[ULift.topologicalSpace, instTopologicalSpaceSigma] g
Tactic: have hg : Continuous g := continuous_sigmaMk.comp <| hf.comp continuous_uliftDown
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
⊢ CompactlyGeneratedSpace X
have refine : ∀ (s : Set X)
  (hs :
    ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
      Continuous[_, inst] f → IsClosed (f ⁻¹' s))
  (K : Set X) (hK : IsCompact K), IsClosed[inst] (s ∩ K)
Tactic: refine compactlyGeneratedSpace_of_isClosed fun s hs ↦ h s fun K hK ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst] (s ∩ K)
have rw : IsClosed[inst]
  (image (α := { x : X // x ∈ K }) (Subtype.val (p := fun (x : X) ↦ x ∈ K))
    (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s))
Tactic: rw [Set.inter_comm, ← Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst]
    (image (α := { x : X // x ∈ K }) (Subtype.val (p := fun (x : X) ↦ x ∈ K))
      (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s))
have a : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)
Tactic: apply hK.isClosed.isClosedMap_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)
have this : CompactSpace.{u} (↑K : Type u)
Tactic: have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
⊢ CompactlyGeneratedSpace X
have refine : ∀ (s : Set X)
  (hs :
    ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
      Continuous[_, inst] f → IsOpen (f ⁻¹' s))
  (K : Set X) (hK : IsCompact K), IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
Tactic: refine compactlyGeneratedSpace_of_isOpen fun s hs ↦ h s fun K hK ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
have this : CompactSpace.{u} (↑K : Type u)
Tactic: have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
⊢ CompactlyGeneratedSpace X
have refine : ∀ (s : Set X) (h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)), IsClosed[inst] s
Tactic: refine compactlyGeneratedSpace_of_isClosed_of_t2 fun s h ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
⊢ IsClosed[inst] s
have rw : ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
Tactic: rw [isClosed_iff_forall_filter]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
hℱ₃ : ℱ ≤ 𝓝 x
⊢ x ∈ s
have rcases : ∀ (K : Set X) (hK : IsCompact K) (K_mem : K ∈ 𝓝 x), x ∈ s
Tactic: rcases exists_compact_mem_nhds x with ⟨K, hK, K_mem⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
⊢ CompactlyGeneratedSpace X
have h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
Tactic: apply compactlyGeneratedSpace_of_isClosed_of_t2
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
⊢ IsClosed[inst] s
have h : ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)
Tactic: rw [CompactlyCoherentSpace.isClosed_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)
have h : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' (s ∩ K))
Tactic: rw [← Subtype.preimage_coe_inter_self]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
⊢ ∃ a ∈ A, ClusterPt a f
have obtain : ∀ (x : ℕ → E) (hx : Tendsto x atTop f), ∃ a ∈ A, ClusterPt a f
Tactic: obtain ⟨x, hx⟩ := f.exists_seq_tendsto
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
⊢ ∃ a ∈ A, ClusterPt a f
have obtain : ∀ (a : E) (ha : a ∈ A) (hxa : MapClusterPt a atTop x), ∃ a ∈ A, ClusterPt a f
Tactic: obtain ⟨a, ha, hxa⟩ := hA x (by simpa using hx.mono_right hle)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : Countable ι
inst_2 : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) U
⊢ ∃ (i : ι), A ⊆ U i
have by_contra! : ∀ (h : ∀ (i : ι), ¬A ⊆ U i), False
Tactic: by_contra! h