awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
C : Set X
hf : IsProperMap f
hC : IsClosed[inst] C
⊢ IsProperMap.{u_1, u_2} (Y := Y) fun (x : (↑C : Type u_1)) ↦ f (↑x : X)

Tactic:
hf.comp hC.isProperMap_subtypeVal

Premises used: IsClosed.isProperMap_subtypeVal, IsProperMap.comp
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsProperMap f
⊢ IsClosed[inst_1] (range f)

Tactic:
hf.isClosedMap.isClosed_range

Premises used: IsProperMap.isClosedMap, IsClosedMap.isClosed_range
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space Y
simp_rw :
  (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
⊢ IsProperMap f ↔ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite

Tactic:
simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto,
    le_cofinite_iff_compl_singleton_mem, mem_map, preimage_compl]

Premises used: Filter.le_cofinite_iff_compl_singleton_mem, Filter.Tendsto, isProperMap_iff_isClosedMap_and_compact_fibers, Set.preimage_compl, Filter.mem_map
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space Y
⊢ (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X

Tactic:
and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
    ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩

Premises used: IsCompact.compl_mem_cocompact, and_congr_right, Iff.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space Y
refine :
  ∀ (f_cont : Continuous[inst, inst_1] f),
    IsClosedMap f → ∀ (H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X) (y : Y), IsCompact (f ⁻¹' {y})
⊢ (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X

Tactic:
refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
    ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩

Premises used: and_congr_right, Iff.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space Y
f_cont : Continuous[inst, inst_1] f
h : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
rcases : ∀ (K : Set X) (hK : IsCompact K) (hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ), IsCompact (f ⁻¹' {y})
⊢ IsCompact (f ⁻¹' {y})

Tactic:
rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩

Premises used: Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space Y
f_cont : Continuous[inst, inst_1] f
h : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})

Tactic:
hK.of_isClosed_subset (isClosed_singleton.preimage f_cont)
    (compl_le_compl_iff_le.mp hKy)

Premises used: IsCompact.of_isClosed_subset, Iff.mp, compl_le_compl_iff_le, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space Y
f_cont : Continuous[inst, inst_1] f
h : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})

Tactic:
exact hK.of_isClosed_subset (isClosed_singleton.preimage f_cont)
    (compl_le_compl_iff_le.mp hKy)

Premises used: IsCompact.of_isClosed_subset, Iff.mp, compl_le_compl_iff_le, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
⊢ Tendsto f (cocompact X) cofinite

Tactic:
simp
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
rw :
  ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
    CompactSpace X
⊢ (IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ↔ CompactSpace X

Tactic:
rw [isProperMap_iff_isClosedMap_and_compact_fibers]

Premises used: isProperMap_iff_isClosedMap_and_compact_fibers
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
mp :
  ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) →
    CompactSpace X
mpr :
  CompactSpace X →
    (Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})
⊢ ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
    CompactSpace X

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
h : ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})
⊢ IsCompact.{u_1} (X := X) univ

Tactic:
simpa using h y
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
h : ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})
⊢ CompactSpace X

Tactic:
exact ⟨by simpa using h y⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
H : CompactSpace X
⊢ (Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})

Tactic:
⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩

Premises used: continuous_const, And.intro, isClosedMap_const
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
H : CompactSpace X
mpr : ∀ (y' : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y'})
⊢ (Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})

Tactic:
refine ⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
H : CompactSpace X
y' : Y
⊢ IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y'})

Tactic:
simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]

Premises used: Set.preimage_const, apply_ite, Set.mem_singleton_iff, isCompact_univ
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
rw rw₁ rw₂ :
  ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
    CompactSpace X
mp :
  ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) →
    CompactSpace X
mpr mpr₁ :
  CompactSpace X →
    (Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})
⊢ (IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ↔ CompactSpace X

Tactic:
classical
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  constructor
  · rintro ⟨-, -, h⟩
    exact ⟨by simpa using h y⟩
  · intro H
    refine ⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩
    simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]

Premises used: Set.preimage_const, apply_ite, Set.mem_singleton_iff, isCompact_univ, isProperMap_iff_isClosedMap_and_compact_fibers
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : CompactSpace X
inst_2 : T1Space Y
y : Y
⊢ IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y

Tactic:
isProperMap_const_iff y |>.mpr h

Premises used: Iff.mpr, isProperMap_const_iff
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
⊢ IsProperMap (X := X × Y) fst

Tactic:
Homeomorph.prodPUnit X |>.isProperMap.comp (isProperMap_id.prodMap (isProperMap_const ()))

Premises used: Unit.unit, Homeomorph.prodPUnit, Homeomorph.isProperMap, isProperMap_const, IsProperMap.prodMap, isProperMap_id, IsProperMap.comp
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
⊢ IsProperMap (X := X × Y) snd

Tactic:
Homeomorph.punitProd Y |>.isProperMap.comp ((isProperMap_const ()).prodMap isProperMap_id)

Premises used: Unit.unit, Homeomorph.isProperMap, isProperMap_const, IsProperMap.prodMap, isProperMap_id, Homeomorph.punitProd, IsProperMap.comp
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace Y
⊢ IsClosedMap (X := X × Y) fst

Tactic:
isProperMap_fst_of_compactSpace.isClosedMap

Premises used: IsProperMap.isClosedMap, isProperMap_fst_of_compactSpace
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
⊢ IsClosedMap (X := X × Y) snd

Tactic:
isProperMap_snd_of_compactSpace.isClosedMap

Premises used: isProperMap_snd_of_compactSpace, IsProperMap.isClosedMap
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
Z : Type u_6
inst_2 : TopologicalSpace Z
h : IsProperMap f
⊢ IsClosedMap (X := X × Z) (Prod.map f id)

