awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst_2 : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed (X := Y) {f x}
have hx₁ : IsLocallyClosed (f '' {x})
Tactic: rw [← Set.image_singleton]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
Y : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ JacobsonSpace X
have rw : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Tactic: rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
Y : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty
have obtain : ∀ (x : X) (hx : x ∈ Z) (hx' : f x ∈ closedPoints Y), (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Tactic: obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
    (hZ.image f) (hZ'.image hf.isInducing hf.isOpen_range.isLocallyClosed)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
Y : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ JacobsonSpace X
have rw : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Tactic: rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
Y : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty
have obtain : ∀ (x : X) (hx : x ∈ Z) (hx' : f x ∈ closedPoints Y), (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Tactic: obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
    (hZ.image f) (hZ'.image hf.isInducing hf.isClosed_range.isLocallyClosed)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
⊢ closedPoints X = Set.univ
have rw : IsClosed[inst] (⋃ x ∈ closedPoints X, {x})
Tactic: rw [← Set.univ_subset_iff, ← closure_closedPoints,
      closure_subset_iff_isClosed, ← (closedPoints X).biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
⊢ DiscreteTopology X
have this : closedPoints X = Set.univ
Tactic: have : closedPoints X = Set.univ := by
    rw [← Set.univ_subset_iff, ← closure_closedPoints,
      closure_subset_iff_isClosed, ← (closedPoints X).biUnion_of_singleton]
    exact h.isClosed_biUnion fun _ ↦ id
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
⊢ DiscreteTopology X
have inst : Finite X
Tactic: have inst : Finite X := Set.finite_univ_iff.mp (this ▸ h)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
⊢ DiscreteTopology X
have rw : ∀ (s : Set X), IsOpen[inst_1] s
Tactic: rw [discreteTopology_iff_forall_isOpen]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
⊢ IsOpen[inst_1] s
have rw : IsClosed[inst_1] (⋃ x ∈ sᶜ, {x})
Tactic: rw [← isClosed_compl_iff, ← sᶜ.biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
⊢ IsClosed[inst_1] (⋃ x ∈ sᶜ, {x})
have refine : ∀ x ∈ sᶜ, IsClosed[inst_1] {x}
Tactic: refine sᶜ.toFinite.isClosed_biUnion fun x _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
x : X
h_1 : x ∈ sᶜ
⊢ IsClosed[inst_1] {x}
have rw : Membership.mem (γ := Set X) Set.univ x
Tactic: rw [← mem_closedPoints_iff, this]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
⊢ JacobsonSpace X ↔ ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
have refine : ∀ (H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)), JacobsonSpace X
Tactic: refine ⟨fun H i ↦ .of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
⊢ JacobsonSpace X
have rw : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Tactic: rw [jacobsonSpace_iff_locallyClosed]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ closedPoints X).Nonempty
have hZ₁ : ∃ (i : ι), (Z ∩ (↑(U i) : Set X)).Nonempty
Tactic: rw [← hU.iUnion_inter Z, Set.nonempty_iUnion] at hZ
Cleared hypotheses: hZ, hZ'
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ : ∃ (i : ι), (Z ∩ (↑(U i) : Set X)).Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ closedPoints X).Nonempty
have obtain : ∀ (i : ι) (x : X) (hx : x ∈ Z) (hx' : x ∈ (↑(U i) : Set X)), (Z ∩ closedPoints X).Nonempty
Tactic: obtain ⟨i, x, hx, hx'⟩ := hZ
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
⊢ (Z ∩ closedPoints X).Nonempty
have obtain : ∀ (y : ↥(U i)) (hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y)
  (hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y), (Z ∩ closedPoints X).Nonempty
Tactic: obtain ⟨y, hy, hy'⟩ := (jacobsonSpace_iff_locallyClosed.mp (H i)) _ ⟨⟨x, hx'⟩, hx⟩
    (hZ'.preimage continuous_subtype_val)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
⊢ (Z ∩ closedPoints X).Nonempty
have refine : ∀ (j : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
Tactic: refine ⟨y, hy, hU.isClosed_iff_coe_preimage.mpr fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
have pos : ∀ (h : (↑y : X) ∈ U j), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
Tactic: by_cases h : (y : X) ∈ U j
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
pos :
  ∀ (h : (↑y : X) ∈ U j),
    IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
have neg : ∀ (h : (↑y : X) ∉ U j), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
Tactic: by_cases h : (y : X) ∈ U j
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∈ U j
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
have h₁ : Eq (α := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
  {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
Tactic: convert_to IsClosed {(⟨y, h⟩ : U j)}
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∈ U j
h₁ :
  Eq (α := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
    {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
have pos : IsClosed[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
Tactic: convert_to IsClosed {(⟨y, h⟩ : U j)}
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∈ U j
⊢ Eq (α := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
    {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
have h₁ : ∀ (x : ↥(U j)),
  Membership.mem (γ := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}) x ↔
    Membership.mem (γ := Set ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∈ U j
⊢ IsClosed[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
have pos : IsLocallyClosed (X := ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
Tactic: apply isClosed_singleton_of_isLocallyClosed_singleton
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∈ U j
⊢ IsLocallyClosed (X := ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
have h₁ : Eq (α := Set ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
  (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' Set.image (α := ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i)) {y})
Tactic: convert!
      (hy'.isLocallyClosed.image IsEmbedding.subtypeVal.isInducing
            (U i).2.isOpenEmbedding_subtypeVal.isOpen_range.isLocallyClosed).preimage
        continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∈ U j
⊢ Eq (α := Set ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
    (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹'
      Set.image (α := ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i)) {y})
have h₁ : ∀ (x : ↥(U j)),
  Membership.mem (γ := Set ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h} x ↔
    Membership.mem (γ := Set ↥(U j))
      (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹'
        Set.image (α := ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i)) {y})
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∉ U j
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
have h₁ : Eq (α := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}) ∅
Tactic: convert! isClosed_empty
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∉ U j
⊢ Eq (α := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}) ∅
have h₁ : ∀ (x : ↥(U j)), x ∉ Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ (↑(U i) : Set X)
y : ↥(U i)
hy : Membership.mem (γ := Set ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i) ⁻¹' Z) y
hy' : Membership.mem (γ := Set ↥(U i)) (closedPoints ↥(U i)) y
j : ι
h : (↑y : X) ∉ U j
z : ↥(U j)
⊢ z ∉ Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}
have h₁ : ∀ (hz : (↑z : X) = (↑y : X)), False
Tactic: (hz : z.1 = y.1)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hS' : IsPreirreducible S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
⊢ (f '' closure[inst] S).Subsingleton
have inl : ∀ (hS : IsLocallyClosed.{u_1} (X := X) ∅) (hS' : IsPreirreducible.{u_1} (X := X) ∅) (hfS : (f '' ∅).Finite),
  (f '' closure[inst] ∅).Subsingleton
Tactic: obtain rfl | hS'' := S.eq_empty_or_nonempty
Cleared hypotheses: S, hS, hS', hfS
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hS' : IsPreirreducible S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
inl :
  ∀ (hS : IsLocallyClosed.{u_1} (X := X) ∅) (hS' : IsPreirreducible.{u_1} (X := X) ∅) (hfS : (f '' ∅).Finite),
    (f '' closure[inst] ∅).Subsingleton
⊢ (f '' closure[inst] S).Subsingleton
have inr : ∀ (hS'' : S.Nonempty), (f '' closure[inst] S).Subsingleton
Tactic: obtain rfl | hS'' := S.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hS' : IsPreirreducible S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
⊢ (f '' closure[inst] S).Subsingleton
have hS'₁ : IsIrreducible S
Tactic: replace hS' : IsIrreducible S := ⟨hS'', hS'⟩
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
⊢ IsIrreducible (S ∩ closedPoints X)
have rwa : ∀ (hS' : IsIrreducible (closure[inst] S)), IsIrreducible (S ∩ closedPoints X)
Tactic: rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
rwa : ∀ (hS' : IsIrreducible (closure[inst] S)), IsIrreducible (S ∩ closedPoints X)
⊢ IsIrreducible (S ∩ closedPoints X)
have rwa₁ : ∀ (hS' : IsIrreducible (closure[inst] (S ∩ closedPoints X))), IsIrreducible (S ∩ closedPoints X)
Tactic: rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
rwa : ∀ (hS' : IsIrreducible (closure[inst] S)), IsIrreducible (S ∩ closedPoints X)
rwa₁ : ∀ (hS' : IsIrreducible (closure[inst] (S ∩ closedPoints X))), IsIrreducible (S ∩ closedPoints X)
⊢ IsIrreducible (S ∩ closedPoints X)
have rwa₂ : ∀ (hS' : IsIrreducible (S ∩ closedPoints X)), IsIrreducible (S ∩ closedPoints X)
Tactic: rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
⊢ (f '' closure[inst] S).Subsingleton
have H₁ : IsIrreducible (S ∩ closedPoints X)
Tactic: have H₁ : IsIrreducible (S ∩ closedPoints X) := by
    rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
⊢ (f '' closure[inst] S).Subsingleton
have H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
Tactic: have H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y := by
    rintro _ ⟨x, hx, rfl⟩; simpa using hf₂ _ hx.2
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
⊢ (f '' closure[inst] S).Subsingleton
have H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
Tactic: have H₃ := ((hfS.subset (Set.image_mono Set.inter_subset_left)).isDiscrete_of_subset_closedPoints
    H₂).subsingleton_of_isPreirreducible (H₁.image _ hf₁.continuousOn).isPreirreducible
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))
have inl : ∀ (h : f '' (S ∩ closedPoints X) = ∅), IsClosed[inst_1] (f '' (S ∩ closedPoints X))
Tactic: obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
inl : ∀ (h : f '' (S ∩ closedPoints X) = ∅), IsClosed[inst_1] (f '' (S ∩ closedPoints X))
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))
have inr : ∀ (x : Y) (hx : x ∈ f '' (S ∩ closedPoints X)), IsClosed[inst_1] (f '' (S ∩ closedPoints X))
Tactic: obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
hS'' : S.Nonempty
hS' : IsIrreducible S
H₁ : IsIrreducible (S ∩ closedPoints X)
H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y
H₃ : (f '' (S ∩ closedPoints X)).Subsingleton
x : Y
hx : x ∈ f '' (S ∩ closedPoints X)
⊢ IsClosed[inst_1] (f '' (S ∩ closedPoints X))
have inr : IsClosed[inst_1] {x}
Tactic: rw [H₃.eq_singleton_of_mem hx]