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
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
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
⊢ (IsProperMap.{u_1, u_2} (Y := Y) fun (x : X) ↦ y) ↔ 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: 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.CompactlyGenerated (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
h_1 : Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
hf : Continuous f
h : ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)
s : Set X
hs : IsClosed s
K : Set Y
hK : IsCompact K
⊢ IsClosed (X := (↑K : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' s)
have h₁ : (↑K : Type u_2) = { x : Y // x ∈ K } →
  Eq (α := Set (↑K : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' s)
    (Subtype.val (p := fun (x : Y) ↦ x ∈ K) ⁻¹' f '' (s ∩ f ⁻¹' K))
Tactic: convert! (((h hK).inter_left hs).image hf).isClosed.preimage continuous_subtype_val using 1
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.CompactlyGenerated (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)
have simp_rw : (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
  Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
Tactic: simp_rw [isProperMap_iff_isCompact_preimage,
    hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.CompactlyGenerated (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
have refine : ∀ (f_cont : Continuous f) (H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X) (K : Set Y) (hK : IsCompact K),
  IsCompact (f ⁻¹' K)
Tactic: refine and_congr_right fun f_cont ↦
    ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.CompactlyGenerated (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactlyCoherentSpace Y
f : X → Y
f_cont : Continuous f
H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)
have rcases : ∀ (K' : Set X) (hK' : IsCompact K') (hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ), IsCompact (f ⁻¹' K)
Tactic: rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
have mp : IsProperMap f → Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
mp : IsProperMap f → Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
have mpr : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id) → IsProperMap f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
⊢ IsProperMap f
have mpr : Continuous f ∧
  ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
Tactic: rw [isProperMap_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
⊢ Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have mpr : ∀ (𝒰 : Ultrafilter X) (y : Y) (hy : Tendsto f (↑𝒰 : Filter X) (nhds y)), ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
Tactic: refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have this : IsClosed (Prod.map f id '' F)
Tactic: have := H.2 F isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have this₁ : (y, (↑𝒰 : Filter X)) ∈ Prod.map f id '' F
Tactic: have : (y, ↑𝒰) ∈ Prod.map f id '' F :=
  -- Note that, by the properties of the topology on `Filter X`, the function `pure : X → Filter X`
  -- tends to the point `𝒰` of `Filter X` along the filter `𝒰` on `X`. Since `f` tends to `y` along
  -- `𝒰`, we get that the function `(f, pure) : X → (Y, Filter X)` tends to `(y, 𝒰)` along
  -- `𝒰`. Furthermore, each `(f, pure)(x) = (f × id)(x, pure x)` is clearly an element of
  -- the closed set `(f × id) '' F`, thus the limit `(y, 𝒰)` also belongs to that set.
      this.mem_of_tendsto (hy.prodMk_nhds (Filter.tendsto_pure_self (𝒰 : Filter X)))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this_1 : IsClosed (Prod.map f id '' F)
this : (y, (↑𝒰 : Filter X)) ∈ Prod.map f id '' F
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have mpr : ∀ (x : X) (hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))) (hx : (x, 𝒰.1) ∈ F),
  ∃ (x_1 : X), f x_1 = f x ∧ (↑𝒰 : Filter X) ≤ nhds x_1
Tactic: rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
Cleared hypotheses: y, hy, this
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx : (x, 𝒰.1) ∈ F
⊢ ∃ (x_1 : X), f x_1 = f x ∧ (↑𝒰 : Filter X) ≤ nhds x_1
have mpr : ∀ (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ 𝒰), False
Tactic: refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx : (x, 𝒰.1) ∈ F
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
⊢ False
have mpr : ∀
  (hx :
    ∀ (t : Set (X × Filter X)),
      Membership.mem (γ := Filter (X × Filter X)) (nhds (x, 𝒰.1)) t →
        (t ∩ {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}).Nonempty)
  (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ 𝒰), False
Tactic: rw [mem_closure_iff_nhds] at hx
Cleared hypotheses: hx, U, hU, hUc
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Filter X) (Prod.map f id)
𝒰 : Ultrafilter X
F : Set (X × Filter X) := closure {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
hy : Tendsto f (↑𝒰 : Filter X) (nhds (f x))
hx :
  ∀ (t : Set (X × Filter X)),
    Membership.mem (γ := Filter (X × Filter X)) (nhds (x, 𝒰.1)) t →
      (t ∩ {xℱ : X × Filter X | xℱ.2 = pure xℱ.1}).Nonempty
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ 𝒰
⊢ False
have mpr : ∀ (z : X) (hz : z ∈ U) (hz' : Membership.mem (γ := Filter X) (pure z) Uᶜ), False
Tactic: rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU (isOpen_setOf_mem.mem_nhds hUc)) with
      ⟨⟨z, 𝒢⟩, ⟨⟨hz : z ∈ U, hz' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure z⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
have mp : IsProperMap f → Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
mp : IsProperMap f → Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
have mpr : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id) → IsProperMap f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
⊢ IsProperMap f
have mpr : Continuous f ∧
  ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
Tactic: rw [isProperMap_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
⊢ Continuous f ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰 : Filter X) (nhds y) → ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have mpr : ∀ (𝒰 : Ultrafilter X) (y : Y) (hy : Tendsto f (↑𝒰 : Filter X) (nhds y)), ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
Tactic: refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have this : IsClosed (Prod.map f id '' F)
Tactic: have := H.2 F isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have this₁ : (y, 𝒰) ∈ Prod.map f id '' F
Tactic: have : (y, 𝒰) ∈ Prod.map f id '' F :=
      this.mem_of_tendsto (hy.prodMk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰 : Filter X) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this_1 : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
⊢ ∃ (x : X), f x = y ∧ (↑𝒰 : Filter X) ≤ nhds x
have mpr : ∀ (x : X) (snd : Ultrafilter X) (hx : (x, snd) ∈ F) (hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))),
  ∃ (x_1 : X), f x_1 = f x ∧ (↑(id snd) : Filter X) ≤ nhds x_1
Tactic: rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
Cleared hypotheses: 𝒰, y, hy, this
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : (x, snd) ∈ F
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
⊢ ∃ (x_1 : X), f x_1 = f x ∧ (↑(id snd) : Filter X) ≤ nhds x_1
have mpr : ∀ (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ id snd), False
Tactic: refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : (x, snd) ∈ F
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd
⊢ False
have mpr : ∀ (hx : ∀ t ∈ nhds (x, snd), (t ∩ {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}).Nonempty)
  (hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))) (U : Set X) (hU : U ∈ nhds x) (hUc : Uᶜ ∈ id snd), False
Tactic: rw [mem_closure_iff_nhds] at hx
Cleared hypotheses: hx, hy, U, hU, hUc
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd), (t ∩ {xℱ : X × Ultrafilter X | xℱ.2 = pure xℱ.1}).Nonempty
hy : Tendsto f (↑(id snd) : Filter X) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd
⊢ False
have mpr : ∀ (y : X) (hy : y ∈ U) (hy' : Membership.mem (γ := Ultrafilter X) (pure y) Uᶜ), False
Tactic: rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc))
      with ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