Tactic:
(h.prodMap isProperMap_id).isClosedMap

Premises used: IsProperMap.isClosedMap, IsProperMap.prodMap, isProperMap_id
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
h_1 : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
hf : Continuous f
h : ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
s : Set X
hs : IsClosed s
K : Set Y
hK : IsCompact K
⊢ IsClosed (X := { x : Y // x ∈ K }) (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' (s ∩ f ⁻¹' K))

Tactic:
(((h hK).inter_left hs).image hf).isClosed.preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsCompact.inter_left, IsClosed.preimage, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
h_1 : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
hf : Continuous f
h : ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
s : Set X
hs : IsClosed s
K : Set Y
hK : IsCompact K
h₁ :
  (↑K : Type u_2) = { x : Y // x ∈ K } →
    Eq (α := Set (↑K : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' s)
      (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' (s ∩ f ⁻¹' K))
⊢ IsClosed (X := (↑K : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' s)

Tactic:
convert! (((h hK).inter_left hs).image hf).isClosed.preimage continuous_subtype_val using 1

Premises used: continuous_subtype_val, IsCompact.inter_left, IsClosed.preimage, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
h_1 : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
hf : Continuous f
h : ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
s : Set X
hs : IsClosed s
K : Set Y
hK : IsCompact K
e_1 : (↑K : Type u_2) = { x : Y // x ∈ K }
⊢ Eq (α := Set (↑K : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' s)
    (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' (s ∩ f ⁻¹' K))

Tactic:
aesop
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
simp_rw :
  (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)

Tactic:
simp_rw [isProperMap_iff_isCompact_preimage,
    hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set, preimage_compl]

Premises used: isProperMap_iff_isCompact_preimage, Filter.hasBasis_cocompact, Filter.HasBasis.tendsto_right_iff, Set.preimage_compl, Filter.eventually_mem_set, Set.mem_preimage
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X

Tactic:
and_congr_right fun f_cont ↦
    ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩

Premises used: IsCompact.compl_mem_cocompact, and_congr_right, Iff.intro
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
refine :
  ∀ (f_cont : Continuous f) (H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X) (K : Set Y) (hK : IsCompact K),
    IsCompact (f ⁻¹' K)
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X

Tactic:
refine and_congr_right fun f_cont ↦
    ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩

Premises used: and_congr_right, Iff.intro
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
rcases : ∀ (K' : Set X) (hK' : IsCompact K') (hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ), IsCompact (f ⁻¹' K)
⊢ IsCompact (f ⁻¹' K)

Tactic:
rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩

Premises used: Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ
⊢ IsCompact (f ⁻¹' K)

Tactic:
hK'.of_isClosed_subset (hK.isClosed.preimage f_cont)
    (compl_le_compl_iff_le.mp hK'y)

Premises used: IsCompact.of_isClosed_subset, Iff.mp, compl_le_compl_iff_le, IsClosed.preimage, IsCompact.isClosed
-- Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ
⊢ IsCompact (f ⁻¹' K)

Tactic:
exact hK'.of_isClosed_subset (hK.isClosed.preimage f_cont)
    (compl_le_compl_iff_le.mp hK'y)

Premises used: IsCompact.of_isClosed_subset, Iff.mp, compl_le_compl_iff_le, IsClosed.preimage, IsCompact.isClosed
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
mp : IsProperMap f → Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
mpr : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id) → IsProperMap f
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)

Tactic:
⟨H.continuous, H.universally_closed _⟩

Premises used: IsProperMap.universally_closed, And.intro, IsProperMap.continuous
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)

Tactic:
exact ⟨H.continuous, H.universally_closed _⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
mpr :
  Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter]

Premises used: isProperMap_iff_ultrafilter
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
⊢ Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x

Tactic:
⟨H.1, fun 𝒰 y hy ↦ ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
mpr :
  ∀ (𝒰 : Ultrafilter X) (y : Y) (hy : Tendsto f (↑𝒰 : Filter X) (nhds y)), ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
⊢ Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x

Tactic:
refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
⊢ IsClosed (Prod.map f id '' F)

Tactic:
have := H.2 F isClosed_closure
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ (y, (↑𝒰 : Filter X)) ∈ Prod.map f id '' F

Tactic:
have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
  -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
  -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
  -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
  -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
  -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.
      this.mem_of_tendsto (hy.prodMk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this_1 : IsClosed (Prod.map f id '' F)
this : (y, (↑𝒰 : Filter X)) ∈ Prod.map f id '' F
mpr :
  ∀ (x : X) (hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))) (hx : (x, 𝒰.1) ∈ F),
    ∃ (x_1 : X), f x_1 = f x ∧ (↑𝒰 : Filter X) ≤ nhds x_1
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x

Tactic:
rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx : (x, 𝒰.1) ∈ F
⊢ ∃ (x_1 : X), f x_1 = f x ∧ (↑𝒰 : Filter X) ≤ nhds x_1

Tactic:
⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩

Premises used: Ultrafilter.compl_notMem_iff, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx : (x, 𝒰.1) ∈ F
mpr : ∀ (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ 𝒰), False
⊢ ∃ (x_1 : X), f x_1 = f x ∧ (↑𝒰 : Filter X) ≤ nhds x_1

Tactic:
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.UniversallyClosed
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx : (x, 𝒰.1) ∈ F
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
mpr :
  ∀
    (hx :
      ∀ (t : Set (X × Filter X)),
        Membership.mem (γ := Filter (X × Filter X)) (nhds (x, 𝒰.1)) t →
          (t ∩ {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}).Nonempty)
    (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ 𝒰), False
⊢ False

Tactic:
rw [mem_closure_iff_nhds] at hx

Premises used: mem_closure_iff_nhds