awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ Set.InjOn (↑(hf.localInverseAt x).symm : X → Y) (hf.localInverseAt x).target

Tactic:
exact (hf.localInverseAt x).symm.injOn

Premises used: IsLocalHomeomorph.localInverseAt, OpenPartialHomeomorph.injOn, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
y : Y
hx : y ∈ (hf.localInverseAt x).source
rw : (↑(hf.localInverseAt x).symm : X → Y) ((↑(hf.localInverseAt x) : Y → X) y) = y
⊢ f ((↑(hf.localInverseAt x) : Y → X) y) = y

Tactic:
rw [← congrFun (hf.localInverseAt_symm x)]

Premises used: IsLocalHomeomorph.localInverseAt_symm, congrFun
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
y : Y
hx : y ∈ (hf.localInverseAt x).source
⊢ (↑(hf.localInverseAt x).symm : X → Y) ((↑(hf.localInverseAt x) : Y → X) y) = y

Tactic:
(hf.localInverseAt x).left_inv hx

Premises used: IsLocalHomeomorph.localInverseAt, OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
y : Y
hx : y ∈ (hf.localInverseAt x).source
⊢ (↑(hf.localInverseAt x).symm : X → Y) ((↑(hf.localInverseAt x) : Y → X) y) = y

Tactic:
exact (hf.localInverseAt x).left_inv hx

Premises used: IsLocalHomeomorph.localInverseAt, OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Topology.IsLocalHomeomorph
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ (↑(hf.localInverseAt x) : Y → X) (f x) ∈ (hf.localInverseAt x).target

Tactic:
simp
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ∈ closedPoints X ↔ IsClosed[inst] {x}

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closedPoints
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst, inst_1] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ IsClosed[inst] (f ⁻¹' {f x})

Tactic:
continuous_iff_isClosed.mp hf' _ hx

Premises used: continuous_iff_isClosed, Iff.mp
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst, inst_1] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
h : {x} = f ⁻¹' {f x}
⊢ IsClosed[inst] {x}

Tactic:
convert! continuous_iff_isClosed.mp hf' _ hx

Premises used: continuous_iff_isClosed, Iff.mp
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst, inst_1] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
h : {x} = f ⁻¹' f '' {x}
h₁ h₂ : Eq (α := Set X) {x} {x}
⊢ {x} = f ⁻¹' {f x}

Tactic:
rw [← Set.image_singleton, Set.preimage_image_eq _ hf]

Premises used: Set.image_singleton, Set.preimage_image_eq
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
h : ∀ (x : X), x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
ext x
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
x : X
⊢ x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X

Tactic:
simp [mem_closedPoints_iff, ← Set.image_singleton, hf.isClosed_iff_image_isClosed]

Premises used: Set.image_singleton, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, mem_closedPoints_iff
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ closedPoints X = Set.univ

Tactic:
Set.eq_univ_iff_forall.mpr fun _ ↦ isClosed_singleton

Premises used: Iff.mpr, Set.eq_univ_iff_forall, isClosed_singleton
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
x : (↑s : Type u_1)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' {(↑x : X)})

