awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ Disjoint s (closure[inst] s \ s)

Tactic:
exact disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : s ⊆ closure[inst] s
⊢ coborder s ∩ closure[inst] s = s

Tactic:
rw [coborder, ← diff_eq_compl_inter, diff_diff_right_self, inter_eq_right]

Premises used: Set.diff_eq_compl_inter, Set.inter_eq_right, coborder, Set.diff_diff_right_self
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ closure[inst] s

Tactic:
subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ closure[inst] s

Tactic:
exact subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : coborder s ∩ closure[inst] s = s
rw₁ rw₂ : s = s
⊢ closure[inst] s ∩ coborder s = s

Tactic:
rw [inter_comm, coborder_inter_closure]

Premises used: coborder_inter_closure, Set.inter_comm
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : (closure[inst] s \ s)ᶜ = s ∪ (frontier s)ᶜ
rw₁ : (s ∪ (frontier s)ᶜ)ᶜ = closure[inst] s \ s
rw₂ : sᶜ ∩ (frontier s)ᶜᶜ = closure[inst] s \ s
rw₃ : sᶜ ∩ frontier s = closure[inst] s \ s
rw₄ : frontier s \ s = closure[inst] s \ s
rw₅ : (frontier s ∪ s) \ s = closure[inst] s \ s
rw₆ : (s ∪ frontier s) \ s = closure[inst] s \ s
rw₇ rw₈ : closure[inst] s \ s = closure[inst] s \ s
⊢ coborder s = s ∪ (frontier s)ᶜ

Tactic:
rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
    ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]

Premises used: Set.compl_union, compl_compl, Set.diff_eq_compl_inter, Set.union_comm, coborder, closure_eq_self_union_frontier, Set.union_diff_right, compl_eq_comm
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ coborder s = univ ↔ IsClosed[inst] s

Tactic:
simp [coborder, diff_eq_empty, closure_subset_iff_isClosed]

Premises used: closure_subset_iff_isClosed, coborder, Set.diff_eq_empty
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw : s ∪ (frontier s)ᶜ = (frontier s)ᶜ ↔ IsOpen[inst] s
simp_rw₁ : s ⊆ (frontier s)ᶜ ↔ IsOpen[inst] s
simp_rw₂ : Disjoint (frontier s) s ↔ IsOpen[inst] s
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen[inst] s

Tactic:
simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]

Premises used: coborder_eq_union_frontier_compl, disjoint_frontier_iff_isOpen, Set.subset_compl_iff_disjoint_left, Set.union_eq_right
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : closure[inst] s ∩ sᶜ = closure[inst] s \ s
⊢ coborder s = s ∪ (closure[inst] s)ᶜ

Tactic:
rw [coborder, compl_eq_comm, compl_union, compl_compl, inter_comm]

Premises used: Set.compl_union, compl_compl, Set.inter_comm, coborder, compl_eq_comm
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s ∩ sᶜ = closure[inst] s \ s

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : univ ⊆ closure[inst] s ∪ closure[inst] (closure[inst] s)ᶜ
⊢ Dense (coborder s)

Tactic:
rw [dense_iff_closure_eq, coborder_eq_union_closure_compl, closure_union, ← univ_subset_iff]

Premises used: Set.univ_subset_iff, dense_iff_closure_eq, closure_union, coborder_eq_union_closure_compl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure[inst] s ∪ closure[inst] (closure[inst] s)ᶜ

Tactic:
_root_.subset_trans ?_ (union_subset_union_right _ (subset_closure))

Premises used: subset_closure, subset_trans, Set.union_subset_union_right
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine : univ ⊆ closure[inst] s ∪ (closure[inst] s)ᶜ
⊢ univ ⊆ closure[inst] s ∪ closure[inst] (closure[inst] s)ᶜ

Tactic:
refine _root_.subset_trans ?_ (union_subset_union_right _ (subset_closure))

Premises used: subset_closure, subset_trans, Set.union_subset_union_right
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ univ ⊆ closure[inst] s ∪ (closure[inst] s)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
rw : f ⁻¹' closure[inst_1] s \ f ⁻¹' s ⊆ closure[inst] (f ⁻¹' s) \ f ⁻¹' s
⊢ coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s

Tactic:
rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]

