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
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
U : Set Y
hUopen : IsOpen[inst_1] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f ⁻¹' U)

Tactic:
exact (hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont

Premises used: IsRetrocompact.isConstructible, 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_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
union : IsConstructible (f ⁻¹' s ∪ f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' (s ∪ t))

Tactic:
rw [preimage_union]

Premises used: Set.preimage_union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' s ∪ f ⁻¹' t)

Tactic:
hs'.union ht'

Premises used: Topology.IsConstructible.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
t : Set Y
ht : IsConstructible t
hs' : IsConstructible (f ⁻¹' s)
ht' : IsConstructible (f ⁻¹' t)
⊢ IsConstructible (f ⁻¹' s ∪ f ⁻¹' t)

Tactic:
exact hs'.union ht'

Premises used: Topology.IsConstructible.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
compl : IsConstructible (f ⁻¹' s)ᶜ
⊢ IsConstructible (f ⁻¹' sᶜ)

Tactic:
rw [preimage_compl]

Premises used: Set.preimage_compl
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' s)ᶜ

Tactic:
hs'.compl

Premises used: Topology.IsConstructible.compl
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set Y
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' s)ᶜ

Tactic:
exact hs'.compl

Premises used: Topology.IsConstructible.compl
-- 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
hfcont : Continuous[inst, inst_1] f
hf : ∀ (s : Set Y), IsOpen[inst_1] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
open_retrocompact : ∀ (U : Set Y) (hUopen : IsOpen[inst_1] U) (hUcomp : IsRetrocompact U), IsConstructible (f ⁻¹' U)
union :
  ∀ (s : Set Y) (hs : IsConstructible s) (t : Set Y) (ht : IsConstructible t) (hs' : IsConstructible (f ⁻¹' s))
    (ht' : IsConstructible (f ⁻¹' t)), IsConstructible (f ⁻¹' (s ∪ t))
compl : ∀ (s : Set Y) (hs : IsConstructible s) (hs' : IsConstructible (f ⁻¹' s)), IsConstructible (f ⁻¹' sᶜ)
⊢ IsConstructible (f ⁻¹' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hf _ hUopen hUcomp).isConstructible <| hUopen.preimage hfcont
  | union s hs t ht hs' ht' => rw [preimage_union]; exact hs'.union ht'
  | compl s hs hs' => rw [preimage_compl]; exact hs'.compl

Premises used: Topology.IsConstructible.union, Topology.IsConstructible.compl, Set.preimage_union, Set.preimage_compl
-- 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
hf : IsOpenEmbedding f
hs : IsConstructible s
⊢ IsConstructible (f ⁻¹' s)

Tactic:
hs.preimage hf.continuous fun _t _ ht ↦ ht.preimage_of_isOpenEmbedding hf

Premises used: Topology.IsOpenEmbedding.continuous, IsRetrocompact.preimage_of_isOpenEmbedding, Topology.IsConstructible.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
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsConstructible s
⊢ IsConstructible (f ⁻¹' s)

Tactic:
hs.preimage hf.continuous fun _t _ ht ↦ ht.preimage_of_isClosedEmbedding hf hf'

Premises used: IsRetrocompact.preimage_of_isClosedEmbedding, Topology.IsClosedEmbedding.continuous, Topology.IsConstructible.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 X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)

Tactic:
(hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen

Premises used: Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.isEmbedding, IsRetrocompact.image_of_isEmbedding, IsRetrocompact.isConstructible
-- 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 X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)

Tactic:
exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen

Premises used: Topology.IsOpenEmbedding.isOpenMap, Topology.IsOpenEmbedding.isEmbedding, IsRetrocompact.image_of_isEmbedding, IsRetrocompact.isConstructible
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
union : IsConstructible (f '' s ∪ f '' t)
⊢ IsConstructible (f '' (s ∪ t))

Tactic:
rw [image_union]

Premises used: Set.image_union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' s ∪ f '' t)

Tactic:
hs'.union ht'

Premises used: Topology.IsConstructible.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' s ∪ f '' t)

Tactic:
exact hs'.union ht'

Premises used: Topology.IsConstructible.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
compl : IsConstructible (range f \ f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
rw [← range_diff_image hfopen.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Set.range_diff_image, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)

Tactic:
(hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'

Premises used: Topology.IsOpenEmbedding.isOpen_range, IsRetrocompact.isConstructible, Topology.IsConstructible.sdiff
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)

Tactic:
exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'

Premises used: Topology.IsOpenEmbedding.isOpen_range, IsRetrocompact.isConstructible, Topology.IsConstructible.sdiff
-- 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 X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
union :
  ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t) (hs' : IsConstructible (f '' s))
    (ht' : IsConstructible (f '' t)), IsConstructible (f '' (s ∪ t))
compl : ∀ (s : Set X) (hs : IsConstructible s) (hs' : IsConstructible (f '' s)), IsConstructible (f '' sᶜ)
⊢ IsConstructible (f '' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <|
      hfopen.isOpenMap _ hUopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hfopen.injective]
    exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs'

Premises used: Topology.IsConstructible.union, Topology.IsConstructible.compl, Topology.IsOpenEmbedding.toIsEmbedding, Set.range_diff_image, Topology.IsEmbedding.injective, Set.image_union
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)

Tactic:
simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.range_diff_image, Set.compl_inter, sdiff_eq, Set.union_comm, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
⊢ IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)

Tactic:
have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
h : IsRetrocompact (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)

Tactic:
simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)

Premises used: Set.inter_eq_left, Iff.mpr, IsClosed.isOpen_compl, Set.image_subset_range, IsRetrocompact.isConstructible, Topology.IsConstructible.sdiff, Set.union_inter_distrib_right
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
open_retrocompact : IsRetrocompact (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)

Tactic:
suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst_1] V
open_retrocompact : IsCompact (f '' (U ∩ f ⁻¹' V) ∪ (range f)ᶜ ∩ V)
⊢ IsCompact ((f '' U ∪ (range f)ᶜ) ∩ V)

Tactic:
rw [union_inter_distrib_right, ← image_inter_preimage]

Premises used: Set.image_inter_preimage, Set.union_inter_distrib_right
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst_1] V
⊢ IsCompact (f '' (U ∩ f ⁻¹' V) ∪ (range f)ᶜ ∩ V)

Tactic:
((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen

Premises used: Topology.IsClosedEmbedding.continuous, Topology.IsClosedEmbedding.isCompact_preimage, IsCompact.union, IsOpen.preimage, IsCompact.image
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst_1] (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen[inst_1] V
⊢ IsCompact (f '' (U ∩ f ⁻¹' V) ∪ (range f)ᶜ ∩ V)

Tactic:
exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen

Premises used: Topology.IsClosedEmbedding.continuous, Topology.IsClosedEmbedding.isCompact_preimage, IsCompact.union, IsOpen.preimage, IsCompact.image
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
union : IsConstructible (f '' s ∪ f '' t)
⊢ IsConstructible (f '' (s ∪ t))

Tactic:
rw [image_union]

Premises used: Set.image_union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' s ∪ f '' t)

Tactic:
hs'.union ht'

Premises used: Topology.IsConstructible.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
t : Set X
ht : IsConstructible t
hs' : IsConstructible (f '' s)
ht' : IsConstructible (f '' t)
⊢ IsConstructible (f '' s ∪ f '' t)

Tactic:
exact hs'.union ht'

Premises used: Topology.IsConstructible.union
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
compl : IsConstructible (range f \ f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
rw [← range_diff_image hf.injective]

Premises used: Set.range_diff_image, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)

Tactic:
(hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'

Premises used: IsClosed.isOpen_compl, Topology.IsConstructible.of_compl, IsRetrocompact.isConstructible, Topology.IsConstructible.sdiff
-- Module: Mathlib.Topology.Constructible
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s_1 : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)

Tactic:
exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'

Premises used: IsClosed.isOpen_compl, Topology.IsConstructible.of_compl, IsRetrocompact.isConstructible, Topology.IsConstructible.sdiff
-- 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 X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst] U) (hUcomp : IsRetrocompact U), IsConstructible (f '' U)
union :
  ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t) (hs' : IsConstructible (f '' s))
    (ht' : IsConstructible (f '' t)), IsConstructible (f '' (s ∪ t))
compl : ∀ (s : Set X) (hs : IsConstructible s) (hs' : IsConstructible (f '' s)), IsConstructible (f '' sᶜ)
⊢ IsConstructible (f '' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with
  | open_retrocompact U hUopen hUcomp =>
    have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
      simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm]
        using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
    suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
      simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)]
        using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
    rintro V hVcomp hVopen
    rw [union_inter_distrib_right, ← image_inter_preimage]
    exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image
      hf.continuous).union <| hfcomp hVcomp hVopen
  | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
  | compl s hs hs' =>
    rw [← range_diff_image hf.injective]
    exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'

Premises used: Topology.IsConstructible.union, Topology.IsConstructible.compl, Set.image_inter_preimage, Set.range_diff_image, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.union_inter_distrib_right, Set.image_union
-- 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
hf : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hsf : s ⊆ range f
hs : IsConstructible (f ⁻¹' s)
⊢ IsConstructible s

Tactic:
simpa [image_preimage_eq_range_inter, inter_eq_right.2 hsf]
    using hs.image_of_isOpenEmbedding hf hfcomp

Premises used: Iff.mpr, Set.image_preimage_eq_range_inter, Set.inter_eq_right, Topology.IsConstructible.image_of_isOpenEmbedding
-- 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₂
⊢ V₁ ⊆ ⋃ (i : ι), (U i).carrier

Tactic:
simp [hU.iSup_set_eq_univ]

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ
-- 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₂
obtain : ∀ (t : Finset ι) (ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier), IsCompact (V₁ ∩ V₂)
⊢ IsCompact (V₁ ∩ V₂)

Tactic:
obtain ⟨t, ht⟩ := hc₁.elim_finite_subcover _ (fun i ↦ (U i).2) (by simp [hU.iSup_set_eq_univ])

Premises used: IsCompact.elim_finite_subcover, TopologicalSpace.Opens.is_open'
-- 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
⊢ IsCompact.{u_2} (X := X) (⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂))

Tactic:
t.isCompact_biUnion fun i _ ↦
        h₂ i _ _ Set.inter_subset_left ((U i).2.inter ho₁) (h₁ i hc₁ ho₁) Set.inter_subset_left
          ((U i).2.inter ho₂) (h₁ i hc₂ ho₂)

Premises used: Set.inter_subset_left, Inter.inter, Finset.isCompact_biUnion, SetLike.coe, IsOpen.inter, TopologicalSpace.Opens.is_open'
-- 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
h : V₁ ∩ V₂ = ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
⊢ IsCompact (V₁ ∩ V₂)

Tactic:
convert!
      t.isCompact_biUnion fun i _ ↦
        h₂ i _ _ Set.inter_subset_left ((U i).2.inter ho₁) (h₁ i hc₁ ho₁) Set.inter_subset_left
          ((U i).2.inter ho₂) (h₁ i hc₂ ho₂)

Premises used: Set.inter_subset_left, Inter.inter, Finset.isCompact_biUnion, SetLike.coe, IsOpen.inter, TopologicalSpace.Opens.is_open'
-- 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
h : V₁ ∩ V₂ ⊆ ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)
h₃ : ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂) ⊆ V₁ ∩ V₂
⊢ V₁ ∩ V₂ = ⋃ i ∈ t, (↑(U i) : Set X) ∩ V₁ ∩ ((↑(U i) : Set X) ∩ V₂)

Tactic:
apply subset_antisymm

Premises used: subset_antisymm