awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.JacobsonSpace
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
rw : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]

Premises used: jacobsonSpace_iff_locallyClosed, Topology.IsClosedEmbedding.preimage_closedPoints
-- Module: Mathlib.Topology.JacobsonSpace
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
obtain : ∀ (x : X) (hx : x ∈ Z) (hx' : f x ∈ closedPoints Y), (Z ∩ f ⁻¹' closedPoints Y).Nonempty
⊢ (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)

Premises used: IsLocallyClosed.image, Topology.IsClosedEmbedding.isInducing, nonempty_inter_closedPoints, Set.Nonempty.image, IsClosed.isLocallyClosed, Topology.IsClosedEmbedding.isClosed_range, rfl
-- Module: Mathlib.Topology.JacobsonSpace
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
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
⟨_, hx, hx'⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.JacobsonSpace
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
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
exact ⟨_, hx, hx'⟩
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
rw : IsClosed[inst] (⋃ x ∈ closedPoints X, {x})
⊢ closedPoints X = Set.univ

Tactic:
rw [← Set.univ_subset_iff, ← closure_closedPoints,
      closure_subset_iff_isClosed, ← (closedPoints X).biUnion_of_singleton]

Premises used: Set.univ_subset_iff, closure_subset_iff_isClosed, Set.biUnion_of_singleton, closedPoints, closure_closedPoints
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
⊢ IsClosed[inst] (⋃ x ∈ closedPoints X, {x})

Tactic:
h.isClosed_biUnion fun _ ↦ id

Premises used: id, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
⊢ IsClosed[inst] (⋃ x ∈ closedPoints X, {x})

Tactic:
exact h.isClosed_biUnion fun _ ↦ id

Premises used: id, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
⊢ 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
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
⊢ Finite X

Tactic:
have inst : Finite X := Set.finite_univ_iff.mp (this ▸ h)
-- Module: Mathlib.Topology.JacobsonSpace
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
rw : ∀ (s : Set X), IsOpen[inst_1] s
⊢ DiscreteTopology X

Tactic:
rw [discreteTopology_iff_forall_isOpen]

Premises used: discreteTopology_iff_forall_isOpen
-- Module: Mathlib.Topology.JacobsonSpace
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
rw : IsClosed[inst_1] (⋃ x ∈ sᶜ, {x})
⊢ IsOpen[inst_1] s

Tactic:
rw [← isClosed_compl_iff, ← sᶜ.biUnion_of_singleton]

Premises used: Compl.compl, Set.biUnion_of_singleton, isClosed_compl_iff
-- Module: Mathlib.Topology.JacobsonSpace
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})

Tactic:
sᶜ.toFinite.isClosed_biUnion fun x _ ↦ ?_

Premises used: Compl.compl, Set.toFinite, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.JacobsonSpace
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
refine : ∀ x ∈ sᶜ, IsClosed[inst_1] {x}
⊢ IsClosed[inst_1] (⋃ x ∈ sᶜ, {x})

Tactic:
refine sᶜ.toFinite.isClosed_biUnion fun x _ ↦ ?_

Premises used: Compl.compl, Set.toFinite, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.JacobsonSpace
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ᶜ
rw : Membership.mem (γ := Set X) Set.univ x
⊢ IsClosed[inst_1] {x}

Tactic:
rw [← mem_closedPoints_iff, this]

Premises used: mem_closedPoints_iff
-- Module: Mathlib.Topology.JacobsonSpace
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ᶜ
⊢ Membership.mem (γ := Set X) Set.univ x

Tactic:
trivial
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type ?u.14233
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : Finite X
inst_3 : JacobsonSpace X
⊢ DiscreteTopology X

Tactic:
JacobsonSpace.discreteTopology (Set.toFinite _)

Premises used: JacobsonSpace.discreteTopology, Set.toFinite
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type ?u.14372
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : T1Space X
⊢ ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z

Tactic:
simp [closedPoints_eq_univ, closure_eq_iff_isClosed]

