awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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
⊢ x ∈ g ⁻¹' q '' V ↔ x ∈ U
have a : ∀ (x : A), p x ∈ g ⁻¹' q '' V ↔ p x ∈ U
Tactic: obtain ⟨x, rfl⟩ := hp x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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
⊢ p x ∈ g ⁻¹' q '' V ↔ p x ∈ U
have a : p x ∈ g ⁻¹' q '' V → p x ∈ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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
⊢ p x ∈ g ⁻¹' q '' V ↔ p x ∈ U
have a₁ : p x ∈ U → p x ∈ g ⁻¹' q '' V
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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)
⊢ p x ∈ U
have a : ∀ (y : A) (hy : f y ∈ V) (e' : q (f y) = g (p x)), p x ∈ U
Tactic: obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩
Cleared hypotheses: y, hy, e'
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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 x ∈ U
have a : p y ∈ U
Tactic: rw [← hg ((congr_fun h y).trans e')]
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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
have a : f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V
Tactic: refine ⟨_, hV, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.OpenQuotient (goal)
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)
⊢ f ⁻¹' q ⁻¹' q '' V = p ⁻¹' g ⁻¹' q '' V
have a : q ∘ f ⁻¹' q '' V = g ∘ p ⁻¹' q '' V
Tactic: simp_rw [← Set.preimage_comp, h]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ IsClosedMap f
have rw : ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ (x : X), f x = y ∧ ClusterPt x (𝓟 s)
Tactic: rw [isClosedMap_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔
    Continuous[inst, inst_1] f ∧
      ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
have 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
Tactic: rw [isProperMap_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
have 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)
Tactic: refine and_congr_right (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ (∀ ⦃ℱ : 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ (∀ ⦃ℱ : 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
have 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 ℱ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
have mp : ∀ (hY : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 y), ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
Tactic: (hY : (Ultrafilter.map f 𝒰 : Filter Y) ≤ _)
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ 𝓝 x
have mp : ∀ (hY : ClusterPt y (↑(Ultrafilter.map f 𝒰) : Filter Y)), ∃ (x : X), f x = y ∧ ClusterPt x (↑𝒰 : Filter X)
Tactic: simp_rw [← Ultrafilter.clusterPt_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt x ℱ
have 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 ⊓ ℱ
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, ← exists_ultrafilter_iff,
      forall_exists_index]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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), f x = y ∧ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x ⊓ ℱ
have mpr : ∀ (x : X) (hxy : f x = y) (hx : (↑𝒰 : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ IsProperMap (g ∘ f)
have refine : ∀ (ℱ : Filter X) (z : Z) (h : MapClusterPt z ℱ (g ∘ f)), ∃ (x : X), (g ∘ f) x = z ∧ ClusterPt x ℱ
Tactic: refine ⟨by fun_prop, fun ℱ z h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (hypothesis)
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)
⊢ ∃ (x : X), (g ∘ f) x = z ∧ ClusterPt x ℱ
have h₁ : MapClusterPt z (map f ℱ) g
Tactic: rw [mapClusterPt_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ ∃ (x : X), (g ∘ f) x = z ∧ ClusterPt x ℱ
have rcases : ∀ (y : Y) (hy : ClusterPt y (map f ℱ)) (h : MapClusterPt (g y) (map f ℱ) g), ∃ (x : X), (g ∘ f) x = g y ∧ ClusterPt x ℱ
Tactic: rcases hg.clusterPt_of_mapClusterPt h with ⟨y, rfl, hy⟩
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ ∃ (x : X), (g ∘ f) x = g y ∧ ClusterPt x ℱ
have 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 ℱ
Tactic: rcases hf.clusterPt_of_mapClusterPt hy with ⟨x, rfl, hx⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ ∃ (x_1 : X), (g ∘ f) x_1 = g (f x) ∧ ClusterPt x_1 ℱ
have left : (g ∘ f) x = g (f x)
Tactic: use x, rfl
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
have refine : ∀ (ℱ : Filter Y) (z : Z) (h : MapClusterPt z ℱ g), ∃ (x : Y), g x = z ∧ ClusterPt x ℱ
Tactic: refine ⟨hg, fun ℱ z h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (hypothesis)
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
⊢ ∃ (x : Y), g x = z ∧ ClusterPt x ℱ
have h₁ : MapClusterPt z (comap f ℱ) (g ∘ f)
Tactic: rw [← ℱ.map_comap_of_surjective f_surj, ← mapClusterPt_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ ∃ (x : Y), g x = z ∧ ClusterPt x ℱ
have 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 ℱ
Tactic: rcases hgf.clusterPt_of_mapClusterPt h with ⟨x, rfl, hx⟩
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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 ℱ
have rw : ∃ (x_1 : Y), g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))
Tactic: rw [← ℱ.map_comap_of_surjective f_surj]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
have refine : ∀ (ℱ : Filter X) (y : Y) (h : MapClusterPt y ℱ f), ∃ (x : X), f x = y ∧ ClusterPt x ℱ
Tactic: refine ⟨hf, fun ℱ y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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), f x = y ∧ ClusterPt x ℱ
have rcases : ∀ (x : X) (hx1 : (g ∘ f) x = g y) (hx2 : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ IsProperMap f
have rw : Continuous[inst, inst_1] f ∧
  ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (𝓝 y) → ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
Tactic: rw [isProperMap_iff_ultrafilter_of_t2]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
have refine : ∀ (𝒰 : Ultrafilter X) (y : Y) (h : Tendsto f (↑𝒰 : Filter X) (𝓝 y)), ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
Tactic: refine ⟨hf, fun 𝒰 y h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
have 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
Tactic: rw [isProperMap_iff_ultrafilter] at hgf
Cleared hypotheses: hgf, 𝒰, y, h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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), (↑𝒰 : Filter X) ≤ 𝓝 x
have rcases : ∀ (x : X) (hx : (↑𝒰 : Filter X) ≤ 𝓝 x), ∃ (x : X), (↑𝒰 : Filter X) ≤ 𝓝 x
Tactic: rcases hgf.2 ((hg.tendsto y).comp h) with ⟨x, -, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
⊢ IsProperMap (Prod.map f g)
have 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
Tactic: simp_rw [isProperMap_iff_ultrafilter] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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) ∧
    ∀ ⦃𝒰 : 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
have left : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map f g)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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⦄,
    Tendsto (Prod.map f g) (↑𝒰 : Filter (X × Z)) (𝓝 y) → ∃ (x : X × Z), Prod.map f g x = y ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
have 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
Tactic: ⟨y, w⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (hypothesis)
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))
⊢ ∃ (x : X × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
have 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)
Tactic: simp_rw [nhds_prod_eq, tendsto_prod_iff'] at hyw
Cleared hypotheses: hyw
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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 × Z), Prod.map f g x = (y, w) ∧ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 x
have 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
Tactic: rcases hf.2 (show Tendsto f (Ultrafilter.map fst 𝒰) (𝓝 y) by simpa using hyw.1) with
      ⟨x, hxy, hx⟩