awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
⊢ Continuous[inst, instTopologicalSpace] ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) ↔
    Continuous[inst, inst_1] f
have rw : Continuous[inst, inst_1]
    (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
      ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
  Continuous[inst, inst_1] f
Tactic: rw [continuous_rng_of_compactSpace, ← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
rw :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
        ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[inst, inst_1] f
⊢ Continuous[inst, instTopologicalSpace] ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) ↔
    Continuous[inst, inst_1] f
have rw₁ : Continuous[inst, inst_1]
    (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
        (⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘
      f) ↔
  Continuous[inst, inst_1] f
Tactic: rw [continuous_rng_of_compactSpace, ← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
rw :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
        ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[inst, inst_1] f
rw₁ :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
          (⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘
        f) ↔
    Continuous[inst, inst_1] f
⊢ Continuous[inst, instTopologicalSpace] ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) ↔
    Continuous[inst, inst_1] f
have rw₂ : Continuous[inst, inst_1] (id ∘ f) ↔ Continuous[inst, inst_1] f
Tactic: rw [continuous_rng_of_compactSpace, ← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
rw :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
        ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
    Continuous[inst, inst_1] f
rw₁ :
  Continuous[inst, inst_1]
      (Function.comp (β := 𝐤Y) (⇑(CompactCoherentification.mk Y).symm : (a : 𝐤Y) → Y)
          (⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘
        f) ↔
    Continuous[inst, inst_1] f
rw₂ : Continuous[inst, inst_1] (id ∘ f) ↔ Continuous[inst, inst_1] f
⊢ Continuous[inst, instTopologicalSpace] ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) ↔
    Continuous[inst, inst_1] f
have rw₃ : Continuous[inst, inst_1] f ↔ Continuous[inst, inst_1] f
Tactic: rw [continuous_rng_of_compactSpace, ← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
⊢ ContinuousOn (Y := 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f) A ↔ ContinuousOn f A
have simp_rw : Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
    (A.restrict (π := fun (a : X) ↦ 𝐤Y) ((⇑(CompactCoherentification.mk Y) : (a : Y) → 𝐤Y) ∘ f)) ↔
  Continuous[instTopologicalSpaceSubtype, inst_1] (A.restrict (π := fun (a : X) ↦ Y) f)
Tactic: simp_rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set (𝐤X)
⊢ IsCompact K ↔ IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)
have mp : IsCompact K → IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set (𝐤X)
mp : IsCompact K → IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)
⊢ IsCompact K ↔ IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K)
have mpr : IsCompact (X := X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' K) → IsCompact K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
K : Set X
⊢ IsCompact (X := 𝐤X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' K) ↔ IsCompact K
have rw : IsCompact (X := X)
    (preimage (β := 𝐤X) (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X)
      ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' K)) ↔
  IsCompact K
Tactic: rw [isCompact_iff, Equiv.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
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
⊢ IsCompact (X := 𝐤X) ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) '' K) ↔ IsCompact K
have rw₁ : IsCompact K ↔ IsCompact K
Tactic: rw [isCompact_iff, Equiv.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ CompactlyCoherentSpace.{u_1} (𝐤X)
have 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)
Tactic: refine .of_isOpen_forall_compactSpace fun U hU ↦ isOpen_iff.mpr fun K hK ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (goal)
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
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ (⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ⁻¹' U)
have rw : IsOpen[instTopologicalSpaceSubtype]
  ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' U)
Tactic: rw [← preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyCoherentSpace (hypothesis)
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
⊢ IsOpen[instTopologicalSpaceSubtype]
    ((⇑(CompactCoherentification.mk X) : (a : X) → 𝐤X) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' U)
have this : CompactSpace.{u_1} (↑K : Type u_1)
Tactic: have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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[compactlyGenerated X, t] f
have 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)
Tactic: rw [continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
⊢ t = compactlyGenerated X
have a : t ≤ compactlyGenerated X
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
a : t ≤ compactlyGenerated X
⊢ t = compactlyGenerated X
have a₁ : compactlyGenerated X ≤ t
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X : Type w
t : TopologicalSpace X
inst : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t
have 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
Tactic: simp only [compactlyGenerated, ← continuous_iff_coinduced_le, continuous_sigma_iff,
      Sigma.forall]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
Goal:
X_1 : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst : DiscreteTopology X
⊢ t ≤ compactlyGenerated X
have rw : ⊥ ≤ compactlyGenerated X
Tactic: rw [DiscreteTopology.eq_bot (t := t)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
⊢ t ≤ compactlyGenerated X
have suffices : Continuous[t, compactlyGenerated X] id
Tactic: suffices Continuous[t, compactlyGenerated.{u} X] (id : X → X) by
      rwa [← continuous_id_iff_le]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
⊢ Continuous[t, compactlyGenerated X] id
have 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))
Tactic: apply h (tY := compactlyGenerated.{u} X)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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] (id ∘ (⇑g : (a : (↑S.toTop : Type u)) → X))
have 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)
Tactic: suffices ∀ (i : (T : CompHaus.{u}) × C(T, X)),
      Continuous[inferInstance, compactlyGenerated X] (fun (a : i.fst) ↦ f ⟨i, a⟩) from this ⟨S, g⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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
⊢ ∀ (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)
have a : Continuous[_, compactlyGenerated X] f
Tactic: rw [← @continuous_sigma_iff]
-- 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
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[tX, tY] f
have apply : Continuous[compactlyGenerated X, tY] f
Tactic: apply continuous_le_dom UCompactlyGeneratedSpace.le_compactlyGenerated
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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)
⊢ IsClosed[tX] s
have 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))
Tactic: rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isClosed_coinduced,
    isClosed_sigma_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CompactlyGeneratedSpace (goal)
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)
⊢ IsOpen[tX] s
have 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))
Tactic: rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isOpen_coinduced,
    isOpen_sigma_iff]
-- 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
⊢ UCompactlyGeneratedSpace Y
have 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
Tactic: refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ ?_