awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
⊢ IsQuotientMap f

Tactic:
(ind.isOpenQuotientMap_of_surjective surj).isQuotientMap

Premises used: Topology.IsInducing.isOpenQuotientMap_of_surjective, IsOpenQuotientMap.isQuotientMap
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
a : ∀ (U : Set C), IsOpen[TopologicalSpace.coinduced p inst] U ↔ IsOpen[TopologicalSpace.induced g inst_2] U
⊢ TopologicalSpace.coinduced p inst = TopologicalSpace.induced g inst_2

Tactic:
ext U
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
a : IsOpen[inst] (p ⁻¹' U) ↔ ∃ (V : Set D), IsOpen[inst_2] V ∧ g ⁻¹' V = U
⊢ IsOpen[TopologicalSpace.coinduced p inst] U ↔ IsOpen[TopologicalSpace.induced g inst_2] U

Tactic:
change IsOpen (p ⁻¹' U) ↔ ∃ V, _

Premises used: Set.preimage, IsOpen
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
a :
  (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) ↔
    ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
⊢ IsOpen[inst] (p ⁻¹' U) ↔ ∃ (V : Set D), IsOpen[inst_2] V ∧ g ⁻¹' V = U

Tactic:
simp_rw [hf.isOpen_iff,
    (Set.image_surjective.mpr hq.surjective).exists,
    ← hq.isQuotientMap.isOpen_preimage]

Premises used: Iff.mpr, Topology.IsInducing.isOpen_iff, Function.Surjective.exists, IsOpenQuotientMap.surjective, Set.image_surjective, Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, IsOpenQuotientMap.isQuotientMap
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
a :
  (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) →
    ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U
a₁ :
  (∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U) →
    ∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U
⊢ (∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' U) ↔
    ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
⊢ ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩

Premises used: IsOpenQuotientMap.continuous, And.intro, Exists.intro, IsOpenQuotientMap.isOpenMap, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
a : g ⁻¹' q '' V = U
⊢ ∃ (x : Set B), IsOpen[inst_1] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U

Tactic:
refine ⟨V, hq.continuous.1 _ (hq.isOpenMap _ hV), ?_⟩
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
a : ∀ (x : C), x ∈ g ⁻¹' q '' V ↔ x ∈ U
⊢ g ⁻¹' q '' V = U

Tactic:
ext x
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x : C
a : ∀ (x : A), p x ∈ g ⁻¹' q '' V ↔ p x ∈ U
⊢ x ∈ g ⁻¹' q '' V ↔ x ∈ U

Tactic:
obtain ⟨x, rfl⟩ := hp x

Premises used: rfl
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x : A
a : p x ∈ g ⁻¹' q '' V → p x ∈ U
a₁ : p x ∈ U → p x ∈ g ⁻¹' q '' V
⊢ p x ∈ g ⁻¹' q '' V ↔ p x ∈ U

Tactic:
constructor
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x : A
y : B
hy : y ∈ V
e' : q y = g (p x)
a : ∀ (y : A) (hy : f y ∈ V) (e' : q (f y) = g (p x)), p x ∈ U
⊢ p x ∈ U

Tactic:
obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩

Premises used: And.intro, Exists.intro, congr_fun, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
a : p y ∈ U
⊢ p x ∈ U

Tactic:
rw [← hg ((congr_fun h y).trans e')]

Premises used: congr_fun, Eq.trans
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p y ∈ U

Tactic:
e.le hy

Premises used: Set.Mem, setOf, Eq.le, Set.preimage
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p y ∈ U

Tactic:
exact e.le hy

Premises used: Eq.le
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H_1 : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x : A
H : p x ∈ U
⊢ p x ∈ g ⁻¹' q '' V

Tactic:
⟨f x, e.ge H, congr_fun h.symm x⟩

Premises used: Eq.ge, Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image, congr_fun, Eq.symm
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H_1 : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst_1] V
e : f ⁻¹' V = p ⁻¹' U
x : A
H : p x ∈ U
⊢ p x ∈ g ⁻¹' q '' V

Tactic:
exact ⟨f x, e.ge H, congr_fun h.symm x⟩
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
V : Set B
hV : IsOpen[inst_1] (q ⁻¹' q '' V)
⊢ ∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' g ⁻¹' q '' V

Tactic:
⟨_, hV, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
V : Set B
hV : IsOpen[inst_1] (q ⁻¹' q '' V)
a : f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V
⊢ ∃ (t : Set B), IsOpen[inst_1] t ∧ f ⁻¹' t = p ⁻¹' g ⁻¹' q '' V

Tactic:
refine ⟨_, hV, ?_⟩
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
V : Set B
hV : IsOpen[inst_1] (q ⁻¹' q '' V)
a : q ∘ f ⁻¹' q '' V = g ∘ p ⁻¹' q '' V
⊢ f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V

Tactic:
simp_rw [← Set.preimage_comp, h]

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace C
inst_3 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : IsQuotientMap p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
⊢ IsEmbedding g

Tactic:
⟨⟨hp.eq_coinduced.trans (coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing
    f g p q h hf hp.surjective hq hg H)⟩, hg⟩

Premises used: Topology.IsQuotientMap.surjective, Topology.IsCoinducing.eq_coinduced, coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing, Topology.IsInducing.mk, Topology.IsQuotientMap.isCoinducing, Eq.trans, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Maps.OpenQuotient
Goal:
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst : TopologicalSpace A
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace C
inst_3 : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : IsEmbedding g
H : q ⁻¹' q '' range f ⊆ range f
⊢ IsQuotientMap p

Tactic:
⟨⟨hg.eq_induced.trans ((coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing
    f g p q h hf hp hq hg.injective H)).symm⟩, hp⟩

Premises used: Topology.IsCoinducing.mk, coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing, Topology.IsEmbedding.injective, Topology.IsQuotientMap.mk, Topology.IsEmbedding.toIsInducing, Eq.symm, Topology.IsInducing.eq_induced, Eq.trans
-- 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

Tactic:
h.toContinuous

Premises used: IsProperMap.toContinuous
-- 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
rw : ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ (x : X), f x = y ∧ ClusterPt x (𝓟 s)
⊢ IsClosedMap f

Tactic:
rw [isClosedMap_iff_clusterPt]

Premises used: isClosedMap_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 : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ (x : X), f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
fun s y ↦ h.clusterPt_of_mapClusterPt (ℱ := 𝓟 s) (y := y)

Premises used: IsProperMap.clusterPt_of_mapClusterPt
-- 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
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ (x : X), f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
exact fun s y ↦ h.clusterPt_of_mapClusterPt (ℱ := 𝓟 s) (y := y)

Premises used: IsProperMap.clusterPt_of_mapClusterPt
-- 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
rw :
  (Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ) ↔
    Continuous[inst, inst_1] f ∧
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ IsProperMap f ↔
    Continuous[inst, inst_1] f ∧
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x

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
⊢ (Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ) ↔
    Continuous[inst, inst_1] f ∧
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
and_congr_right (fun _ ↦ ?_)

Premises used: and_congr_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
refine :
  Continuous[inst, inst_1] f →
    ((∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ) ↔
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x)
⊢ (Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ) ↔
    Continuous[inst, inst_1] f ∧
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
refine and_congr_right (fun _ ↦ ?_)

Premises used: and_congr_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
mp :
  (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ) →
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
mpr :
  (∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x) →
    ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ) ↔
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 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
f : X → Y
h : Continuous[inst, inst_1] f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
mp : ∀ (hY : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 y), ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
(hY : (Ultrafilter.map f 𝒰 : Filter Y) ≤ _)
-- 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
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 y
mp : ∀ (hY : ClusterPt y (↑(Ultrafilter.map f 𝒰) : Filter Y)), ∃ (x : X), f x = y ∧ ClusterPt x (↑𝒰 : Filter X)
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
simp_rw [← Ultrafilter.clusterPt_iff] at hY ⊢

Premises used: Ultrafilter.clusterPt_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
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ClusterPt y (↑(Ultrafilter.map f 𝒰) : Filter Y)
⊢ ∃ (x : X), f x = y ∧ ClusterPt x (↑𝒰 : Filter X)

Tactic:
H 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
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ClusterPt y (↑(Ultrafilter.map f 𝒰) : Filter Y)
⊢ ∃ (x : X), f x = y ∧ ClusterPt x (↑𝒰 : Filter X)

Tactic:
exact H 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
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
mpr :
  ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄ (x : Ultrafilter X) (h : (↑x : Filter X) ≤ comap f (𝓝 y) ⊓ ℱ),
    ∃ (x : X), f x = y ∧ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x ⊓ ℱ
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ

Tactic:
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, ← exists_ultrafilter_iff,
      forall_exists_index]

Premises used: Filter.push_pull', forall_exists_index, Filter.exists_ultrafilter_iff, ClusterPt, MapClusterPt, Filter.map_neBot_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
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : (↑𝒰 : Filter X) ≤ comap f (𝓝 y) ⊓ ℱ
mpr :
  ∀ (x : X) (hxy : f x = y) (hx : (↑𝒰 : Filter X) ≤ 𝓝 x),
    ∃ (x : X), f x = y ∧ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x ⊓ ℱ
⊢ ∃ (x : X), f x = y ∧ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x ⊓ ℱ

Tactic:
rcases H (tendsto_iff_comap.mpr <| hy.trans inf_le_left) with ⟨x, hxy, hx⟩

Premises used: Iff.mpr, Filter.tendsto_iff_comap, inf_le_left, LE.le.trans
-- 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
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : (↑𝒰 : Filter X) ≤ comap f (𝓝 y) ⊓ ℱ
x : X
hxy : f x = y
hx : (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), f x = y ∧ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x ⊓ ℱ

Tactic:
⟨x, hxy, 𝒰, le_inf hx (hy.trans inf_le_right)⟩

Premises used: inf_le_right, le_inf, And.intro, Exists.intro, LE.le.trans
-- 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
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
ℱ : Filter X
y : Y
𝒰 : Ultrafilter X
hy : (↑𝒰 : Filter X) ≤ comap f (𝓝 y) ⊓ ℱ
x : X
hxy : f x = y
hx : (↑𝒰 : Filter X) ≤ 𝓝 x
⊢ ∃ (x : X), f x = y ∧ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x ⊓ ℱ

Tactic:
exact ⟨x, hxy, 𝒰, le_inf hx (hy.trans inf_le_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
inst_2 : T2Space Y
⊢ IsProperMap f ↔
    Continuous[inst, inst_1] f ∧
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
isProperMap_iff_ultrafilter.trans <| and_congr_right fun hc ↦ forall₃_congr fun _𝒰 _y hy ↦
    exists_congr fun x ↦ and_iff_right_of_imp fun h ↦
      tendsto_nhds_unique ((hc.tendsto x).mono_left h) hy

Premises used: isProperMap_iff_ultrafilter, forall₃_congr, and_congr_right, Continuous.tendsto, exists_congr, Iff.trans, Filter.Tendsto.mono_left, and_iff_right_of_imp, tendsto_nhds_unique
-- 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
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (𝓝 y)
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x

Tactic:
(isProperMap_iff_ultrafilter.mp h).2 hy

Premises used: isProperMap_iff_ultrafilter, And.right, Iff.mp
-- 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
⊢ Continuous[inst, inst_2] (g ∘ f)

Tactic:
fun_prop
-- 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
refine : ∀ (ℱ : Filter X) (z : Z) (h : MapClusterPt z ℱ (g ∘ f)), ∃ (x : X), (g ∘ f) x = z ∧ ClusterPt x ℱ
⊢ IsProperMap (g ∘ f)

Tactic:
refine ⟨by fun_prop, 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
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z ℱ (g ∘ f)
⊢ MapClusterPt z (map f ℱ) g

Tactic:
rw [mapClusterPt_comp] at h

Premises used: 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
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z (map f ℱ) g
rcases :
  ∀ (y : Y) (hy : ClusterPt y (map f ℱ)) (h : MapClusterPt (g y) (map f ℱ) g),
    ∃ (x : X), (g ∘ f) x = g y ∧ ClusterPt x ℱ
⊢ ∃ (x : X), (g ∘ f) x = z ∧ ClusterPt x ℱ

Tactic:
rcases hg.clusterPt_of_mapClusterPt h with ⟨y, rfl, hy⟩

Premises used: IsProperMap.clusterPt_of_mapClusterPt, rfl