awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
⟨f ⁻¹' U, hf.continuous.continuousAt.preimage_mem_nhds hxU, hU.preimage hf.continuous,
    (H.preimage_of_isOpenEmbedding (hf.restrictPreimage _) :)⟩

Premises used: ContinuousAt.preimage_mem_nhds, Topology.IsConstructible.preimage_of_isOpenEmbedding, Topology.IsOpenEmbedding.continuous, Topology.IsOpenEmbedding.restrictPreimage, Continuous.continuousAt, Set.preimage, And.intro, Exists.intro, IsOpen.preimage
-- 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
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)

Tactic:
exact ⟨f ⁻¹' U, hf.continuous.continuousAt.preimage_mem_nhds hxU, hU.preimage hf.continuous,
    (H.preimage_of_isOpenEmbedding (hf.restrictPreimage _) :)⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hUs : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ s)
⊢ IsRetrocompact.{u_2} (X := X) (range (ι := { x : X // x ∈ V }) (Subtype.val (p := fun (x : X) ↦ x ∈ V)))

Tactic:
simpa using hV₂.isRetrocompact hV₁

Premises used: IsCompact.isRetrocompact
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hUs : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ s)
⊢ IsConstructible (image (α := { x : X // x ∈ V }) (Subtype.val (p := fun (x : X) ↦ x ∈ V)) (V ↓∩ s))

Tactic:
have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal
        (by simpa using hV₂.isRetrocompact hV₁)
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst] U
hUs : IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this_1 : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ s)
this : IsConstructible (image (α := { x : X // x ∈ V }) (Subtype.val (p := fun (x : X) ↦ x ∈ V)) (V ↓∩ s))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : IsConstructible (V ∩ s)), IsConstructible (V ∩ s)
⊢ IsConstructible (V ∩ s)

Tactic:
rwa [Subtype.image_preimage_coe] at this

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
⊢ ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s)

Tactic:
have (x : _) : ∃ U, IsOpen U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s) :=
    have ⟨U, hxU, hU, hUs⟩ := hs x
    have ⟨V, ⟨hV₁, hV₂⟩, hxV, hVU⟩ := PrespectralSpace.isTopologicalBasis.mem_nhds_iff.mp hxU
    have : IsConstructible (V ↓∩ s) :=
      (hUs.preimage_of_isOpenEmbedding (IsOpenEmbedding.id.restrict hVU hV₁) :)
    have : IsConstructible (V ∩ s) := by
      have := this.image_of_isOpenEmbedding hV₁.isOpenEmbedding_subtypeVal
        (by simpa using hV₂.isRetrocompact hV₁)
      rwa [Subtype.image_preimage_coe] at this
    ⟨V, hV₁, hV₂, hxV, this⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
this : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s)
choose :
  ∀ (U : (x : X) → Set X) (hU : ∀ (x : X), IsOpen[inst] (U x)) (hU' : ∀ (x : X), IsCompact (U x))
    (hxU : ∀ (x : X), x ∈ U x) (hUs : ∀ (x : X), IsConstructible (U x ∩ s)), IsConstructible s
⊢ IsConstructible s

Tactic:
choose U hU hU' hxU hUs using this
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
obtain : ∀ (σ : Finset X) (hσ : ∀ x ∈ σ, x ∈ t) (htσ : t ⊆ ⋃ x ∈ σ, U x), IsConstructible s
⊢ IsConstructible s

Tactic:
obtain ⟨σ, hσ, htσ⟩ := ht.elim_nhds_subcover U (fun x _ ↦ (hU x).mem_nhds (hxU x))

Premises used: IsCompact.elim_nhds_subcover, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ IsConstructible.{u_2} (X := X) (⋃ i ∈ (↑σ : Set X), U i ∩ s)

Tactic:
IsConstructible.biUnion σ.finite_toSet (fun x _ ↦ hUs x)

Premises used: Topology.IsConstructible.biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
h : s = ⋃ i ∈ (↑σ : Set X), U i ∩ s
⊢ IsConstructible s

Tactic:
convert! IsConstructible.biUnion σ.finite_toSet (fun x _ ↦ hUs x)

Premises used: Topology.IsConstructible.biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
h : s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∩ s
h₁ : ⋃ i ∈ (↑σ : Set X), U i ∩ s ⊆ s
⊢ s = ⋃ i ∈ (↑σ : Set X), U i ∩ s

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
h : s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∧ s ⊆ s
⊢ s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∩ s

Tactic:
rw [← Set.iUnion₂_inter, Set.subset_inter_iff]

Premises used: Set.subset_inter_iff, Set.iUnion₂_inter
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∧ s ⊆ s

Tactic:
⟨hst.trans htσ, subset_rfl⟩

Premises used: HasSubset.Subset.trans, And.intro, subset_rfl
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ s ⊆ ⋃ i ∈ (↑σ : Set X), U i ∧ s ⊆ s

Tactic:
exact ⟨hst.trans htσ, subset_rfl⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ ⋃ i ∈ (↑σ : Set X), U i ∩ s ⊆ s

Tactic:
Set.iUnion₂_subset fun _ _ ↦ Set.inter_subset_right

Premises used: Set.iUnion₂_subset, Set.inter_subset_right
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : (x : X) → Set X
hU : ∀ (x : X), IsOpen[inst] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
σ : Finset X
hσ : ∀ x ∈ σ, x ∈ t
htσ : t ⊆ ⋃ x ∈ σ, U x
⊢ ⋃ i ∈ (↑σ : Set X), U i ∩ s ⊆ s

Tactic:
exact Set.iUnion₂_subset fun _ _ ↦ Set.inter_subset_right

Premises used: Set.iUnion₂_subset, Set.inter_subset_right
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
inst_3 : CompactSpace X
hs : IsLocallyConstructible s
⊢ IsConstructible s

Tactic:
hs.isConstructible_of_subset_of_isCompact s.subset_univ isCompact_univ

Premises used: Set.subset_univ, Topology.IsLocallyConstructible.isConstructible_of_subset_of_isCompact, isCompact_univ
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
ht : IsOpen[inst] t
ht' : IsCompact t
⊢ IsConstructible (s ∩ t)

Tactic:
(hs.inter (ht'.isConstructible ht).isLocallyConstructible).isConstructible_of_subset_of_isCompact
    Set.inter_subset_right ht'

Premises used: Topology.IsLocallyConstructible.inter, Topology.IsConstructible.isLocallyConstructible, IsCompact.isConstructible, Topology.IsLocallyConstructible.isConstructible_of_subset_of_isCompact, Set.inter_subset_right
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
have : ∀ (i : ι) (hi : x ∈ U i), ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)

Tactic:
have ⟨i, hi⟩ := hU.exists_mem x
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
have :
  ∀ (V : Set (↑(↑(U i) : Set X) : Type u_2)) (hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi))
    (hV : IsOpen[instTopologicalSpaceSubtype] V)
    (hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)),
    ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)

Tactic:
have ⟨V, hVx, hV, hV'⟩ := H i ⟨x, hi⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)

Tactic:
⟨_, (U i).2.isOpenEmbedding_subtypeVal.image_mem_nhds.mpr hVx,
      (U i).2.isOpenMap_subtype_val _ hV, ?_⟩

Premises used: Iff.mpr, IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.image_mem_nhds, And.intro, Exists.intro, TopologicalSpace.Opens.is_open', IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
refine :
  IsConstructible (X := (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
    ((Subtype.val '' V) ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen[inst] U ∧ IsConstructible (X := (↑U : Type u_2)) (U ↓∩ s)

Tactic:
refine ⟨_, (U i).2.isOpenEmbedding_subtypeVal.image_mem_nhds.mpr hVx,
      (U i).2.isOpenMap_subtype_val _ hV, ?_⟩
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
⊢ MapsTo (Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier)) V ↑V

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
e : (↑V : Type u_2) ≃ₜ (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) :=
  (Equiv.Set.image (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X))) V ⋯).toHomeomorphOfIsInducing ⋯
⊢ IsConstructible (X := (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2))
    (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
      (V ↓∩ (↑(U i) : Set X) ↓∩ s))

Tactic:
hV'.preimage_of_isOpenEmbedding e.symm.isOpenEmbedding

Premises used: Topology.IsConstructible.preimage_of_isOpenEmbedding, Homeomorph.symm, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
e : (↑V : Type u_2) ≃ₜ (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) :=
  (Equiv.Set.image (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X))) V ⋯).toHomeomorphOfIsInducing ⋯
