awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
have 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
Tactic: rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using hyw.2) with
      ⟨z, hzw, hz⟩
-- 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
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
have right : (↑𝒰 : Filter (X × Z)) ≤ 𝓝 (x, z)
Tactic: refine ⟨⟨x, z⟩, Prod.ext hxy hzw, ?_⟩
-- 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
hxy : f x = y
hx : (↑(Ultrafilter.map fst 𝒰) : Filter X) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : (↑(Ultrafilter.map snd 𝒰) : Filter Z) ≤ 𝓝 z
⊢ (↑𝒰 : Filter (X × Z)) ≤ 𝓝 (x, z)
have right : Tendsto fst (↑𝒰 : Filter (X × Z)) (𝓝 x) ∧ Tendsto snd (↑𝒰 : Filter (X × Z)) (𝓝 z)
Tactic: rw [nhds_prod_eq, le_prod]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ IsProperMap (Y := (i : ι) → Y i) fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)
have 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
Tactic: simp_rw [isProperMap_iff_ultrafilter] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)) ∧
    ∀ ⦃𝒰 : 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
have left : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (hypothesis)
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)
⊢ ∃ (x : (i : ι) → X i), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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), (fun (i : ι) ↦ f i (x i)) = y ∧ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
have 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
Tactic: choose x hxy hx using fun i ↦ (h i).2 (this i)
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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
have right : (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
Tactic: refine ⟨x, funext hxy, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
have right : (↑𝒰 : Filter ((i : ι) → X i)) ≤ Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (x i)
Tactic: rwa [nhds_pi, le_pi]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (goal)
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)
⊢ (↑𝒰 : Filter ((i : ι) → X i)) ≤ 𝓝 x
have right₁ : ∀ (i : ι), Tendsto (eval (β := X) i) (↑𝒰 : Filter ((i : ι) → X i)) (𝓝 (x i))
Tactic: rwa [nhds_pi, le_pi]
-- 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
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
have rw : ∀ (f_1 : Ultrafilter X), (↑f_1 : Filter X) ≤ 𝓟 (f ⁻¹' K) → ∃ x ∈ f ⁻¹' K, (↑f_1 : Filter X) ≤ 𝓝 x
Tactic: rw [isCompact_iff_ultrafilter_le_nhds]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (hypothesis)
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)
⊢ ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x
have h𝒰₁ : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓟 K
Tactic: rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] 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
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 ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x
have rcases : ∀ (y : Y) (hyK : y ∈ K) (hy : (↑(Ultrafilter.map f 𝒰) : Filter Y) ≤ 𝓝 y), ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x
Tactic: rcases hK.ultrafilter_le_nhds _ h𝒰 with ⟨y, hyK, 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 : 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
⊢ ∃ x ∈ f ⁻¹' K, (↑𝒰 : Filter X) ≤ 𝓝 x
have 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
Tactic: rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩
Cleared hypotheses: y, hyK, 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
⊢ IsProperMap f ↔ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
have mp : IsProperMap f → Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
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
mp : IsProperMap f → Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f ↔ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
have mpr : (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) → IsProperMap f
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 ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f
have mpr : Continuous[inst, inst_1] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ (x : X), f x = y ∧ ClusterPt 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
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 ℱ
have mpr : ∀ (ℱ : Filter X) (y : Y) (hy : MapClusterPt y ℱ f), ∃ (x : X), f x = y ∧ ClusterPt x ℱ
Tactic: refine ⟨H.1, fun ℱ y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.Basic (hypothesis)
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
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ
have hy₁ : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
Tactic: rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] 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 ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ ∃ (x : X), f x = y ∧ ClusterPt x ℱ
have mpr : ∀ (x : X) (hxy : x ∈ f ⁻¹' {y}) (hx : ClusterPt x (ℱ.lift' closure[inst] ⊓ 𝓟 (f ⁻¹' {y}))),
  ∃ (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⟩
-- 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 ∧ 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 ℱ
have mpr : ClusterPt x ℱ
Tactic: refine ⟨x, hxy, ?_⟩
-- 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 ∧ 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 ℱ
have mpr : ClusterPt x (ℱ.lift' closure[inst])
Tactic: rw [← clusterPt_lift'_closure_iff]
-- 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
⊢ IsProperMap f ↔ IsClosedMap f
have refine : ∀ (h : IsClosedMap f), IsProperMap f
Tactic: refine ⟨fun h ↦ h.isClosedMap, fun 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
f_cont : Continuous[inst, inst_1] f
f_inj : Injective f
h : IsClosedMap f
⊢ IsProperMap f
have rw : Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
Tactic: rw [isProperMap_iff_isClosedMap_and_compact_fibers]
-- 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
inst_2 : T1Space Y
⊢ IsProperMap f ↔ Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite
have simp_rw : (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
  Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
Tactic: simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto,
    le_cofinite_iff_compl_singleton_mem, mem_map, preimage_compl]
-- 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
inst_2 : T1Space Y
⊢ (Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst, inst_1] f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
have refine : ∀ (f_cont : Continuous[inst, inst_1] f),
  IsClosedMap f → ∀ (H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X) (y : Y), IsCompact (f ⁻¹' {y})
Tactic: refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
    ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H 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
inst_2 : T1Space Y
f_cont : Continuous[inst, inst_1] f
h : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})
have rcases : ∀ (K : Set X) (hK : IsCompact K) (hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ), IsCompact (f ⁻¹' {y})
Tactic: rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩
-- 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
inst_2 : T1Space Y
y : Y
⊢ (IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ↔ CompactSpace X
have rw : ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
  CompactSpace X
Tactic: rw [isProperMap_iff_isClosedMap_and_compact_fibers]
-- 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
inst_2 : T1Space Y
y : Y
⊢ ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
    CompactSpace X
have mp : ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) →
  CompactSpace X
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
inst_2 : T1Space Y
y : Y
mp :
  ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) →
    CompactSpace X
⊢ ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
    CompactSpace X
have mpr : CompactSpace X →
  (Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})
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
inst_2 : T1Space Y
y : Y
H : CompactSpace X
⊢ (Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})
have mpr : ∀ (y' : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y'})
Tactic: refine ⟨continuous_const, isClosedMap_const, fun 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
inst_2 : T1Space Y
y : Y
⊢ (IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ↔ CompactSpace X
have rw : ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
  CompactSpace X
Tactic: classical
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  constructor
  · rintro ⟨-, -, h⟩
    exact ⟨by simpa using h y⟩
  · intro H
    refine ⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩
    simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]
-- 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
inst_2 : T1Space Y
y : Y
rw rw₁ rw₂ :
  ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
      (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
        ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) ↔
    CompactSpace X
⊢ (IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ↔ CompactSpace X
have mp : ((Continuous[inst, inst_1] fun (x : X) ↦ y) ∧
    (IsClosedMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ∧
      ∀ (y_1 : Y), IsCompact.{u_1} (X := X) (preimage (β := Y) (fun (x : X) ↦ y) {y_1})) →
  CompactSpace X
Tactic: classical
  rw [isProperMap_iff_isClosedMap_and_compact_fibers]
  constructor
  · rintro ⟨-, -, h⟩
    exact ⟨by simpa using h y⟩
  · intro H
    refine ⟨continuous_const, isClosedMap_const, fun y' ↦ ?_⟩
    simp [preimage_const, mem_singleton_iff, apply_ite, isCompact_univ]