Premises used: closure_eq_iff_isClosed, closedPoints_eq_univ
-- Module: Mathlib.Topology.JacobsonSpace
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)

Tactic:
⟨fun H i ↦ .of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal, fun H ↦ ?_⟩

Premises used: IsOpen.isOpenEmbedding_subtypeVal, JacobsonSpace.of_isOpenEmbedding, Iff.intro, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
refine : ∀ (H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)), JacobsonSpace X
⊢ JacobsonSpace X ↔ ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)

Tactic:
refine ⟨fun H i ↦ .of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal, fun H ↦ ?_⟩
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace.{u_2} ↥(U i)
rw : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed]

Premises used: jacobsonSpace_iff_locallyClosed
-- Module: Mathlib.Topology.JacobsonSpace
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
⊢ ∃ (i : ι), (Z ∩ (↑(U i) : Set X)).Nonempty

Tactic:
rw [← hU.iUnion_inter Z, Set.nonempty_iUnion] at hZ

Premises used: Set.nonempty_iUnion, TopologicalSpace.IsOpenCover.iUnion_inter
-- Module: Mathlib.Topology.JacobsonSpace
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
hZ₁ : ∃ (i : ι), (Z ∩ (↑(U i) : Set X)).Nonempty
⊢ IsLocallyClosed Z

Tactic:
rw [← hU.iUnion_inter Z, Set.nonempty_iUnion] at hZ

Premises used: Set.nonempty_iUnion, TopologicalSpace.IsOpenCover.iUnion_inter
-- Module: Mathlib.Topology.JacobsonSpace
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
obtain : ∀ (i : ι) (x : X) (hx : x ∈ Z) (hx' : x ∈ (↑(U i) : Set X)), (Z ∩ closedPoints X).Nonempty
⊢ (Z ∩ closedPoints X).Nonempty

Tactic:
obtain ⟨i, x, hx, hx'⟩ := hZ
-- Module: Mathlib.Topology.JacobsonSpace
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)
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
⊢ (Z ∩ closedPoints X).Nonempty

Tactic:
obtain ⟨y, hy, hy'⟩ := (jacobsonSpace_iff_locallyClosed.mp (H i)) _ ⟨⟨x, hx'⟩, hx⟩
    (hZ'.preimage continuous_subtype_val)

Premises used: continuous_subtype_val, jacobsonSpace_iff_locallyClosed, Subtype.mk, IsLocallyClosed.preimage, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.JacobsonSpace
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

Tactic:
⟨y, hy, hU.isClosed_iff_coe_preimage.mpr fun j ↦ ?_⟩

Premises used: Iff.mpr, TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage, Set.Nonempty, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.JacobsonSpace
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
refine : ∀ (j : ι), IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})
⊢ (Z ∩ closedPoints X).Nonempty

Tactic:
refine ⟨y, hy, hU.isClosed_iff_coe_preimage.mpr fun j ↦ ?_⟩
-- Module: Mathlib.Topology.JacobsonSpace
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)})
neg :
  ∀ (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)})

Tactic:
by_cases h : (y : X) ∈ U j

Premises used: Subtype.val
-- Module: Mathlib.Topology.JacobsonSpace
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}
pos : IsClosed[instTopologicalSpaceSubtype] {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)})

Tactic:
convert_to IsClosed {(⟨y, h⟩ : U j)}

Premises used: Subtype.mk, IsClosed, Singleton.singleton, Subtype.val
-- Module: Mathlib.Topology.JacobsonSpace
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₁ :
  ∀ (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
⊢ 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:
ext
-- Module: Mathlib.Topology.JacobsonSpace
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
x_1 : ↥(U j)
⊢ Membership.mem (γ := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}) x_1 ↔
    Membership.mem (γ := Set ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h} x_1

