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
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
y : Y
hy : ClusterPt y (map f ℱ)
h : MapClusterPt (g y) (map f ℱ) g
rcases :
  ∀ (x : X) (hx : ClusterPt x ℱ) (hy : ClusterPt (f x) (map f ℱ)) (h : MapClusterPt (g (f x)) (map f ℱ) g),
    ∃ (x_1 : X), (g ∘ f) x_1 = g (f x) ∧ ClusterPt x_1 ℱ
⊢ ∃ (x : X), (g ∘ f) x = g y ∧ ClusterPt x ℱ

Tactic:
rcases hf.clusterPt_of_mapClusterPt hy with ⟨x, rfl, hx⟩

Premises used: IsProperMap.clusterPt_of_mapClusterPt, rfl
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
x : X
hx : ClusterPt x ℱ
hy : ClusterPt (f x) (map f ℱ)
h : MapClusterPt (g (f x)) (map f ℱ) g
w : X
left : (g ∘ f) x = g (f x)
right : ClusterPt x ℱ
⊢ ∃ (x_1 : X), (g ∘ f) x_1 = g (f x) ∧ ClusterPt x_1 ℱ

Tactic:
use x, rfl

Premises used: rfl
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
⊢ IsProperMap g

Tactic:
⟨hg, fun ℱ z h ↦ ?_⟩

Premises used: IsProperMap.mk
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
refine : ∀ (ℱ : Filter Y) (z : Z) (h : MapClusterPt z ℱ g), ∃ (x : Y), g x = z ∧ ClusterPt x ℱ
⊢ IsProperMap g

Tactic:
refine ⟨hg, fun ℱ z h ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z ℱ g
⊢ MapClusterPt z (comap f ℱ) (g ∘ f)

Tactic:
rw [← ℱ.map_comap_of_surjective f_surj, ← mapClusterPt_comp] at h

Premises used: Filter.map_comap_of_surjective, mapClusterPt_comp
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z (comap f ℱ) (g ∘ f)
rcases :
  ∀ (x : X) (hx : ClusterPt x (comap f ℱ)) (h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)),
    ∃ (x_1 : Y), g x_1 = (g ∘ f) x ∧ ClusterPt x_1 ℱ
⊢ ∃ (x : Y), g x = z ∧ ClusterPt x ℱ

Tactic:
rcases hgf.clusterPt_of_mapClusterPt h with ⟨x, rfl, hx⟩

Premises used: IsProperMap.clusterPt_of_mapClusterPt, rfl
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
rw : ∃ (x_1 : Y), g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))
⊢ ∃ (x_1 : Y), g x_1 = (g ∘ f) x ∧ ClusterPt x_1 ℱ

Tactic:
rw [← ℱ.map_comap_of_surjective f_surj]

Premises used: Filter.map_comap_of_surjective
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ (x_1 : Y), g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))

Tactic:
⟨f x, rfl, hx.map hf.continuousAt tendsto_map⟩

Premises used: Continuous.continuousAt, Filter.tendsto_map, ClusterPt.map, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ (x_1 : Y), g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))

Tactic:
exact ⟨f x, rfl, hx.map hf.continuousAt tendsto_map⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
⊢ IsProperMap f

Tactic:
⟨hf, fun ℱ y h ↦ ?_⟩

Premises used: IsProperMap.mk
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
refine : ∀ (ℱ : Filter X) (y : Y) (h : MapClusterPt y ℱ f), ∃ (x : X), f x = y ∧ ClusterPt x ℱ
⊢ IsProperMap f

Tactic:
refine ⟨hf, fun ℱ y h ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
rcases : ∀ (x : X) (hx1 : (g ∘ f) x = g y) (hx2 : ClusterPt x ℱ), ∃ (x : X), f x = y ∧ ClusterPt x ℱ
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
rcases hgf.clusterPt_of_mapClusterPt (h.map hg.continuousAt tendsto_map) with ⟨x, hx1, hx2⟩

Premises used: Continuous.continuousAt, Filter.tendsto_map, IsProperMap.clusterPt_of_mapClusterPt, ClusterPt.map
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
x : X
hx1 : (g ∘ f) x = g y
hx2 : ClusterPt x ℱ
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
⟨x, g_inj hx1, hx2⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
x : X
hx1 : (g ∘ f) x = g y
hx2 : ClusterPt x ℱ
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
exact ⟨x, g_inj hx1, hx2⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
rw :
  Continuous[inst, inst_1] f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter_of_t2]

