awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
h :
  ∀ (i : ι) (hi : i ∈ t) (hxi : x ∈ (U i).carrier),
    Membership.mem (γ := Set X) (⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)) x
⊢ Membership.mem (γ := Set X) (⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)) x

Tactic:
obtain ⟨i, hi, hxi⟩ := Set.mem_iUnion₂.mp (ht hx₁)

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
i : ι
hi : i ∈ t
hxi : x ∈ (U i).carrier
⊢ x ∈ (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)

Tactic:
simpa [*]
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
i : ι
hi : i ∈ t
hxi : x ∈ (U i).carrier
⊢ Membership.mem (γ := Set X) (⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)) x

Tactic:
exact Set.mem_iUnion₂.mpr ⟨i, hi, by simpa [*]⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact (↑(U i) : Set X)
h₂ : ∀ (i : ι), IsQuasiSeparated (↑(U i) : Set X)
V₁ V₂ : Set X
ho₁ : IsOpen[inst] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂) ⊆ V₁ ∩ V₂

Tactic:
aesop (add simp Set.subset_def)

Premises used: Set.subset_def
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
inst_1 : CompactSpace X
hs : IsRetrocompact s
⊢ IsCompact s

Tactic:
simpa using hs CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
U : Set X
inst_1 : QuasiSeparatedSpace X
hU' : IsCompact U
hU : IsOpen[inst] U
⊢ IsRetrocompact U

Tactic:
fun _ hV' hV ↦ hU'.inter_of_isOpen hV' hU hV

Premises used: IsRetrocompact, IsCompact.inter_of_isOpen
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
U : Set X
inst_1 : QuasiSeparatedSpace X
hU' : IsCompact U
hU : IsOpen[inst] U
⊢ IsConstructible U

Tactic:
(hU'.isRetrocompact hU).isConstructible hU

Premises used: IsCompact.isRetrocompact, IsRetrocompact.isConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
U : Set X
inst_1 : CompactSpace X
inst_2 : QuasiSeparatedSpace X
hU : IsOpen[inst] U
⊢ IsRetrocompact U ↔ IsCompact U

Tactic:
⟨IsRetrocompact.isCompact, (IsCompact.isRetrocompact · hU)⟩

Premises used: IsCompact.isRetrocompact, IsRetrocompact.isCompact, Iff.intro
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsConstructible s
x : X
⊢ univ ∈ 𝓝 x

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsConstructible s
x : X
⊢ IsOpen[inst] univ

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsConstructible s
x : X
⊢ IsRetrocompact.{u_2} (X := X)
    (range (ι := { x : X // Membership.mem (γ := Set X) univ x })
      (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) univ x)))

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
hs : IsConstructible s
x : X
⊢ s ⊆
    range (ι := { x : X // Membership.mem (γ := Set X) univ x })
      (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) univ x))

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsLocallyConstructible U

Tactic:
(hUcomp.isConstructible hUopen).isLocallyConstructible

Premises used: Topology.IsConstructible.isLocallyConstructible, IsRetrocompact.isConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ IsLocallyConstructible.{u_2} (X := X) ∅

Tactic:
IsConstructible.empty.isLocallyConstructible

Premises used: Topology.IsConstructible.empty, Topology.IsConstructible.isLocallyConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ IsLocallyConstructible.{u_2} (X := X) univ

Tactic:
IsConstructible.univ.isLocallyConstructible

Premises used: Topology.IsConstructible.isLocallyConstructible, Topology.IsConstructible.univ
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
obtain :
  ∀ (U : Set X) (hxU : U ∈ 𝓝 x) (hU : IsOpen[inst] U) (hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)),
    ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)

Tactic:
obtain ⟨U, hxU, hU, hsU⟩ := hs x
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
obtain :
  ∀ (V : Set X) (hxV : V ∈ 𝓝 x) (hV : IsOpen[inst] V) (htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)),
    ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)

Tactic:
obtain ⟨V, hxV, hV, htV⟩ := ht x
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)

Tactic:
⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩

Premises used: Filter.inter_mem, Inter.inter, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
refine : IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ s ∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s ∩ t)

Tactic:
refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
change :
  IsConstructible (X := (↑(U ∩ V) : Type u_2))
    ((inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s) ∩ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ s ∩ t)

Tactic:
change IsConstructible
    (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t))

Premises used: Set.inter_subset_left, Inter.inter, Set.preimage, Set.inclusion, Topology.IsConstructible, Subtype.val, Set.inter_subset_right
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2))
    ((inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s) ∩ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)

Tactic:
.inter (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)

Premises used: continuous_subtype_val, Topology.IsConstructible.preimage_of_isOpenEmbedding, Topology.IsConstructible.inter, IsOpen.inter, Topology.IsOpenEmbedding.inclusion, IsOpen.preimage
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2))
    ((inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s) ∩ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)

Tactic:
exact .inter (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (Finset.inf ∅ t)

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsLocallyConstructible (t i)), IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
cons : IsLocallyConstructible (t i ⊓ s.inf t)
⊢ IsLocallyConstructible ((Finset.cons i s ih).inf t)

Tactic:
rw [Finset.inf_cons]

Premises used: Finset.inf_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsLocallyConstructible (t i)), IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : ∀ (ht : ∀ i ∈ s, IsLocallyConstructible (t i)), IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible (t i ⊓ s.inf t)

Tactic:
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Premises used: Topology.IsLocallyConstructible.inter, Finset.forall_of_forall_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
empty :
  ∀ (ht : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsLocallyConstructible (t i)),
    IsLocallyConstructible (Finset.inf ∅ t)
cons :
  ∀ (i : ι) (s : Finset ι) (ih : i ∉ s)
    (hi : ∀ (ht : ∀ i ∈ s, IsLocallyConstructible (t i)), IsLocallyConstructible (s.inf t))
    (ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)),
    IsLocallyConstructible ((Finset.cons i s ih).inf t)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Premises used: Topology.IsLocallyConstructible.inter, Finset.forall_of_forall_cons, Finset.inf_cons
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
rw : IsLocallyConstructible (s.inf t)
⊢ IsLocallyConstructible (s.inf' hs t)

Tactic:
rw [Finset.inf'_eq_inf]

Premises used: Finset.inf'_eq_inf
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
.finsetInf ht

Premises used: Topology.IsLocallyConstructible.finsetInf
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
exact .finsetInf ht
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ InfClosed.{u_2} (α := Set X) {s : Set X | IsLocallyConstructible s}

Tactic:
fun _s hs _t ht ↦ hs.inter ht

Premises used: Topology.IsLocallyConstructible.inter, Set.Mem, setOf, Topology.IsLocallyConstructible, InfClosed
-- Module: Mathlib.Topology.Constructible
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Finite ι
f : ι → Set X
hf : ∀ (i : ι), IsLocallyConstructible (f i)
⊢ IsLocallyConstructible.{u_2} (X := X) (⋂ (i : ι), f i)

Tactic:
infClosed_isLocallyConstructible.iInf_mem .univ hf

Premises used: Set.Mem, Set.iInter, Topology.IsLocallyConstructible.univ, setOf, Topology.IsLocallyConstructible, InfClosed.iInf_mem, _private.0.Topology.infClosed_isLocallyConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
hS' : ∀ s ∈ S, IsLocallyConstructible s
⊢ IsLocallyConstructible (⋂₀ S)

Tactic:
infClosed_isLocallyConstructible.sInf_mem hS .univ hS'

Premises used: Set.Mem, Topology.IsLocallyConstructible.univ, setOf, Topology.IsLocallyConstructible, _private.0.Topology.infClosed_isLocallyConstructible, Set.sInter, InfClosed.sInf_mem
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
obtain :
  ∀ (U : Set X) (hxU : U ∈ 𝓝 x) (hU : IsOpen[inst] U) (hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)),
    ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))

Tactic:
obtain ⟨U, hxU, hU, hsU⟩ := hs x
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
obtain :
  ∀ (V : Set X) (hxV : V ∈ 𝓝 x) (hV : IsOpen[inst] V) (htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)),
    ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))