Tactic:
simp [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.Topology.JacobsonSpace
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
pos : IsLocallyClosed (X := ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}
⊢ IsClosed[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}

Tactic:
apply isClosed_singleton_of_isLocallyClosed_singleton

Premises used: isClosed_singleton_of_isLocallyClosed_singleton
-- Module: Mathlib.Topology.JacobsonSpace
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.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹'
      Set.image (α := ↥(U i)) (Subtype.val (p := fun (x : X) ↦ x ∈ U i)) {y})

Tactic:
(hy'.isLocallyClosed.image IsEmbedding.subtypeVal.isInducing
            (U i).2.isOpenEmbedding_subtypeVal.isOpen_range.isLocallyClosed).preimage
        continuous_subtype_val

Premises used: IsLocallyClosed.image, IsOpen.isOpenEmbedding_subtypeVal, continuous_subtype_val, Topology.IsEmbedding.isInducing, IsOpen.isLocallyClosed, Topology.IsOpenEmbedding.isOpen_range, IsLocallyClosed.preimage, IsClosed.isLocallyClosed, TopologicalSpace.Opens.is_open', Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.JacobsonSpace
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.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})
⊢ IsLocallyClosed (X := ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h}

Tactic:
convert!
      (hy'.isLocallyClosed.image IsEmbedding.subtypeVal.isInducing
            (U i).2.isOpenEmbedding_subtypeVal.isOpen_range.isLocallyClosed).preimage
        continuous_subtype_val

Premises used: IsLocallyClosed.image, IsOpen.isOpenEmbedding_subtypeVal, continuous_subtype_val, Topology.IsEmbedding.isInducing, IsOpen.isLocallyClosed, Topology.IsOpenEmbedding.isOpen_range, IsLocallyClosed.preimage, IsClosed.isLocallyClosed, TopologicalSpace.Opens.is_open', Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.JacobsonSpace
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₁ :
  ∀ (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
⊢ 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:
ext
-- Module: Mathlib.Topology.JacobsonSpace
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
x_1 : ↥(U j)
⊢ Membership.mem (γ := Set ↥(U j)) {Subtype.mk (p := fun (x : X) ↦ x ∈ U j) (↑y : X) h} x_1 ↔
    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_1

Tactic:
simp [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.Topology.JacobsonSpace
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] ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.JacobsonSpace
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)}) ∅
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)})

Tactic:
convert! isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.JacobsonSpace
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₁ : ∀ (x : ↥(U j)), x ∉ Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}
⊢ Eq (α := Set ↥(U j)) (Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}) ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.JacobsonSpace
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)
h₁ : ∀ (hz : (↑z : X) = (↑y : X)), False
⊢ z ∉ Subtype.val (p := fun (x : X) ↦ x ∈ U j) ⁻¹' {(↑y : X)}

Tactic:
(hz : z.1 = y.1)
-- Module: Mathlib.Topology.JacobsonSpace
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)
hz : (↑z : X) = (↑y : X)
⊢ False

Tactic:
h (hz ▸ z.2)

Premises used: Eq.rec, Subtype.property
-- Module: Mathlib.Topology.JacobsonSpace
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)
hz : (↑z : X) = (↑y : X)
⊢ False

Tactic:
exact h (hz ▸ z.2)

Premises used: Eq.rec, Subtype.property
-- Module: Mathlib.Topology.JacobsonSpace
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
inr : ∀ (hS'' : S.Nonempty), (f '' closure[inst] S).Subsingleton
⊢ (f '' closure[inst] S).Subsingleton

Tactic:
obtain rfl | hS'' := S.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : JacobsonSpace X
hf₁ : Continuous[inst, inst_1] f
hf₂ : IsClosedMap f
hS : IsLocallyClosed.{u_1} (X := X) ∅
hS' : IsPreirreducible.{u_1} (X := X) ∅
hfS : (f '' ∅).Finite
⊢ (f '' closure[inst] ∅).Subsingleton

Tactic:
simp
-- Module: Mathlib.Topology.JacobsonSpace
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
⊢ IsIrreducible S

Tactic:
replace hS' : IsIrreducible S := ⟨hS'', hS'⟩