-- Mathlib/Topology/ClopenBox.lean
theorem exists_prod_subset (W : Clopens (X × Y)) {a : X × Y} (h : a ∈ W) :
    ∃ U : Clopens X, a.1 ∈ U ∧ ∃ V : Clopens Y, a.2 ∈ V ∧ U ×ˢ V ≤ W

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
have hp : Continuous (fun y : Y ↦ (a.1, y)) := Continuous.Prod.mk _

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
let V : Set Y := {y | (a.1, y) ∈ W}

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
hUV : U ×ˢ V ⊆ ↑W
⊢ a.1 ∈ { carrier := U, isClopen' := ⋯ }

Tactic:
simp [U, V, MapsTo]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
have hV : IsCompact V := (W.2.1.preimage hp).isCompact

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
hUV : U ×ˢ V ⊆ ↑W
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
let U : Set X := {x | MapsTo (Prod.mk x) V W}

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace Y
W : Clopens (X × Y)
a : X × Y
h : a ∈ W
hp : Continuous fun y => (a.1, y)
V : Set Y := {y | (a.1, y) ∈ W}
hV : IsCompact V
U : Set X := {x | MapsTo (Prod.mk x) V ↑W}
hUV : U ×ˢ V ⊆ ↑W
⊢ ∃ U, a.1 ∈ U ∧ ∃ V, a.2 ∈ V ∧ U ×ˢ V ≤ W

Tactic:
exact ⟨⟨U, (ContinuousMap.isClopen_setOf_mapsTo hV W.2).preimage
  (ContinuousMap.id (X × Y)).curry.2⟩, by simp [U, V, MapsTo], ⟨V, W.2.preimage hp⟩, h, hUV⟩

Result:
no goals