Premises used: Set.compl_subset_compl, coborder, Set.preimage_compl, Set.preimage_diff
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
h : f ⁻¹' closure[inst_1] s ⊆ closure[inst] (f ⁻¹' s)
⊢ f ⁻¹' closure[inst_1] s \ f ⁻¹' s ⊆ closure[inst] (f ⁻¹' s) \ f ⁻¹' s

Tactic:
apply diff_subset_diff_left

Premises used: Set.diff_subset_diff_left
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst_1] s ⊆ closure[inst] (f ⁻¹' s)

Tactic:
hf.preimage_closure_subset_closure_preimage

Premises used: IsOpenMap.preimage_closure_subset_closure_preimage
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst_1] s ⊆ closure[inst] (f ⁻¹' s)

Tactic:
exact hf.preimage_closure_subset_closure_preimage

Premises used: IsOpenMap.preimage_closure_subset_closure_preimage
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set Y
rw : closure[inst] (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure[inst_1] s \ f ⁻¹' s
⊢ f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)

Tactic:
rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]

Premises used: Set.compl_subset_compl, coborder, Set.preimage_compl, Set.preimage_diff
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set Y
h : closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' closure[inst_1] s
⊢ closure[inst] (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure[inst_1] s \ f ⁻¹' s

Tactic:
apply diff_subset_diff_left

Premises used: Set.diff_subset_diff_left
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set Y
⊢ closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' closure[inst_1] s

Tactic:
hf.closure_preimage_subset s

Premises used: Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
s : Set Y
⊢ closure[inst] (f ⁻¹' s) ⊆ f ⁻¹' closure[inst_1] s

Tactic:
exact hf.closure_preimage_subset s

Premises used: Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenMap f
hf' : Continuous[inst, inst_1] f
s : Set Y
⊢ coborder (f ⁻¹' s) = f ⁻¹' coborder s

Tactic:
(hf.coborder_preimage_subset s).antisymm (hf'.preimage_coborder_subset s)

Premises used: HasSubset.Subset.antisymm, Continuous.preimage_coborder_subset, IsOpenMap.coborder_preimage_subset
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set Y
⊢ coborder (f ⁻¹' s) = f ⁻¹' coborder s

Tactic:
coborder_preimage hf.isOpenMap hf.continuous s

Premises used: Topology.IsOpenEmbedding.isOpenMap, coborder_preimage, Topology.IsOpenEmbedding.continuous
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : coborder s ∩ closure[inst] (coborder s ∩ s) ⊆ s
rw₁ : coborder s ∩ closure[inst] s ⊆ s
rw₂ rw₃ : s ⊆ s
⊢ IsClosed[instTopologicalSpaceSubtype] (coborder s ↓∩ s)

Tactic:
rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]

Premises used: Iff.mpr, coborder_inter_closure, Set.inter_eq_right, isClosed_preimage_val, subset_coborder
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyClosed s
ht : IsLocallyClosed t
obtain : ∀ (U₁ Z₁ : Set X) (hU₁ : IsOpen[inst] U₁) (hZ₁ : IsClosed[inst] Z₁), IsLocallyClosed (U₁ ∩ Z₁ ∩ t)
⊢ IsLocallyClosed (s ∩ t)

Tactic:
obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set X
ht : IsLocallyClosed t
U₁ Z₁ : Set X
hU₁ : IsOpen[inst] U₁
hZ₁ : IsClosed[inst] Z₁
obtain : ∀ (U₂ Z₂ : Set X) (hU₂ : IsOpen[inst] U₂) (hZ₂ : IsClosed[inst] Z₂), IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ t)

Tactic:
obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U₁ Z₁ : Set X
hU₁ : IsOpen[inst] U₁
hZ₁ : IsClosed[inst] Z₁
U₂ Z₂ : Set X
hU₂ : IsOpen[inst] U₂
hZ₂ : IsClosed[inst] Z₂
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))

Tactic:
⟨_, _, hU₁.inter hU₂, hZ₁.inter hZ₂, inter_inter_inter_comm U₁ Z₁ U₂ Z₂⟩

Premises used: Set.inter_inter_inter_comm, IsLocallyClosed, And.intro, IsOpen.inter, Exists.intro, IsClosed.inter
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U₁ Z₁ : Set X
hU₁ : IsOpen[inst] U₁
hZ₁ : IsClosed[inst] Z₁
U₂ Z₂ : Set X
hU₂ : IsOpen[inst] U₂
hZ₂ : IsClosed[inst] Z₂
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))