Tactic:
(hs' x.2).preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage, Subtype.property
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
x : (↑s : Type u_1)
h :
  (↑s : Type u_1) = { x : X // x ∈ s } →
    Eq (α := Set (↑s : Type u_1)) {x} (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' {(↑x : X)})
⊢ IsClosed[instTopologicalSpaceSubtype] {x}

Tactic:
convert! (hs' x.2).preimage continuous_subtype_val

Premises used: continuous_subtype_val, IsClosed.preimage, Subtype.property
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
x : (↑s : Type u_1)
e_1 : (↑s : Type u_1) = { x : X // x ∈ s }
⊢ Eq (α := Set (↑s : Type u_1)) {x} (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' {(↑x : X)})

Tactic:
aesop
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
⊢ T1Space.{u_1} (↑s : Type u_1)

Tactic:
have : T1Space s := ⟨fun x ↦ by convert! (hs' x.2).preimage continuous_subtype_val; aesop⟩
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
this : T1Space.{u_1} (↑s : Type u_1)
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : Finite s := hs
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
this_1 : T1Space.{u_1} (↑s : Type u_1)
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ IsDiscrete s

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, IsDiscrete.mk
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
this_1 : T1Space.{u_1} (↑s : Type u_1)
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ IsDiscrete s

Tactic:
exact ⟨inferInstance⟩
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
⊢ closure[inst] (closedPoints X) = Set.univ

Tactic:
simpa using closure_inter_closedPoints isClosed_univ

Premises used: isClosed_univ, JacobsonSpace.closure_inter_closedPoints
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
rw :
  (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
⊢ JacobsonSpace X ↔ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
rw [jacobsonSpace_iff]

Premises used: jacobsonSpace_iff
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
mp :
  (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
mpr :
  (∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty) →
    ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
⊢ (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
constructor
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
mp :
  (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z ≠ ∅ → IsClosed[inst] (closure[inst] Z \ Z) → Z ∩ closedPoints X ≠ ∅
⊢ (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
simp_rw [isLocallyClosed_iff_isOpen_coborder, coborder, isOpen_compl_iff,
      Set.nonempty_iff_ne_empty]

Premises used: coborder, Set.nonempty_iff_ne_empty, isLocallyClosed_iff_isOpen_coborder, isOpen_compl_iff
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ Z ⊆ closure[inst] Z \ Z

Tactic:
subset_closure.trans ?_

Premises used: subset_closure, HasSubset.Subset.trans
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
refine : closure[inst] Z ⊆ closure[inst] Z \ Z
⊢ Z ⊆ closure[inst] Z \ Z

Tactic:
refine subset_closure.trans ?_

Premises used: subset_closure, HasSubset.Subset.trans
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
nth_rw : closure[inst] (closure[inst] Z ∩ closedPoints X) ⊆ closure[inst] Z \ Z
⊢ closure[inst] Z ⊆ closure[inst] Z \ Z

Tactic:
nth_rw 1 [← H isClosed_closure]

Premises used: isClosed_closure
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
rw : closure[inst] Z ∩ closedPoints X ⊆ closure[inst] Z ∧ closure[inst] Z ∩ ∅ ⊆ ∅
⊢ closure[inst] (closure[inst] Z ∩ closedPoints X) ⊆ closure[inst] Z \ Z

Tactic:
rw [hZ'.closure_subset_iff, Set.subset_diff, Set.disjoint_iff, Set.inter_assoc,
        Set.inter_comm _ Z, e]

Premises used: Set.subset_diff, IsClosed.closure_subset_iff, Set.inter_comm, Set.inter_assoc, Set.disjoint_iff
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure[inst] Z ∩ closedPoints X ⊆ closure[inst] Z ∧ closure[inst] Z ∩ ∅ ⊆ ∅

Tactic:
⟨Set.inter_subset_left, Set.inter_subset_right⟩

Premises used: Set.inter_subset_left, And.intro, Set.inter_subset_right
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure[inst] Z ∩ closedPoints X ⊆ closure[inst] Z ∧ closure[inst] Z ∩ ∅ ⊆ ∅

Tactic:
exact ⟨Set.inter_subset_left, Set.inter_subset_right⟩
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ Z ⊆ closure[inst] Z \ Z

Tactic:
have : Z ⊆ closure Z \ Z := by
      refine subset_closure.trans ?_
      nth_rw 1 [← H isClosed_closure]
      rw [hZ'.closure_subset_iff, Set.subset_diff, Set.disjoint_iff, Set.inter_assoc,
        Set.inter_comm _ Z, e]
      exact ⟨Set.inter_subset_left, Set.inter_subset_right⟩
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst] Z \ Z
⊢ Z ⊆ closure[inst] Z ∧ Z = ∅

Tactic:
rw [Set.subset_diff, disjoint_self, Set.bot_eq_empty] at this

Premises used: Set.subset_diff, Set.bot_eq_empty, disjoint_self
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst] Z ∧ Z = ∅
⊢ False

Tactic:
hZ this.2

Premises used: And.right
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst] (closure[inst] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst] Z ∧ Z = ∅
⊢ False

Tactic:
exact hZ this.2

Premises used: And.right
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
⊢ closure[inst] (Z ∩ closedPoints X) = Z

Tactic:
subset_antisymm (hZ.closure_subset_iff.mpr Set.inter_subset_left) ?_

Premises used: Iff.mpr, subset_antisymm, Set.inter_subset_left, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
mpr : Z ⊆ closure[inst] (Z ∩ closedPoints X)
⊢ closure[inst] (Z ∩ closedPoints X) = Z

Tactic:
refine subset_antisymm (hZ.closure_subset_iff.mpr Set.inter_subset_left) ?_

Premises used: Iff.mpr, subset_antisymm, Set.inter_subset_left, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
mpr : ¬((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
⊢ Z ⊆ closure[inst] (Z ∩ closedPoints X)

Tactic:
rw [← Set.disjoint_compl_left_iff_subset, Set.disjoint_iff_inter_eq_empty,
      ← Set.not_nonempty_iff_eq_empty]

Premises used: Set.disjoint_compl_left_iff_subset, Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
H' : ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
⊢ ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty

Tactic:
have := H _ H' (isClosed_closure.isOpen_compl.isLocallyClosed.inter hZ.isLocallyClosed)
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
H' : ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty
⊢ ¬Z ∩ closedPoints X ⊆ closure[inst] (Z ∩ closedPoints X)

Tactic:
rw [Set.nonempty_iff_ne_empty, Set.inter_assoc, ne_eq,
      ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset] at this

Premises used: Set.disjoint_compl_left_iff_subset, ne_eq, Set.disjoint_iff_inter_eq_empty, Set.nonempty_iff_ne_empty, Set.inter_assoc
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
H' : ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬Z ∩ closedPoints X ⊆ closure[inst] (Z ∩ closedPoints X)
⊢ False

Tactic:
this subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst] Z
H' : ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬Z ∩ closedPoints X ⊆ closure[inst] (Z ∩ closedPoints X)
⊢ False

Tactic:
exact this subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ closedPoints X).Nonempty

Tactic:
jacobsonSpace_iff_locallyClosed.mp inferInstance Z hZ hZ'

Premises used: inferInstance, jacobsonSpace_iff_locallyClosed, Iff.mp
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
⊢ closure[inst] (S ∩ closedPoints X) = closure[inst] S

Tactic:
(closure_mono (Set.inter_subset_left)).antisymm ?_

Premises used: Set.inter_subset_left, closure_mono, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
refine : closure[inst] S ⊆ closure[inst] (S ∩ closedPoints X)
⊢ closure[inst] (S ∩ closedPoints X) = closure[inst] S

Tactic:
refine (closure_mono (Set.inter_subset_left)).antisymm ?_

Premises used: Set.inter_subset_left, closure_mono, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
rw : S ⊆ closure[inst] (S ∩ closedPoints X)
⊢ closure[inst] S ⊆ closure[inst] (S ∩ closedPoints X)

Tactic:
rw [IsClosed.closure_subset_iff isClosed_closure]

Premises used: IsClosed.closure_subset_iff, isClosed_closure
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
x : X
hx : x ∈ S
by_contra : ∀ (H : x ∉ closure[inst] (S ∩ closedPoints X)), False
⊢ x ∈ closure[inst] (S ∩ closedPoints X)

Tactic:
by_contra H
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
x : X
hx : x ∈ S
H : x ∉ closure[inst] (S ∩ closedPoints X)
obtain : ∀ (y : X) (hy₃ : y ∈ closedPoints X) (hy₁ : y ∈ S) (hy₂ : y ∉ closure[inst] (S ∩ closedPoints X)), False
⊢ False

Tactic:
obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := nonempty_inter_closedPoints (Z := S \ closure (S ∩ closedPoints X))
    ⟨x, hx, H⟩ (.inter hS isClosed_closure.isOpen_compl.isLocallyClosed)

Premises used: nonempty_inter_closedPoints, IsClosed.isOpen_compl, IsLocallyClosed.inter, IsOpen.isLocallyClosed, And.intro, Exists.intro
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
x : X
hx : x ∈ S
H : x ∉ closure[inst] (S ∩ closedPoints X)
y : X
hy₃ : y ∈ closedPoints X
hy₁ : y ∈ S
hy₂ : y ∉ closure[inst] (S ∩ closedPoints X)
⊢ False

Tactic:
hy₂ (subset_closure ⟨hy₁, hy₃⟩)

Premises used: subset_closure, And.intro
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
x : X
hx : x ∈ S
H : x ∉ closure[inst] (S ∩ closedPoints X)
y : X
hy₃ : y ∈ closedPoints X
hy₁ : y ∈ S
hy₂ : y ∉ closure[inst] (S ∩ closedPoints X)
⊢ False

Tactic:
exact hy₂ (subset_closure ⟨hy₁, hy₃⟩)

Premises used: subset_closure, And.intro
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
x : X
hx : IsLocallyClosed (X := X) {x}
⊢ x ∈ closedPoints X

Tactic:
obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
    nonempty_inter_closedPoints (Set.singleton_nonempty x) hx

Premises used: Set.singleton_nonempty, nonempty_inter_closedPoints, rfl
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
x : X
hx : IsLocallyClosed (X := X) {x}
hy' : x ∈ closedPoints X
⊢ IsClosed[inst] {x}

Tactic:
hy'

Premises used: Set.Mem, setOf, closedPoints
-- Module: Mathlib.Topology.JacobsonSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
x : X
hx : IsLocallyClosed (X := X) {x}
hy' : x ∈ closedPoints X
⊢ IsClosed[inst] {x}

Tactic:
exact hy'
-- Module: Mathlib.Topology.JacobsonSpace
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
apply : closedPoints X ⊆ f ⁻¹' closedPoints Y
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
apply subset_antisymm (preimage_closedPoints_subset hf.injective hf.continuous)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.continuous, subset_antisymm, preimage_closedPoints_subset, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.JacobsonSpace
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
hx₁ : IsLocallyClosed (X := Y) {f x}
⊢ x ∈ f ⁻¹' closedPoints Y

Tactic:
apply isClosed_singleton_of_isLocallyClosed_singleton

Premises used: isClosed_singleton_of_isLocallyClosed_singleton
-- Module: Mathlib.Topology.JacobsonSpace
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
hx₁ : IsLocallyClosed (f '' {x})
⊢ IsLocallyClosed (X := Y) {f x}

Tactic:
rw [← Set.image_singleton]

Premises used: Set.image_singleton
-- Module: Mathlib.Topology.JacobsonSpace
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 (f '' {x})

Tactic:
(hx.isLocallyClosed.image hf.isInducing hf.isOpen_range.isLocallyClosed)

Premises used: IsLocallyClosed.image, IsOpen.isLocallyClosed, Topology.IsOpenEmbedding.isOpen_range, Topology.IsOpenEmbedding.isInducing, IsClosed.isLocallyClosed
-- Module: Mathlib.Topology.JacobsonSpace
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 (f '' {x})

Tactic:
exact (hx.isLocallyClosed.image hf.isInducing hf.isOpen_range.isLocallyClosed)

Premises used: IsLocallyClosed.image, IsOpen.isLocallyClosed, Topology.IsOpenEmbedding.isOpen_range, Topology.IsOpenEmbedding.isInducing, IsClosed.isLocallyClosed
-- 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 : IsOpenEmbedding 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.IsOpenEmbedding.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 : IsOpenEmbedding 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.isOpen_range.isLocallyClosed)

Premises used: IsLocallyClosed.image, nonempty_inter_closedPoints, IsOpen.isLocallyClosed, Topology.IsOpenEmbedding.isOpen_range, Set.Nonempty.image, Topology.IsOpenEmbedding.isInducing, 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 : IsOpenEmbedding 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 : IsOpenEmbedding 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'⟩