awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[instTopologicalSpaceSubtype] (coborder s ↓∩ s)
have rw : coborder s ∩ closure[inst] (coborder s ∩ s) ⊆ s
Tactic: rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : coborder s ∩ closure[inst] (coborder s ∩ s) ⊆ s
⊢ IsClosed[instTopologicalSpaceSubtype] (coborder s ↓∩ s)
have rw₁ : coborder s ∩ closure[inst] s ⊆ s
Tactic: rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ IsClosed[instTopologicalSpaceSubtype] (coborder s ↓∩ s)
have rw₂ : s ⊆ s
Tactic: rw [isClosed_preimage_val, inter_eq_right.mpr subset_coborder, coborder_inter_closure]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyClosed s
ht : IsLocallyClosed t
⊢ IsLocallyClosed (s ∩ t)
have obtain : ∀ (U₁ Z₁ : Set X) (hU₁ : IsOpen[inst] U₁) (hZ₁ : IsClosed[inst] Z₁), IsLocallyClosed (U₁ ∩ Z₁ ∩ t)
Tactic: obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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₁
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ t)
have obtain : ∀ (U₂ Z₂ : Set X) (hU₂ : IsOpen[inst] U₂) (hZ₂ : IsClosed[inst] Z₂), IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))
Tactic: obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ IsLocallyClosed (f ⁻¹' s)
have obtain : ∀ (U Z : Set Y) (hU : IsOpen[inst_1] U) (hZ : IsClosed[inst_1] Z), IsLocallyClosed (f ⁻¹' (U ∩ Z))
Tactic: obtain ⟨U, Z, hU, hZ, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ f ⁻¹' s' = s
have 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
Tactic: simp_rw [IsLocallyClosed, hf.isOpen_iff, hf.isClosed_iff]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ s' ∩ range f = f '' s
have simp_rw : (∃ (s' : Set Y), IsLocallyClosed s' ∧ f ⁻¹' s' = 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]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
⊢ IsLocallyClosed s ↔ ∃ (s' : Set Y), IsLocallyClosed s' ∧ s' ∩ range f = f '' s
have simp_rw₁ : (∃ (s' : Set Y), IsLocallyClosed s' ∧ f '' f ⁻¹' s' = f '' 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]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
⊢ IsLocallyClosed (f '' s)
have obtain : ∀ (t : Set Y) (ht : IsLocallyClosed t) (hs : IsLocallyClosed (f ⁻¹' t)), IsLocallyClosed (f '' f ⁻¹' t)
Tactic: obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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 (f '' f ⁻¹' t)
have rw : IsLocallyClosed (t ∩ range f)
Tactic: rw [image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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
have nth_rw : closure[inst] Z ∪ (frontier (U ∩ Z))ᶜ = univ
Tactic: nth_rw 1 [← hZ.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
⊢ closure[inst] Z ∪ (frontier (U ∩ Z))ᶜ = univ
have rw : frontier (U ∩ Z) ⊆ closure[inst] Z
Tactic: rw [← compl_subset_iff_union, compl_subset_compl]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
U Z : Set X
hU : IsOpen[inst] U
hZ : IsClosed[inst] Z
⊢ IsOpen[inst] (coborder (U ∩ Z))
have this : 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)
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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] (coborder (U ∩ Z))
have rw : IsOpen[inst] (U ∪ (frontier (U ∩ Z))ᶜ)
Tactic: rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
      inter_univ]
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ [IsLocallyClosed s, 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,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)].TFAE
have tfae_1_to_2 : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
⊢ [IsLocallyClosed s, 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,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)].TFAE
have tfae_2_to_3 : ∀ (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⟩)
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
have obtain : ∀ (t : Set X) (ht : t ∈ 𝓝 x) (ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)),
  ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
Tactic: obtain ⟨t, ht, ht'⟩ := h x hx
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
have obtain : ∀ (U : Set X) (hUt : U ⊆ t) (hU : IsOpen[inst] U) (hxU : x ∈ U),
  ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
Tactic: obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst] U
hxU : x ∈ U
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
have rw : ∀ (ht' : t ∩ closure[inst] (t ∩ s) ⊆ s) (U : Set X) (hUt : U ⊆ t) (hU : IsOpen[inst] U) (hxU : x ∈ U),
  ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
Tactic: rw [isClosed_preimage_val] at ht'
Cleared hypotheses: ht', U, hUt, hU, hxU
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (hypothesis)
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)
⊢ [IsLocallyClosed s, 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,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)].TFAE
have tfae_3_to_4 : ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
  ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
Tactic: tfae_have 3 → 4
  | h, x, hx => by
    obtain ⟨t, ht, ht'⟩ := h x hx
    obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
    rw [isClosed_preimage_val] at ht'
    exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
H : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s := h
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
have choose : ∀ (U : (x : X) → x ∈ s → Set X) (hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a)
  (hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)) (e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s),
  IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
Tactic: choose U hxU hU e using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
have refine_1 : ∀ (x : { x : X // x ∈ closure[inst] s }),
  Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
      (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x →
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x
Tactic: refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
refine_1 :
  ∀ (x : { x : X // x ∈ closure[inst] s }),
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
        (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x →
      Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
have refine_2 : ∀ (x : { x : X // x ∈ closure[inst] s }),
  Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x →
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
      (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x
Tactic: refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (hypothesis)
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)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ [IsLocallyClosed s, 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,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)].TFAE
have tfae_4_to_5 : ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
  IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
Tactic: tfae_have 4 → 5
  | H => by
    choose U hxU hU e using H
    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩
    · exact (subset_iUnion₂ _ _ <| hxU x ·)
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (goal)
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)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
h : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s) := h
⊢ IsLocallyClosed s
have h : s = ↑(closure[inst] s ↓∩ s)
Tactic: convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)
-- Lean 4 proof step from Mathlib.Topology.LocallyClosed (hypothesis)
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)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
⊢ [IsLocallyClosed s, 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,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)].TFAE
have tfae_5_to_1 : ∀ (a : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)), IsLocallyClosed s
Tactic: tfae_have 5 → 1
  | H => by
    convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)
    simpa using subset_closure
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Algebra (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
⊢ HMul.hMul (α := LocallyConstant X Y)
      ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x =
    HMul.hMul (β := LocallyConstant X Y) x
      ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y)
have h : ∀ (x_1 : X),
  Eq.{u_2 + 1} (α := Y)
    ((HMul.hMul (α := LocallyConstant X Y)
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
          (a : X) → Y)
        x_1 :
      Y)
    ((HMul.hMul (β := LocallyConstant X Y) x
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) :
          (a : X) → Y)
        x_1 :
      Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Algebra (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
⊢ r • x =
    HMul.hMul (α := LocallyConstant X Y)
      ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x
have h : ∀ (x_1 : X),
  Eq.{u_2 + 1} (α := Y) ((r • x : (a : X) → Y) x_1 : Y)
    ((HMul.hMul (α := LocallyConstant X Y)
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
          (a : X) → Y)
        x_1 :
      Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x},
      ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
have tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
Tactic: tfae_have 1 → 4 := fun h y => h {y}
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x},
      ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
have tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
Tactic: tfae_have 4 → 3 := fun h x => h (f x)
-- Lean 4 proof step from Mathlib.Topology.LocallyConstant.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x},
      ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y}), ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
have tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
Tactic: tfae_have 3 → 2 := fun h x => IsOpen.mem_nhds (h x) rfl