-- Mathlib/Topology/Constructible.lean
@[stacks 09YE "Extracted from the proof"]
lemma IsRetrocompact.preimage_of_isClosedEmbedding {s : Set Y} (hf : IsClosedEmbedding f)
    (hf' : IsCompact (range f)ᶜ) (hs : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s)

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

Tactic:
rintro U hUcomp hUopen

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f ⁻¹' s ∩ U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
have hfUopen : 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:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
hfUopen : IsOpen (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
hfUopen : IsOpen (f '' U ∪ (range f)ᶜ)
hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..),
  hf.isCompact_iff, image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
hfUopen : IsOpen (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen U
hfUopen : IsOpen (f '' U ∪ (range f)ᶜ)
hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)