have mp : IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
mp :
  IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
have mpr : (Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)) → IsProperMap f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Maps.Proper.UniversallyClosed (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (X := X × Z) (Prod.map f id)
⊢ IsProperMap f
have mpr : Continuous f ∧ IsClosedMap (X := X × Ultrafilter X) (Prod.map f id)
Tactic: rw [isProperMap_iff_isClosedMap_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsStrictMap f ↔
    IsHomeomorph.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
      (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2))
have simp : IsQuotientMap (rangeFactorization f) ↔
  IsQuotientMap.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
    (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2))
Tactic: simp only [IsStrictMap, isHomeomorph_iff_isQuotientMap_injective, Equiv.injective, and_true]
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsStrictMap f ↔ IsEmbedding (kerLift f)
have simp : IsEmbedding.{u_1, u_2} (X := Quotient (ker f)) (Y := (↑(range f) : Type u_2))
    (⇑(quotientKerEquivRange f) : (a : Quotient (ker f)) → (↑(range f) : Type u_2)) ↔
  IsEmbedding (kerLift f)
Tactic: simp only [isStrictMap_iff_isHomeomorph_quotientKerEquivRange,
    isHomeomorph_iff_isEmbedding_surjective, Equiv.surjective, and_true]
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsStrictMap f
⊢ Continuous[inst, inst_1] f
have hf₁ : IsQuotientMap (rangeFactorization f)
Tactic: rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.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
f_quot : IsQuotientMap f
Φ : (↑(range (g ∘ f)) : Type u_3) ≃ₜ (↑(range g) : Type u_3) :=
  Homeomorph.setCongr (s := range (g ∘ f)) (t := range g) ⋯
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)
have key : rangeFactorization g ∘ f =
  (⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)