h :
  (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2) =
      (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) →
    Eq (α := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2)) ((Subtype.val '' V) ↓∩ s)
      (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
        (V ↓∩ (↑(U i) : Set X) ↓∩ s))
⊢ IsConstructible (X := (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
    ((Subtype.val '' V) ↓∩ s)

Tactic:
convert! hV'.preimage_of_isOpenEmbedding e.symm.isOpenEmbedding

Premises used: Topology.IsConstructible.preimage_of_isOpenEmbedding, Homeomorph.symm, Homeomorph.isOpenEmbedding
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x : X
i : ι
hi : x ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
e : (↑V : Type u_2) ≃ₜ (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) :=
  (Equiv.Set.image (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X))) V ⋯).toHomeomorphOfIsInducing ⋯
e_1 :
  (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2) =
    (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2)
h :
  ∀ (x : { x : X // x ∈ (U i).carrier }) (hx : x ∈ V),
    Membership.mem (γ := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
        ((Subtype.val '' V) ↓∩ s)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) (↑x : X) ⋯) ↔
      Membership.mem (γ := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
        (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
          (V ↓∩ (↑(U i) : Set X) ↓∩ s))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) (↑x : X) ⋯)
⊢ Eq (α := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2)) ((Subtype.val '' V) ↓∩ s)
    (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
      (V ↓∩ (↑(U i) : Set X) ↓∩ s))

