-- Mathlib/Topology/Constructible.lean
@[stacks 09YG]
lemma IsConstructible.image_of_isClosedEmbedding (hf : IsClosedEmbedding f)
    (hfcomp : IsRetrocompact (range f)ᶜ) (hs : IsConstructible s) : IsConstructible (f '' s)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (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)

Result:
no goals

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

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
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f '' U)

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

Result:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)

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
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (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)

Result:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
⊢ IsRetrocompact (f '' U ∪ (range f)ᶜ)

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
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen V
⊢ IsCompact ((f '' U ∪ (range f)ᶜ) ∩ V)

Tactic:
rw [union_inter_distrib_right, ← image_inter_preimage]

Result:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen V
⊢ IsCompact (f '' (U ∩ f ⁻¹' V) ∪ (range f)ᶜ ∩ V)

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

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
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
⊢ IsRetrocompact (f '' U ∪ (range f)ᶜ)

Tactic:
rintro V hVcomp hVopen

Result:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen V
⊢ IsCompact ((f '' U ∪ (range f)ᶜ) ∩ V)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
⊢ IsOpen (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

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
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'

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
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'

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
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen U
hUcomp : IsRetrocompact U
hfU : IsOpen (f '' U ∪ (range f)ᶜ)
V : Set Y
hVcomp : IsCompact V
hVopen : IsOpen 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

Result:
no goals