Tactic:
obtain ⟨V, hxV, hV, htV⟩ := ht x
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))

Tactic:
⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩

Premises used: Filter.inter_mem, Inter.inter, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
refine : IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ (s ∪ t))

Tactic:
refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
h :
  ∀ (x : (↑(U ∩ V) : Type u_2)),
    Membership.mem (γ := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t)) x ↔
      Membership.mem (γ := Set (↑(U ∩ V) : Type u_2))
        (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t) x
⊢ Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)

Tactic:
ext
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
x_1 : (↑(U ∩ V) : Type u_2)
⊢ Membership.mem (γ := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t)) x_1 ↔
    Membership.mem (γ := Set (↑(U ∩ V) : Type u_2))
      (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t) x_1

Tactic:
simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
⊢ Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)

Tactic:
have : (U ∩ V) ↓∩ (s ∪ t) =
      inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∪ inclusion inter_subset_right ⁻¹' (V ↓∩ t) := by
    ext; simp
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
this :
  Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
rw :
  IsConstructible (X := (↑(U ∩ V) : Type u_2))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))

Tactic:
rw [this]
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
this :
  Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)

Tactic:
.union (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)

Premises used: Topology.IsConstructible.union, continuous_subtype_val, Topology.IsConstructible.preimage_of_isOpenEmbedding, IsOpen.inter, Topology.IsOpenEmbedding.inclusion, IsOpen.preimage
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hsU : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst] V
htV : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ t)
this :
  Eq (α := Set (↑(U ∩ V) : Type u_2)) ((U ∩ V) ↓∩ (s ∪ t))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)
⊢ IsConstructible (X := (↑(U ∩ V) : Type u_2))
    (inclusion (s := U ∩ V) (t := U) ⋯ ⁻¹' U ↓∩ s ∪ inclusion (s := U ∩ V) (t := V) ⋯ ⁻¹' V ↓∩ t)

Tactic:
exact .union (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
    (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
      .preimage continuous_subtype_val <| hU.inter hV)
-- Module: Mathlib.Topology.Constructible
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Finite ι
f : ι → Set X
hf : ∀ (i : ι), IsLocallyConstructible (f i)
⊢ IsLocallyConstructible.{u_2} (X := X) (⋃ (i : ι), f i)

Tactic:
SupClosed.iSup_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.union) .empty hf

Premises used: Set.Mem, SupClosed.iSup_mem, setOf, Topology.IsLocallyConstructible.empty, Topology.IsLocallyConstructible.union, Topology.IsLocallyConstructible, Set.iUnion
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_4
f : ι → Set X
s : Set ι
hs : s.Finite
hf : ∀ i ∈ s, IsLocallyConstructible (f i)
⊢ IsLocallyConstructible.{u_2} (X := X) (⋃ i ∈ s, f i)

Tactic:
SupClosed.biSup_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.union) hs .empty hf

Premises used: Set.Mem, setOf, Topology.IsLocallyConstructible.empty, Topology.IsLocallyConstructible.union, SupClosed.biSup_mem, Topology.IsLocallyConstructible, Set.iUnion
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
hS' : ∀ s ∈ S, IsLocallyConstructible s
⊢ IsLocallyConstructible (⋃₀ S)

Tactic:
SupClosed.sSup_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.union) hS .empty hS'

Premises used: Set.Mem, setOf, Set.sUnion, Topology.IsLocallyConstructible.empty, Topology.IsLocallyConstructible.union, SupClosed.sSup_mem, Topology.IsLocallyConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsLocallyConstructible s
hf : IsOpenEmbedding f
x : X
obtain :
  ∀ (U : Set Y) (hxU : U ∈ 𝓝 (f x)) (hU : IsOpen[inst_1] U) (H : IsConstructible (X := (↑U : Type u_3)) (U ↓∩ s)),
    ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ f ⁻¹' s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ f ⁻¹' s)

Tactic:
obtain ⟨U, hxU, hU, H⟩ := hs (f x)