Tactic:
ext ⟨_, x, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)
x_1 : X
i : ι
hi : x_1 ∈ U i
V : Set (↑(↑(U i) : Set X) : Type u_2)
hVx : V ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) x_1 hi)
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (X := (↑V : Type u_2)) (V ↓∩ (↑(U i) : Set X) ↓∩ s)
e : (↑V : Type u_2) ≃ₜ (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2) :=
  (Equiv.Set.image (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X))) V ⋯).toHomeomorphOfIsInducing ⋯
e_1 :
  (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2) =
    (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) '' V) : Type u_2)
x : { x : X // x ∈ (U i).carrier }
hx : x ∈ V
⊢ Membership.mem (γ := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
      ((Subtype.val '' V) ↓∩ s)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) (↑x : X) ⋯) ↔
    Membership.mem (γ := Set (↑(Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) : Type u_2))
      (preimage (β := (↑V : Type u_2)) (⇑e.symm : (a : (↑(Subtype.val '' V) : Type u_2)) → (↑V : Type u_2))
        (V ↓∩ (↑(U i) : Set X) ↓∩ s))
      (Subtype.mk (p := fun (x : X) ↦ x ∈ Subtype.val (p := fun (x : X) ↦ x ∈ (U i).carrier) '' V) (↑x : X) ⋯)

Tactic:
simp [e, Equiv.toHomeomorphOfIsInducing]

Premises used: Equiv.toHomeomorphOfIsInducing
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (s ∩ (↑(U i) : Set X))
i : ι
rw :
  IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2))
    (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) ⁻¹' (s ∩ (↑(U i) : Set X)))
⊢ IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)

Tactic:
rw [← Subtype.preimage_coe_inter_self]

Premises used: Subtype.preimage_coe_inter_self
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (s ∩ (↑(U i) : Set X))
i : ι
⊢ IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2))
    (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) ⁻¹' (s ∩ (↑(U i) : Set X)))

Tactic:
(H i).preimage_of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, IsOpen.isOpenEmbedding_subtypeVal, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (s ∩ (↑(U i) : Set X))
i : ι
⊢ IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2))
    (Subtype.val (p := fun (x : X) ↦ x ∈ (↑(U i) : Set X)) ⁻¹' (s ∩ (↑(U i) : Set X)))

Tactic:
exact (H i).preimage_of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, IsOpen.isOpenEmbedding_subtypeVal, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
⊢ IsLocallyConstructible s ↔
    ∀ (i : ι), IsLocallyConstructible (X := (↑(↑(U i) : Set X) : Type u_2)) ((↑(U i) : Set X) ↓∩ s)

Tactic:
⟨fun H i ↦ H.preimage_of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal,
    fun H ↦ .of_isOpenCover hU H⟩

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, IsOpen.isOpenEmbedding_subtypeVal, Topology.IsLocallyConstructible.of_isOpenCover, Iff.intro, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
inst_1 : PrespectralSpace X
inst_2 : QuasiSeparatedSpace X
hU : IsOpenCover U
hU' : ∀ (i : ι), IsCompact (↑(U i) : Set X)
⊢ IsLocallyConstructible s ↔ ∀ (i : ι), IsConstructible (s ∩ (↑(U i) : Set X))

Tactic:
⟨fun H i ↦ H.inter_of_isOpen_isCompact (U i).2 (hU' i),
    fun H ↦ .of_isOpenCover' hU fun i ↦ (H i).isLocallyConstructible⟩

Premises used: Topology.IsConstructible.isLocallyConstructible, Topology.IsLocallyConstructible.inter_of_isOpen_isCompact, Iff.intro, TopologicalSpace.Opens.is_open', Topology.IsLocallyConstructible.of_isOpenCover'
-- Module: Mathlib.Topology.Constructions.SumProd
Goal:
X : Type u
Y : Type v
Z : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : X → Z
⊢ (Continuous[inst, instTopologicalSpaceProd] fun (x : X) ↦ (f x, g x)) ↔
    Continuous[inst, inst_1] f ∧ Continuous[inst, inst_2] g

Tactic:
continuous_inf_rng.trans <| continuous_induced_rng.and continuous_induced_rng

Premises used: setOf, Iff.and, Iff.trans, continuous_inf_rng, continuous_induced_rng