Tactic:
refine ⟨_, _, hU₁.inter hU₂, hZ₁.inter hZ₂, inter_inter_inter_comm U₁ Z₁ U₂ Z₂⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
hs : IsLocallyClosed s
f : X → Y
hf : Continuous[inst, inst_1] f
obtain : ∀ (U Z : Set Y) (hU : IsOpen[inst_1] U) (hZ : IsClosed[inst_1] Z), IsLocallyClosed (f ⁻¹' (U ∩ Z))
⊢ IsLocallyClosed (f ⁻¹' s)

Tactic:
obtain ⟨U, Z, hU, hZ, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
⊢ IsLocallyClosed (f ⁻¹' (U ∩ Z))

Tactic:
⟨_, _, hU.preimage hf, hZ.preimage hf, preimage_inter⟩

Premises used: Set.preimage_inter, IsLocallyClosed, And.intro, Exists.intro, IsClosed.preimage, IsOpen.preimage
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
⊢ IsLocallyClosed (f ⁻¹' (U ∩ Z))

Tactic:
exact ⟨_, _, hU.preimage hf, hZ.preimage hf, preimage_inter⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
simp_rw :
  (∃ (U : Set X) (Z : Set X),
      (∃ (t : Set Y), IsOpen[inst_1] t ∧ f ⁻¹' t = U) ∧ (∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔
    ∃ (s' : Set Y), (∃ (U : Set Y) (Z : Set Y), IsOpen[inst_1] U ∧ IsClosed[inst_1] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s
⊢ IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ f ⁻¹' s' = s

Tactic:
simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]

Premises used: Topology.IsInducing.isOpen_iff, IsLocallyClosed, Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
mp :
  (∃ (U : Set X) (Z : Set X),
      (∃ (t : Set Y), IsOpen[inst_1] t ∧ f ⁻¹' t = U) ∧ (∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) →
    ∃ (s' : Set Y), (∃ (U : Set Y) (Z : Set Y), IsOpen[inst_1] U ∧ IsClosed[inst_1] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s
mpr :
  (∃ (s' : Set Y), (∃ (U : Set Y) (Z : Set Y), IsOpen[inst_1] U ∧ IsClosed[inst_1] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ (U : Set X) (Z : Set X),
      (∃ (t : Set Y), IsOpen[inst_1] t ∧ f ⁻¹' t = U) ∧ (∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z
⊢ (∃ (U : Set X) (Z : Set X),
      (∃ (t : Set Y), IsOpen[inst_1] t ∧ f ⁻¹' t = U) ∧ (∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) ↔
    ∃ (s' : Set Y), (∃ (U : Set Y) (Z : Set Y), IsOpen[inst_1] U ∧ IsClosed[inst_1] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

Tactic:
constructor
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U : Set Y
hU : IsOpen[inst_1] U
Z : Set Y
hZ : IsClosed[inst_1] Z
⊢ ∃ (s' : Set Y),
    (∃ (U : Set Y) (Z : Set Y), IsOpen[inst_1] U ∧ IsClosed[inst_1] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = f ⁻¹' U ∩ f ⁻¹' Z

Tactic:
⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U : Set Y
hU : IsOpen[inst_1] U
Z : Set Y
hZ : IsClosed[inst_1] Z
⊢ ∃ (s' : Set Y),
    (∃ (U : Set Y) (Z : Set Y), IsOpen[inst_1] U ∧ IsClosed[inst_1] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = f ⁻¹' U ∩ f ⁻¹' Z

Tactic:
exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
⊢ ∃ (U_1 : Set X) (Z_1 : Set X),
    (∃ (t : Set Y), IsOpen[inst_1] t ∧ f ⁻¹' t = U_1) ∧
      (∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = Z_1) ∧ f ⁻¹' (U ∩ Z) = U_1 ∩ Z_1

Tactic:
⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
⊢ ∃ (U_1 : Set X) (Z_1 : Set X),
    (∃ (t : Set Y), IsOpen[inst_1] t ∧ f ⁻¹' t = U_1) ∧
      (∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = Z_1) ∧ f ⁻¹' (U ∩ Z) = U_1 ∩ Z_1

Tactic:
exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsEmbedding f
simp_rw :
  (∃ (s' : Set Y), IsLocallyClosed s' ∧ f ⁻¹' s' = s) ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ s' ∩ range f = f '' s
simp_rw₁ :
  (∃ (s' : Set Y), IsLocallyClosed s' ∧ f '' f ⁻¹' s' = f '' s) ↔
    ∃ (s' : Set Y), IsLocallyClosed s' ∧ s' ∩ range f = f '' s
⊢ IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ s' ∩ range f = f '' s

Tactic:
simp_rw [hf.isInducing.isLocallyClosed_iff,
    ← (image_injective.mpr hf.injective).eq_iff, image_preimage_eq_inter_range]

Premises used: Iff.mpr, Topology.IsInducing.isLocallyClosed_iff, Set.image_injective, Function.Injective.eq_iff, Set.image_preimage_eq_inter_range, Topology.IsEmbedding.isInducing, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
hs : IsLocallyClosed s
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
obtain : ∀ (t : Set Y) (ht : IsLocallyClosed t) (hs : IsLocallyClosed (f ⁻¹' t)), IsLocallyClosed (f '' f ⁻¹' t)
⊢ IsLocallyClosed (f '' s)

Tactic:
obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs

Premises used: Topology.IsInducing.isLocallyClosed_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
rw : IsLocallyClosed (t ∩ range f)
⊢ IsLocallyClosed (f '' f ⁻¹' t)

Tactic:
rw [image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (t ∩ range f)

Tactic:
ht.inter hf'

Premises used: IsLocallyClosed.inter
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
t : Set Y
ht : IsLocallyClosed t
hs : IsLocallyClosed (f ⁻¹' t)
⊢ IsLocallyClosed (t ∩ range f)

Tactic:
exact ht.inter hf'

Premises used: IsLocallyClosed.inter
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsLocallyClosed s

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsOpen[inst] (coborder s)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
nth_rw : closure[inst] Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ Z ∪ (frontier (U ∩ Z))ᶜ = univ

Tactic:
nth_rw 1 [← hZ.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
rw : frontier (U ∩ Z) ⊆ closure[inst] Z
⊢ closure[inst] Z ∪ (frontier (U ∩ Z))ᶜ = univ

Tactic:
rw [← compl_subset_iff_union, compl_subset_compl]

Premises used: Set.compl_subset_compl, Set.compl_subset_iff_union
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
⊢ frontier (U ∩ Z) ⊆ closure[inst] Z

Tactic:
frontier_subset_closure.trans (closure_mono inter_subset_right)

Premises used: HasSubset.Subset.trans, closure_mono, frontier_subset_closure, Set.inter_subset_right
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
⊢ frontier (U ∩ Z) ⊆ closure[inst] Z

Tactic:
refine frontier_subset_closure.trans (closure_mono inter_subset_right)

Premises used: HasSubset.Subset.trans, closure_mono, frontier_subset_closure, Set.inter_subset_right
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
⊢ Z ∪ (frontier (U ∩ Z))ᶜ = univ

Tactic:
have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
      nth_rw 1 [← hZ.closure_eq]
      rw [← compl_subset_iff_union, compl_subset_compl]
      refine frontier_subset_closure.trans (closure_mono inter_subset_right)
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
rw : IsOpen[inst] (U ∪ (frontier (U ∩ Z))ᶜ)
⊢ IsOpen[inst] (coborder (U ∩ Z))

Tactic:
rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
      inter_univ]

Premises used: Set.inter_univ, Set.inter_union_distrib_right, coborder_eq_union_frontier_compl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen[inst] (U ∪ (frontier (U ∩ Z))ᶜ)

Tactic:
hU.union isClosed_frontier.isOpen_compl

Premises used: IsClosed.isOpen_compl, IsOpen.union
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen[inst] (U ∪ (frontier (U ∩ Z))ᶜ)

Tactic:
exact hU.union isClosed_frontier.isOpen_compl

Premises used: IsClosed.isOpen_compl, IsOpen.union
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)

Tactic:
tfae_have 1 → 2 := by
    rintro ⟨U, Z, hU, hZ, rfl⟩
    have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
      nth_rw 1 [← hZ.closure_eq]
      rw [← compl_subset_iff_union, compl_subset_compl]
      refine frontier_subset_closure.trans (closure_mono inter_subset_right)
    rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
      inter_univ]
    exact hU.union isClosed_frontier.isOpen_compl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
⊢ IsOpen[inst] (coborder s)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
⊢ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
⊢ ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
⊢ ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)

Tactic:
tfae_have 2 → 3
  | h, x => (⟨coborder s, h.mem_nhds <| subset_coborder ·, isClosed_preimage_val_coborder⟩)
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
⊢ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
⊢ ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false