-- Mathlib/Topology/Constructible.lean
@[stacks 09YD]
lemma IsConstructible.image_of_isOpenEmbedding (hfopen : IsOpenEmbedding f)
    (hfcomp : IsRetrocompact (range f)) (hs : IsConstructible s) : IsConstructible (f '' s)

Proof state:
case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : 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'

Result:
no goals

Proof state:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
rw [← range_diff_image hfopen.injective]

Result:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)

Proof state:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : 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'

Result:
no goals

Proof state:
case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : 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 ∪ t))

Tactic:
rw [image_union]

Result:
case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : 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)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible 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'

Result:
no goals

Proof state:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)

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

Result:
no goals