-- Mathlib/Topology/Constructible.lean
/-- Variant of `TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact` for a
non-indexed topological basis. -/
@[stacks 0069 "Iff form of (2). Note that Stacks doesn't define quasi-separated spaces."]
lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact'
    (basis : IsTopologicalBasis B) (isCompact_basis : ∀ U ∈ B, IsCompact U)
    (hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U

Proof state:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ ∀ (a b : Set X) (x : a ∈ B), ⟨a, ⋯⟩ ∈ s → ∀ (x : b ∈ B), ⟨b, ⋯⟩ ∈ t → IsCompact (a ∩ b)

Tactic:
exact fun u v hu _ hv _ ↦ (isCompact_basis _ hu).inter_of_isOpen (isCompact_basis _ hv)
  (basis.isOpen hu) (basis.isOpen hv)

Result:
no goals

Proof state:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ IsCompact (⋃₀ (Subtype.val '' ↑s) ∩ ⋃₀ (Subtype.val '' ↑t))

Tactic:
rw [Set.sUnion_inter_sUnion]

Result:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ IsCompact (⋃ p ∈ (Subtype.val '' ↑s) ×ˢ (Subtype.val '' ↑t), p.1 ∩ p.2)

Proof state:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ IsCompact (⋃ p ∈ (Subtype.val '' ↑s) ×ˢ (Subtype.val '' ↑t), p.1 ∩ p.2)

Tactic:
refine ((s.finite_toSet.image _).prod (t.finite_toSet.image _)).isCompact_biUnion ?_

Result:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ ∀ i ∈ ↑↑s ×ˢ ↑↑t, IsCompact (i.1 ∩ i.2)

Proof state:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ ∀ i ∈ ↑↑s ×ˢ ↑↑t, IsCompact (i.1 ∩ i.2)

Tactic:
simp only [mem_prod, mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right,
  and_imp, forall_exists_index, Prod.forall]

Result:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ ∀ (a b : Set X) (x : a ∈ B), ⟨a, ⋯⟩ ∈ s → ∀ (x : b ∈ B), ⟨b, ⋯⟩ ∈ t → IsCompact (a ∩ b)

Proof state:
case intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
V : Set X
hV' : IsCompact V
hV : IsOpen V
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
⊢ IsCompact (⋃₀ (Subtype.val '' ↑s) ∩ V)

Tactic:
obtain ⟨t, rfl⟩ := eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _ basis _ hV' hV

Result:
case intro.intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
t : Finset ↑B
hV' : IsCompact (⋃₀ (Subtype.val '' ↑t))
hV : IsOpen (⋃₀ (Subtype.val '' ↑t))
⊢ IsCompact (⋃₀ (Subtype.val '' ↑s) ∩ ⋃₀ (Subtype.val '' ↑t))

Proof state:
X : Type u_2
inst✝² : TopologicalSpace X
U : Set X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
hU : IsOpen U
⊢ IsRetrocompact U ↔ IsCompact U

Tactic:
refine ⟨IsRetrocompact.isCompact, fun hU' {V} hV' hV ↦ ?_⟩

Result:
X : Type u_2
inst✝² : TopologicalSpace X
U : Set X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
hU : IsOpen U
hU' : IsCompact U
V : Set X
hV' : IsCompact V
hV : IsOpen V
⊢ IsCompact (U ∩ V)

Proof state:
X : Type u_2
inst✝² : TopologicalSpace X
U : Set X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
hU : IsOpen U
hU' : IsCompact U
V : Set X
hV' : IsCompact V
hV : IsOpen V
⊢ IsCompact (U ∩ V)

Tactic:
obtain ⟨s, rfl⟩ := eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _ basis _ hU' hU

Result:
case intro
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
B : Set (Set X)
inst✝ : QuasiSeparatedSpace X
basis : IsTopologicalBasis B
isCompact_basis : ∀ U ∈ B, IsCompact U
V : Set X
hV' : IsCompact V
hV : IsOpen V
s : Finset ↑B
hU : IsOpen (⋃₀ (Subtype.val '' ↑s))
hU' : IsCompact (⋃₀ (Subtype.val '' ↑s))
⊢ IsCompact (⋃₀ (Subtype.val '' ↑s) ∩ V)