Premises used: isProperMap_iff_ultrafilter_of_t2
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
⊢ Continuous[inst, inst_1] f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
⟨hf, fun 𝒰 y h ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
refine : ∀ (𝒰 : Ultrafilter X) (y : Y) (h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)), ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ Continuous[inst, inst_1] f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
refine ⟨hf, fun 𝒰 y h ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf : IsProperMap (g ∘ f)
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)
rw :
  ∀
    (hgf :
      Continuous[inst, inst_2] (g ∘ f) ∧
        ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄,
          Tendsto (g ∘ f) (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (g ∘ f) x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x)
    (𝒰 : Ultrafilter X) (y : Y) (h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)), ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
rw [isProperMap_iff_ultrafilter] at hgf

Premises used: isProperMap_iff_ultrafilter
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf :
  Continuous[inst, inst_2] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄,
      Tendsto (g ∘ f) (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (g ∘ f) x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)
rcases : ∀ (x : X) (hx : (↑𝒰 : Filter X) ≤ 𝓝 x), ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
rcases hgf.2 ((hg.tendsto y).comp h) with ⟨x, -, hx⟩

Premises used: Continuous.tendsto, And.right, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf :
  Continuous[inst, inst_2] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄,
      Tendsto (g ∘ f) (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (g ∘ f) x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)
x : X
hx : (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
⟨x, hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Maps.Proper.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
inst_3 : T2Space Y
hf : Continuous[inst, inst_1] f
hg : Continuous[inst_1, inst_2] g
hgf :
  Continuous[inst, inst_2] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄,
      Tendsto (g ∘ f) (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (g ∘ f) x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)
x : X
hx : (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
exact ⟨x, hx⟩
-- 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 : IsProperMap f
hg : IsProperMap g
simp_rw :
  ∀
    (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),
    Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g) ∧
      ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄,
        Tendsto (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 y) →
          ∃ (x : X × Z), Prod.map f g x = y ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
⊢ IsProperMap (Prod.map f g)

Tactic:
simp_rw [isProperMap_iff_ultrafilter] at hf hg ⊢

Premises used: isProperMap_iff_ultrafilter
-- 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
left : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g)
right :
  ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄,
    Tendsto (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 y) → ∃ (x : X × Z), Prod.map f g x = y ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g) ∧
    ∀ ⦃𝒰 : Ultrafilter (X × Z)⦄ ⦃y : Y × W⦄,
      Tendsto (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 y) →
        ∃ (x : X × Z), Prod.map f g x = y ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x

Tactic:
constructor
-- 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
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g)

Tactic:
hf.1.prodMap hg.1

Premises used: Continuous.prodMap, And.left
-- 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
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g)

Tactic:
exact hf.1.prodMap hg.1

Premises used: Continuous.prodMap, And.left
-- 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)
right :
  ∀ (y : Y) (w : W),
    Tendsto (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 (y, w)) →
      ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
⊢ ∀ ⦃y : Y × W⦄,
    Tendsto (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 y) → ∃ (x : X × Z), Prod.map f g x = y ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x

Tactic:
⟨y, w⟩
-- 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 (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 (y, w))
⊢ 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)

Tactic:
simp_rw [nhds_prod_eq, tendsto_prod_iff'] at hyw

Premises used: Filter.tendsto_prod_iff', nhds_prod_eq
-- 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)
⊢ Tendsto f (↑(Ultrafilter.map fst 𝒰) : Filter X) (𝓝 y)

Tactic:
simpa using hyw.1

Premises used: And.left
-- 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)
right :
  ∀ (x : X) (hxy : f x = y) (hx : (↑(Ultrafilter.map fst 𝒰) : Filter X) ≤ 𝓝 x),
    ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
⊢ ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x

Tactic:
rcases hf.2 (show Tendsto f (Ultrafilter.map fst 𝒰) (𝓝 y) by simpa using hyw.1) with
      ⟨x, hxy, hx⟩

Premises used: And.right
-- 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
⊢ Tendsto g (↑(Ultrafilter.map snd 𝒰) : Filter Z) (𝓝 w)

Tactic:
simpa using hyw.2

Premises used: And.right
-- 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
right :
  ∀ (z : Z) (hzw : g z = w) (hz : (↑(Ultrafilter.map snd 𝒰) : Filter Z) ≤ 𝓝 z),
    ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
⊢ ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x

Tactic:
rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using hyw.2) with
      ⟨z, hzw, hz⟩

Premises used: And.right
-- 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
⊢ ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x

Tactic:
⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩

Premises used: Prod.mk, Prod.ext, And.intro, Exists.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
right : (↑𝒰 : Filter (X × Z)) ≤ 𝓝 (x, z)
⊢ ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x

Tactic:
refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩
-- 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
right : Tendsto fst (↑𝒰 : Filter (X × Z)) (𝓝 x) ∧ Tendsto snd (↑𝒰 : Filter (X × Z)) (𝓝 z)
⊢ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 (x, z)

Tactic:
rw [nhds_prod_eq, le_prod]

Premises used: Filter.le_prod, nhds_prod_eq