mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
⊢ (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
⊢ (ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ = ↑x₂) = (x₁ = x₂)

Tactic:
]

Goal state after:
X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ = ↑x₂) = (x₁ = x₂)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
s : Set X
⊢ some '' sᶜ ∪ {∞} = some '' sᶜ ∪ {∞}

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ IsCompact {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ IsCompact {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j}
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x : OnePoint X
⊢ x = ∞ ↔ x = ∞

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
⊢ IsClosed (⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j})

Tactic:
]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} =
    ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}
⊢ IsClosed (⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j})
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (Prod.map π π ⁻¹' diagonal (Quotient R))

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (Prod.map π π ⁻¹' diagonal (Quotient R))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' t)
⊢ IsOpen[inst✝] (⋃ t ∈ S, some ⁻¹' t)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' t)
⊢ IsOpen[inst✝] (⋃ t ∈ S, some ⁻¹' t)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
⊢ IsOpen[inst✝] (some ⁻¹' s)ᶜ ↔ IsOpen[inst✝] (some ⁻¹' s)ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
⊢ IsClosed[inst✝] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s) ↔ IsClosed[inst✝] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝] s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
⊢ (∃ x, x • x₂ = x₁) ↔ ∃ a, a • x₂ = x₁

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ IsCompact s ↔ IsClosed[inst✝] s ∧ IsCompact s

pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ∧ IsCompact s ↔ IsClosed[inst✝] s ∧ IsCompact s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsOpen[instTopologicalSpace] (range some)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsOpen[instTopologicalSpace] (range some)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, t] (f ∘ ⇑g)
⊢ Continuous[_, t]
    (f ∘ fun x ↦
      match x with
      | ⟨⟨fst, i⟩, s⟩ => i s)

Tactic:
]

Goal state after:
X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, t] (f ∘ ⇑g)
⊢ Continuous[_, t]
    (f ∘ fun x ↦
      match x with
      | ⟨⟨fst, i⟩, s⟩ => i s)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
this : range f = {1} ×ˢ univ
⊢ IsClosed[instTopologicalSpaceProd] ({1} ×ˢ univ)

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
this : range f = {1} ×ˢ univ
⊢ IsClosed[instTopologicalSpaceProd] ({1} ×ˢ univ)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X

Tactic:
]

Goal state after:
X✝ : Type w
Y : Type x
X : Type v
t : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ ⊥ ≤ compactlyGenerated X
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
this : Continuous[t, compactlyGenerated X] id
⊢ Continuous[t, compactlyGenerated X] id

Tactic:
]

Goal state after:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
this : Continuous[t, compactlyGenerated X] id
⊢ Continuous[t, compactlyGenerated X] id
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = Function.diag
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (range (g ∘ f))

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = Function.diag
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (range (g ∘ f))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : NoncompactSpace X
⊢ (map some (coclosedCompact X)).NeBot

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : NoncompactSpace X
⊢ (map some (coclosedCompact X)).NeBot
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ y ∉ C

Tactic:
]

Goal state after:
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
⊢ y ∉ C
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝 ∞ = 𝓝 ∞

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x ↦ x)
this : (fun hx ↦ (hx.1 • hx.2, hx.2)) = fun hx ↦ (f hx.1 • hx.2, hx.2)
⊢ IsProperMap fun hx ↦ (f hx.1 • hx.2, hx.2)

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
H : Type u_3
inst✝³ : Group H
inst✝² : MulAction H X
inst✝¹ : TopologicalSpace H
inst✝ : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding ⇑f
f_compat : ∀ (h : H) (x : X), f h • x = h • x
h : IsProperMap (Prod.map ⇑f fun x ↦ x)
this : (fun hx ↦ (hx.1 • hx.2, hx.2)) = fun hx ↦ (f hx.1 • hx.2, hx.2)
⊢ IsProperMap fun hx ↦ (f hx.1 • hx.2, hx.2)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) fun s ↦ some '' sᶜ ∪ {∞}

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) fun s ↦ some '' sᶜ ∪ {∞}
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g

Tactic:
]

Goal state after:
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x ↦
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ Continuous[_, compactlyGenerated X] f

Tactic:
]

