awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
refine_1 :
  ∀ (u : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        u →
      IsOpen[inst] u
⊢ IsTopologicalBasis.{u_1} (α := X)
    {U : Set X |
      ∃ (V : Set Y),
        IsOpen[inst_1] V ∧
          ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
            Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
              Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
have refine_2 : ∀ (x : X) (U : Set X) (hx : x ∈ U) (hU : IsOpen[inst] U),
  ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen[inst_1] U
s : ContinuousMap.{u_2, u_1} (↑U : Type u_2) X
hs : Eq (α := (↑U : Type u_2) → Y) (f ∘ (⇑s : (a : (↑U : Type u_2)) → X)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U))
⊢ IsOpen[inst] (Set.range.{u_1, u_2 + 1} (ι := (↑U : Type u_2)) (⇑s : (a : (↑U : Type u_2)) → X))
have refine_1 : IsOpen[inst_1] (Set.range (ι := (↑U : Type u_2)) (Subtype.val (p := fun (x : Y) ↦ x ∈ U)))
Tactic: refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩)
      s.continuous).isOpen_range
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) (f ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U
have refine_2 : ∀ (f : OpenPartialHomeomorph X Y) (hxf : x ∈ f.source) (hf : IsLocalHomeomorph (↑f : X → Y)),
  ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) ((↑f : X → Y) ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U
Tactic: obtain ⟨f, hxf, rfl⟩ := hf x
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) ((↑f : X → Y) ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U
have refine_2 : Eq (α := (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) → Y)
  ((↑f : X → Y) ∘
    (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun, continuous_toFun := sorry :
          ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
      (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
  (Subtype.val (p := fun (x : Y) ↦ x ∈ f.target ∩ (↑f.symm : Y → X) ⁻¹' U))
Tactic: refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
      ⟨_, continuousOn_iff_continuous_restrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩,
      ?_, (Set.range_restrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 :
  Eq (α := (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) → Y)
    ((↑f : X → Y) ∘
      (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
            continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
        (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
    (Subtype.val (p := fun (x : Y) ↦ x ∈ f.target ∩ (↑f.symm : Y → X) ⁻¹' U))
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X))
        {U : Set X |
          ∃ (V : Set Y),
            IsOpen[inst_1] V ∧
              ∃ (s : ContinuousMap.{u_2, u_1} (↑V : Type u_2) X),
                Eq (α := (↑V : Type u_2) → Y) ((↑f : X → Y) ∘ (⇑s : (a : (↑V : Type u_2)) → X))
                    (Subtype.val (p := fun (x : Y) ↦ x ∈ V)) ∧
                  Set.range.{u_1, u_2 + 1} (ι := (↑V : Type u_2)) (⇑s : (a : (↑V : Type u_2)) → X) = U}
        v ∧
      x ∈ v ∧ v ⊆ U
have refine_2₁ : f.toPartialEquiv.2 '' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
Tactic: refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
      ⟨_, continuousOn_iff_continuous_restrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩,
      ?_, (Set.range_restrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ Eq (α := (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) → Y)
    ((↑f : X → Y) ∘
      (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
            continuous_toFun := ⋯ : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
        (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
    (Subtype.val (p := fun (x : Y) ↦ x ∈ f.target ∩ (↑f.symm : Y → X) ⁻¹' U))
have refine_2 : ∀ (y : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)),
  ((↑f : X → Y) ∘
        (⇑{ toFun := (f.target ∩ (↑f.symm : Y → X) ⁻¹' U).restrict (π := fun (a : Y) ↦ X) f.invFun,
              continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2) X } :
          (a : (↑(f.target ∩ (↑f.symm : Y → X) ⁻¹' U) : Type u_2)) → X))
      y =
    (↑y : Y)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ f.toPartialEquiv.2 '' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
have refine_2 : f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
Tactic: apply (f.symm_image_target_inter_eq _).trans
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
⊢ f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
have refine_2 : f.source ∩ ((↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
Tactic: rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 : f.source ∩ ((↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
⊢ f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
have refine_2₁ : f.source ∩ (↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
Tactic: rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 : f.source ∩ ((↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
refine_2₁ : f.source ∩ (↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
⊢ f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
have refine_2₂ : f.source ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
Tactic: rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph (↑f : X → Y)
refine_2 : f.source ∩ ((↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
refine_2₁ : f.source ∩ (↑f : X → Y) ⁻¹' f.target ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
refine_2₂ : f.source ∩ (↑f : X → Y) ⁻¹' (↑f.symm : Y → X) ⁻¹' U = f.source ∩ U
⊢ f.source ∩ (↑f : X → Y) ⁻¹' (f.target ∩ (↑f.symm : Y → X) ⁻¹' U) = f.source ∩ U
have refine_2₃ : f.source ∩ U = f.source ∩ U
Tactic: rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ f x ∈ (hf.localInverseAt x).source
have rw : (↑(hf.localInverseAt x).symm : X → Y) x ∈ (hf.localInverseAt x).source
Tactic: rw [← congrFun (hf.localInverseAt_symm x)]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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 f (hf.localInverseAt x).target
have rw : Set.InjOn (↑(hf.localInverseAt x).symm : X → Y) (hf.localInverseAt x).target
Tactic: rw [Set.EqOn.injOn_iff (f₂ := (hf.localInverseAt x).symm) (fun y _ ↦ by simp)]
-- Lean 4 proof step from Mathlib.Topology.IsLocalHomeomorph (goal)
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
⊢ f ((↑(hf.localInverseAt x) : Y → X) y) = y
have rw : (↑(hf.localInverseAt x).symm : X → Y) ((↑(hf.localInverseAt x) : Y → X) y) = y
Tactic: rw [← congrFun (hf.localInverseAt_symm 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
hf : Function.Injective f
hf' : Continuous[inst, inst_1] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ IsClosed[inst] {x}
have h : {x} = f ⁻¹' {f x}
Tactic: convert! continuous_iff_isClosed.mp hf' _ hx
-- 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 : Function.Injective f
hf' : Continuous[inst, inst_1] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' {f x}
have h : {x} = f ⁻¹' f '' {x}
Tactic: rw [← Set.image_singleton, Set.preimage_image_eq _ hf]
-- 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 : Function.Injective f
hf' : Continuous[inst, inst_1] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
h : {x} = f ⁻¹' f '' {x}
⊢ {x} = f ⁻¹' {f x}
have h₁ : Eq (α := Set X) {x} {x}
Tactic: rw [← Set.image_singleton, Set.preimage_image_eq _ hf]
-- 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 : IsClosedEmbedding f
⊢ f ⁻¹' closedPoints Y = closedPoints X
have h : ∀ (x : X), x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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] {x}
have 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)})
Tactic: convert! (hs' x.2).preimage continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s.Finite
hs' : s ⊆ closedPoints X
⊢ IsDiscrete s
have this : T1Space.{u_1} (↑s : Type u_1)
Tactic: have : T1Space s := ⟨fun x ↦ by convert! (hs' x.2).preimage continuous_subtype_val; aesop⟩
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
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)
⊢ IsDiscrete s
have this₁ : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have : Finite s := hs
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ JacobsonSpace X ↔ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
have rw : (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) ↔
  ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Tactic: rw [jacobsonSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
have mp : (∀ {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
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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
⊢ (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
have mpr : (∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty) →
  ∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed[inst] Z → closure[inst] (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
have 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 ≠ ∅
Tactic: simp_rw [isLocallyClosed_iff_isOpen_coborder, coborder, isOpen_compl_iff,
      Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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
have refine : closure[inst] Z ⊆ closure[inst] Z \ Z
Tactic: refine subset_closure.trans ?_
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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 ⊆ closure[inst] Z \ Z
have nth_rw : closure[inst] (closure[inst] Z ∩ closedPoints X) ⊆ closure[inst] Z \ Z
Tactic: nth_rw 1 [← H isClosed_closure]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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] (closure[inst] Z ∩ closedPoints X) ⊆ closure[inst] Z \ Z
have rw : closure[inst] Z ∩ closedPoints X ⊆ closure[inst] Z ∧ closure[inst] Z ∩ ∅ ⊆ ∅
Tactic: rw [hZ'.closure_subset_iff, Set.subset_diff, Set.disjoint_iff, Set.inter_assoc,
        Set.inter_comm _ Z, e]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
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 = ∅
⊢ False
have this : 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⟩
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
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
have this₁ : Z ⊆ closure[inst] Z ∧ Z = ∅
Tactic: rw [Set.subset_diff, disjoint_self, Set.bot_eq_empty] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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
have mpr : Z ⊆ closure[inst] (Z ∩ closedPoints X)
Tactic: refine subset_antisymm (hZ.closure_subset_iff.mpr Set.inter_subset_left) ?_
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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
⊢ Z ⊆ closure[inst] (Z ∩ closedPoints X)
have mpr : ¬((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
Tactic: rw [← Set.disjoint_compl_left_iff_subset, Set.disjoint_iff_inter_eq_empty,
      ← Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
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
⊢ False
have this : ((closure[inst] (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty
Tactic: have := H _ H' (isClosed_closure.isOpen_compl.isLocallyClosed.inter hZ.isLocallyClosed)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
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
⊢ False
have this₁ : ¬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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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
have refine : closure[inst] S ⊆ closure[inst] (S ∩ closedPoints X)
Tactic: refine (closure_mono (Set.inter_subset_left)).antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
⊢ closure[inst] S ⊆ closure[inst] (S ∩ closedPoints X)
have rw : S ⊆ closure[inst] (S ∩ closedPoints X)
Tactic: rw [IsClosed.closure_subset_iff isClosed_closure]
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
x : X
hx : x ∈ S
⊢ x ∈ closure[inst] (S ∩ closedPoints X)
have by_contra : ∀ (H : x ∉ closure[inst] (S ∩ closedPoints X)), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (goal)
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)
⊢ False
have obtain : ∀ (y : X) (hy₃ : y ∈ closedPoints X) (hy₁ : y ∈ S) (hy₂ : y ∉ closure[inst] (S ∩ closedPoints X)), 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)
-- Lean 4 proof step from Mathlib.Topology.JacobsonSpace (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : JacobsonSpace X
x : X
hx : IsLocallyClosed (X := X) {x}
⊢ IsClosed[inst] {x}
have hy' : x ∈ closedPoints X
Tactic: obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
    nonempty_inter_closedPoints (Set.singleton_nonempty x) hx
-- 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
⊢ f ⁻¹' closedPoints Y = closedPoints X
have apply : closedPoints X ⊆ f ⁻¹' closedPoints Y
Tactic: apply subset_antisymm (preimage_closedPoints_subset hf.injective hf.continuous)
-- 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
⊢ x ∈ f ⁻¹' closedPoints Y
have hx₁ : IsLocallyClosed (X := Y) {f x}
Tactic: apply isClosed_singleton_of_isLocallyClosed_singleton