-- Mathlib/Topology/Constructible.lean
/-- If `f` is continuous and is such that preimages of retrocompact sets are retrocompact, then
preimages of constructible sets are constructible. -/
@[stacks 005I]
lemma IsConstructible.preimage {s : Set Y} (hfcont : Continuous f)
    (hf : ∀ s, IsRetrocompact s → IsRetrocompact (f ⁻¹' s)) (hs : IsConstructible s) :
    IsConstructible (f ⁻¹' s)

Proof state:
case open_retrocompact
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous f
hf : ∀ (s : Set Y), IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
U : Set Y
hUopen : IsOpen U
hUcomp : IsRetrocompact U
⊢ IsConstructible (f ⁻¹' U)

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

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
hfcont : Continuous f
hf : ∀ (s : Set Y), IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
⊢ IsConstructible (f ⁻¹' s)

Tactic:
induction hs using IsConstructible.empty_union_induction with
| open_retrocompact U hUopen hUcomp =>
  exact (hf _ 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

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 Y
hfcont : Continuous f
hf : ∀ (s : Set Y), 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'

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 Y
hfcont : Continuous f
hf : ∀ (s : Set Y), IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' sᶜ)

Tactic:
rw [preimage_compl]

Result:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set Y
hfcont : Continuous f
hf : ∀ (s : Set Y), IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (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 Y
hfcont : Continuous f
hf : ∀ (s : Set Y), IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
s : Set Y
hs : IsConstructible s
hs' : IsConstructible (f ⁻¹' s)
⊢ IsConstructible (f ⁻¹' s)ᶜ

Tactic:
exact hs'.compl

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 Y
hfcont : Continuous f
hf : ∀ (s : Set Y), 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 ∪ t))

Tactic:
rw [preimage_union]

Result:
case union
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set Y
hfcont : Continuous f
hf : ∀ (s : Set Y), 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)