Goal state after:
X : Type w
t : TopologicalSpace X
h :
  ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y),
    (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous[t, _] f
S : CompHaus
g : C(↑S.toTop, X)
f : (i : (T : CompHaus) × C(↑T.toTop, X)) × ↑i.fst.toTop → X :=
  fun x ↦
    match x with
    | ⟨⟨fst, i⟩, s⟩ => i s
⊢ Continuous[_, compactlyGenerated X] f
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : Tendsto (⇑f) (coclosedCompact X) (𝓝 y)
⊢ Tendsto (fun x ↦ (↑x).elim y ⇑f) (coclosedCompact X) (𝓝 (∞.elim y ⇑f)) ∧
    Continuous[inst✝¹, inst✝] fun x ↦ (↑x).elim y ⇑f

Tactic:
]

Goal state after:
X : Type u_1
Y✝ : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : Tendsto (⇑f) (coclosedCompact X) (𝓝 y)
⊢ Tendsto (fun x ↦ (↑x).elim y ⇑f) (coclosedCompact X) (𝓝 (∞.elim y ⇑f)) ∧
    Continuous[inst✝¹, inst✝] fun x ↦ (↑x).elim y ⇑f
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ IsClosed[inst✝¹] (fst ∘ Ψ '' fst ⁻¹' s)

Tactic:
]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst✝²] s
ht : IsCompact t
Ψ : G × ↑t → X × ↑t := fun gx ↦ (gx.1 • ↑gx.2, gx.2)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ IsClosed[inst✝¹] (fst ∘ Ψ '' fst ⁻¹' s)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ (∃ a, (MulAction.toPerm g) a ∈ g • U ∧ (MulAction.toPerm g) a ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U

Tactic:
]

Goal state after:
X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ (∃ a, (MulAction.toPerm g) a ∈ g • U ∧ (MulAction.toPerm g) a ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Epi (↾⇑(ConcreteCategory.hom f)) → Epi f

Tactic:
]

Goal state after:
case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Epi (↾⇑(ConcreteCategory.hom f)) → Epi f
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsClosed
      (Sigma.mk i ⁻¹'
        (fun x ↦
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s)

Tactic:
]

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsClosed
      (Sigma.mk i ⁻¹'
        (fun x ↦
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
⊢ ProperSMul G X

Tactic:
by
  constructor
  let f : G × G → G × X := Prod.map id (fun g ↦ g • x)
  have hfsurj : f.Surjective := Function.surjective_id.prodMap (surjective_smul G x)
  refine isProperMap_of_comp_of_surj (by fun_prop) (by fun_prop) ?_ hfsurj
  simpa [Function.comp_def, Prod.map_apply, mul_smul]
    using! (hx.prodMap hx).comp (ProperSMul.isProperMap_smul_pair (G := G))

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint ℕ → Y
⊢ Tendsto (fun x ↦ f ↑x) atTop (𝓝 (f ∞)) ↔ Tendsto (fun x ↦ f ↑x) atTop (𝓝 (f ∞))

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsOpen
      (Sigma.mk i ⁻¹'
        (fun x ↦
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s)

Tactic:
]

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsOpen
      (Sigma.mk i ⁻¹'
        (fun x ↦
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝ : TopologicalSpace Y
f : ℕ → Y
y : Y
h : Tendsto f atTop (𝓝 y)
⊢ Tendsto f atTop (𝓝 y)

Tactic:
]

Goal state after:
X : Type u_1
Y✝ : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝ : TopologicalSpace Y
f : ℕ → Y
y : Y
h : Tendsto f atTop (𝓝 y)
⊢ Tendsto f atTop (𝓝 y)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)

Tactic:
]

Goal state after:
X : Type u_1
Y✝ : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) cofinite (𝓝 L)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)

Tactic:
]

Goal state after:
X : Type u_1
Y✝ : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : { f // ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L) }
f : ℕ → Y
hf : ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)
⊢ ∃ L, Tendsto (fun x ↦ f x) atTop (𝓝 L)
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MulAction G X
inst✝³ : CompactlyGeneratedSpace (X × X)
inst✝² : T2Space X
inst✝¹ : DiscreteTopology G
inst✝ : ContinuousConstSMul G X
this : ContinuousSMul G X
⊢ (∀ {K L : Set X}, IsCompact K → IsCompact L → {m | (m • K ∩ L).Nonempty}.Finite) ↔
    ∀ {U V : Set X}, IsCompact U → IsCompact V → {g | (g • U ∩ V).Nonempty}.Finite

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