awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf :
  Continuous[inst, inst_1] f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
hg :
  Continuous[inst_2, inst_3] g ∧
    ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰 : Filter Z) (𝓝 y) → ∃ (x : Z), g x = y ∧ (↑𝒰 : Filter Z) ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw :
  Tendsto (fun (n : X × Z) ↦ (Prod.map f g n).1) (↑𝒰 : Filter (X × Z)) (𝓝 y) ∧
    Tendsto (fun (n : X × Z) ↦ (Prod.map f g n).2) (↑𝒰 : Filter (X × Z)) (𝓝 w)
x : X
hxy : f x = y
hx : (↑(Ultrafilter.map fst 𝒰) : Filter X) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : (↑(Ultrafilter.map snd 𝒰) : Filter Z) ≤ 𝓝 z
⊢ Tendsto fst (↑𝒰 : Filter (X × Z)) (𝓝 x) ∧ Tendsto snd (↑𝒰 : Filter (X × Z)) (𝓝 z)

Tactic:
⟨hx, hz⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace W
f : X → Y
g : Z → W
hf :
  Continuous[inst, inst_1] f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
hg :
  Continuous[inst_2, inst_3] g ∧
    ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰 : Filter Z) (𝓝 y) → ∃ (x : Z), g x = y ∧ (↑𝒰 : Filter Z) ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw :
  Tendsto (fun (n : X × Z) ↦ (Prod.map f g n).1) (↑𝒰 : Filter (X × Z)) (𝓝 y) ∧
    Tendsto (fun (n : X × Z) ↦ (Prod.map f g n).2) (↑𝒰 : Filter (X × Z)) (𝓝 w)
x : X
hxy : f x = y
hx : (↑(Ultrafilter.map fst 𝒰) : Filter X) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : (↑(Ultrafilter.map snd 𝒰) : Filter Z) ≤ 𝓝 z
⊢ Tendsto fst (↑𝒰 : Filter (X × Z)) (𝓝 x) ∧ Tendsto snd (↑𝒰 : Filter (X × Z)) (𝓝 z)

Tactic:
exact ⟨hx, hz⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h : ∀ (i : ι), IsProperMap (f i)
simp_rw :
  ∀
    (h :
      ∀ (i : ι),
        Continuous[inst i, inst_1 i] (f i) ∧
          ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
            Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x),
    (Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ∧
      ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
        Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y) →
          ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
⊢ IsProperMap (Y := (i : ι) → Y i) fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)

Tactic:
simp_rw [isProperMap_iff_ultrafilter] at h ⊢

Premises used: isProperMap_iff_ultrafilter
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
left : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)
right :
  ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y) →
      ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
⊢ (Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ∧
    ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
      Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y) →
        ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)

Tactic:
continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)

Premises used: Continuous.comp, continuous_pi, And.left, continuous_apply
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)

Tactic:
exact continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)

Premises used: Continuous.comp, continuous_pi, And.left, continuous_apply
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y)
⊢ ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) (𝓝 (y i))

Tactic:
simpa [tendsto_pi_nhds] using hy

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y)
⊢ ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) (𝓝 (y i))

Tactic:
have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by
      simpa [tendsto_pi_nhds] using hy
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) (𝓝 (y i))
right :
  ∀ (x : (i : ι) → X i) (hxy : ∀ (i : ι), f i (x i) = y i)
    (hx : ∀ (i : ι), (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) ≤ 𝓝 (x i)),
    ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
⊢ ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x

Tactic:
choose x hxy hx using fun i ↦ (h i).2 (this i)

Premises used: And.right
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) ≤ 𝓝 (x i)
⊢ ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x

Tactic:
⟨x, funext hxy, ?_⟩