Tactic: have key : rangeFactorization g ∘ f = Φ ∘ rangeFactorization (g ∘ f) := rfl
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.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
f_quot : IsQuotientMap f
Φ : (↑(range (g ∘ f)) : Type u_3) ≃ₜ (↑(range g) : Type u_3) :=
  Homeomorph.setCongr (s := range (g ∘ f)) (t := range g) ⋯
key :
  rangeFactorization g ∘ f =
    (⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)
have simp_rw : IsQuotientMap (Y := (↑(range g) : Type u_3))
    ((⇑Φ : (a : (↑(range (g ∘ f)) : Type u_3)) → (↑(range g) : Type u_3)) ∘ rangeFactorization (g ∘ f)) ↔
  IsQuotientMap (rangeFactorization (g ∘ f))
Tactic: simp_rw [isStrictMap_iff_isQuotientMap_rangeFactorization, ← f_quot.of_comp_iff, key]
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.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
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
⊢ IsStrictMap f ↔ IsStrictMap (g ∘ f)
have key : g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)) = kerLift (g ∘ f)
Tactic: have key : g ∘ kerLift f ∘ Φ = kerLift (g ∘ f) :=
    funext <| Quotient.ind fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.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
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)) = kerLift (g ∘ f)
⊢ IsStrictMap f ↔ IsStrictMap (g ∘ f)
have simp_rw : IsEmbedding (g ∘ kerLift f) ↔
  IsEmbedding (X := Quotient (ker (g ∘ f))) (g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)))
Tactic: simp_rw [isStrictMap_iff_isEmbedding_kerLift, ← g_emb.of_comp_iff, ← key]
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsQuotientMap f ↔ IsStrictMap f ∧ Surjective f
have refine : IsStrictMap f ∧ Surjective f → ∀ (f_strict : IsStrictMap f) (f_surj : Surjective f), IsQuotientMap f
Tactic: refine ⟨fun H ↦ ⟨H.isStrictMap, H.surjective⟩, fun ⟨f_strict, f_surj⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Surjective f
f_strict : IsStrictMap f
f_surj : Surjective f
⊢ IsQuotientMap f
have f_strict₁ : IsQuotientMap (rangeFactorization f)
Tactic: rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at f_strict
Cleared hypotheses: f_strict, f_surj
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding f ↔ IsStrictMap f ∧ Injective f
have refine : IsStrictMap f ∧ Injective f → ∀ (f_strict : IsStrictMap f) (f_inj : Injective f), IsEmbedding f
Tactic: refine ⟨fun H ↦ ⟨H.isStrictMap, H.injective⟩, fun ⟨f_strict, f_inj⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Strict.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Injective f
f_strict : IsStrictMap f
f_inj : Injective f
⊢ IsEmbedding f
have f_strict₁ : IsEmbedding (kerLift f)
Tactic: rw [isStrictMap_iff_isEmbedding_kerLift] at f_strict
Cleared hypotheses: f_strict, f_inj
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : Monoid β
inst_2 : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.1 * p.2) (q.1 * q.2) ≤ (↑(LipschitzMul.C β) : ℝ) * dist p q
have rw : LipschitzWith (β := β) (LipschitzMul.C β) fun (p : β × β) ↦ p.1 * p.2
Tactic: rw [← lipschitzWith_iff_dist_le_mul]