-- Mathlib/Topology/Constructible.lean
lemma IsLocallyConstructible.inter (hs : IsLocallyConstructible s) (ht : IsLocallyConstructible t) :
    IsLocallyConstructible (s ∩ t)

Proof state:
case intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s ∩ t)

Tactic:
obtain ⟨V, hxV, hV, htV⟩ := ht x

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen V
htV : IsConstructible (V ↓∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s ∩ t)

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((inclusion ⋯ ⁻¹' U ↓∩ s) ∩ inclusion ⋯ ⁻¹' V ↓∩ t)

Tactic:
exact .inter (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <|
    .preimage continuous_subtype_val <| hU.inter hV)
  (htV.preimage_of_isOpenEmbedding <| .inclusion _ <|
    .preimage continuous_subtype_val <| hU.inter hV )

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen V
htV : IsConstructible (V ↓∩ t)
⊢ ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s ∩ t)

Tactic:
refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((U ∩ V) ↓∩ s ∩ t)

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((U ∩ V) ↓∩ s ∩ t)

Tactic:
change IsConstructible
  (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t))

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((inclusion ⋯ ⁻¹' U ↓∩ s) ∩ inclusion ⋯ ⁻¹' V ↓∩ t)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
⊢ IsLocallyConstructible (s ∩ t)

Tactic:
rintro x

Result:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s ∩ t)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
⊢ ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s ∩ t)

Tactic:
obtain ⟨U, hxU, hU, hsU⟩ := hs x

Result:
case intro.intro.intro
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen U
hsU : IsConstructible (U ↓∩ s)
⊢ ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s ∩ t)