Premises used: funext, And.intro, Exists.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) ≤ 𝓝 (x i)
right : (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
⊢ ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x

Tactic:
refine ⟨x, funext hxy, ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst i, inst_1 i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄,
        Tendsto (f i) (↑𝒰 : Filter (X i)) (𝓝 y) → ∃ (x : X i), f i x = y ∧ (↑𝒰 : Filter (X i)) ≤ 𝓝 x
𝒰 : Ultrafilter ((i : ι) → X i)
y : (i : ι) → Y i
hy : Tendsto (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 y)
this : ∀ (i : ι), Tendsto (f i) (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) (𝓝 (y i))
x : (i : ι) → X i
hxy : ∀ (i : ι), f i (x i) = y i
hx : ∀ (i : ι), (↑(Ultrafilter.map (eval (β := X) i) 𝒰) : Filter (X i)) ≤ 𝓝 (x i)
right : (↑𝒰 : Filter ((i : ι) → X i)) ≤ Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (x i)
right₁ right₂ right₃ right₄ : ∀ (i : ι), Tendsto (eval (β := X) i) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 (x i))
⊢ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x

Tactic:
rwa [nhds_pi, le_pi]

Premises used: nhds_pi, Filter.le_pi
-- 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
h : IsProperMap f
K : Set Y
hK : IsCompact K
rw : ∀ (f_1 : Ultrafilter X), (↑f_1 : Filter X) ≤ 𝓟 (f ⁻¹' K) → ∃ x ∈ f ⁻¹' K, (↑f_1 : Filter X) ≤ 𝓝 x
⊢ IsCompact (f ⁻¹' K)

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Premises used: isCompact_iff_ultrafilter_le_nhds
-- 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
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : (↑𝒰 : Filter X) ≤ 𝓟 (f ⁻¹' K)
⊢ (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓟 K

Tactic:
rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] at h𝒰

Premises used: Ultrafilter.coe_map, Filter.map_le_iff_le_comap, Filter.comap_principal
-- 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
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓟 K
rcases : ∀ (y : Y) (hyK : y ∈ K) (hy : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 y), ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
rcases hK.ultrafilter_le_nhds _ h𝒰 with ⟨y, hyK, hy⟩

Premises used: IsCompact.ultrafilter_le_nhds
-- 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
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓟 K
y : Y
hyK : y ∈ K
hy : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 y
rcases :
  ∀ (x : X) (hx : (↑𝒰 : Filter X) ≤ 𝓝 x) (hyK : f x ∈ K) (hy : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 (f x)),
    ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩

Premises used: IsProperMap.ultrafilter_le_nhds_of_tendsto, rfl
-- 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
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓟 K
x : X
hx : (↑𝒰 : Filter X) ≤ 𝓝 x
hyK : f x ∈ K
hy : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 (f x)
⊢ ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
⟨x, hyK, hx⟩

Premises used: And.intro, Exists.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
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓟 K
x : X
hx : (↑𝒰 : Filter X) ≤ 𝓝 x
hyK : f x ∈ K
hy : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 (f x)
⊢ ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
exact ⟨x, hyK, hx⟩
-- 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
mp : IsProperMap f → Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
mpr : (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) → IsProperMap f
⊢ IsProperMap f ↔ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
constructor
-- 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
H : IsProperMap f
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_singleton⟩

Premises used: IsProperMap.isClosedMap, IsProperMap.isCompact_preimage, isCompact_singleton, And.intro, IsProperMap.continuous
-- 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
H : IsProperMap f
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
exact ⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
mpr : Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_clusterPt]

Premises used: isProperMap_iff_clusterPt
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ

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

Premises used: And.left, And.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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
mpr : ∀ (ℱ : Filter X) (y : Y) (hy : MapClusterPt y ℱ f), ∃ (x : X), f x = y ∧ ClusterPt x ℱ
⊢ Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
refine ⟨H.1, fun ℱ y hy ↦ ?_⟩
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : MapClusterPt y ℱ f
⊢ (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy

Premises used: And.right, And.left, IsClosedMap.mapClusterPt_iff_lift'_closure
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
mpr :
  ∀ (x : X) (hxy : x ∈ f ⁻¹' {y}) (hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))),
    ∃ (x : X), f x = y ∧ ClusterPt x ℱ
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y})) inf_le_right with ⟨x, hxy, hx⟩

Premises used: inf_le_right, And.right
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
⟨x, hxy, ?_⟩

Premises used: And.intro, Exists.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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))
mpr : ClusterPt x ℱ
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
refine ⟨x, hxy, ?_⟩
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))
mpr : ClusterPt x (ℱ.lift' closure[inst])
⊢ ClusterPt x ℱ

Tactic:
rw [← clusterPt_lift'_closure_iff]

Premises used: clusterPt_lift'_closure_iff
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (ℱ.lift' closure[inst])

Tactic:
hx.mono inf_le_left

Premises used: ClusterPt.mono, inf_le_left
-- 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
H : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (ℱ.lift' closure[inst])

Tactic:
exact hx.mono inf_le_left

Premises used: ClusterPt.mono, inf_le_left
-- 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
⊢ IsProperMap f ↔ IsClosedMap f

Tactic:
⟨fun h ↦ h.isClosedMap, fun h ↦ ?_⟩

Premises used: IsProperMap.isClosedMap, 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
refine : ∀ (h : IsClosedMap f), IsProperMap f
⊢ IsProperMap f ↔ IsClosedMap f

Tactic:
refine ⟨fun h ↦ h.isClosedMap, fun h ↦ ?_⟩
-- 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
h : IsClosedMap f
rw : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f

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
f : X → Y
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
h : IsClosedMap f
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
⟨f_cont, h, fun y ↦ (subsingleton_singleton.preimage f_inj).isCompact⟩

Premises used: Set.subsingleton_singleton, And.intro, Set.Subsingleton.preimage, Set.Subsingleton.isCompact
-- 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
h : IsClosedMap f
⊢ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
exact ⟨f_cont, h, fun y ↦ (subsingleton_singleton.preimage f_inj).isCompact⟩
-- 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
f_closed : IsClosedMap f
⊢ IsProperMap f

Tactic:
(isProperMap_iff_isClosedMap_of_inj f_cont f_inj).2 f_closed

Premises used: Iff.mpr, isProperMap_iff_isClosedMap_of_inj
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
⊢ IsProperMap.{u_1, u_2} (X := X) (Y := Y) (⇑e : (a : X) → Y)

Tactic:
isProperMap_of_isClosedMap_of_inj e.continuous e.injective e.isClosedMap

Premises used: Homeomorph.continuous, isProperMap_of_isClosedMap_of_inj, Homeomorph.injective, Homeomorph.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
hf : IsHomeomorph f
⊢ IsProperMap f

Tactic:
isProperMap_of_isClosedMap_of_inj hf.continuous hf.injective hf.isClosedMap

Premises used: IsHomeomorph.injective, isProperMap_of_isClosedMap_of_inj, IsHomeomorph.continuous, IsHomeomorph.isClosedMap
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsProperMap.{u_1, u_1} (X := X) id

Tactic:
IsHomeomorph.id.isProperMap

Premises used: IsHomeomorph.isProperMap, IsHomeomorph.id
-- 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 : IsClosedEmbedding f
⊢ IsProperMap f

Tactic:
isProperMap_of_isClosedMap_of_inj hf.continuous hf.injective hf.isClosedMap

Premises used: Topology.IsClosedEmbedding.isClosedMap, isProperMap_of_isClosedMap_of_inj, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsClosedEmbedding.continuous, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
hC : IsClosed[inst] C
⊢ IsProperMap.{u_1, u_1} (X := { x : X // x ∈ C }) (Subtype.val (p := fun (x : X) ↦ x ∈ C))

Tactic:
hC.isClosedEmbedding_subtypeVal.isProperMap

Premises used: Topology.IsClosedEmbedding.isProperMap, IsClosed.isClosedEmbedding_subtypeVal