-- Mathlib/Topology/QuasiSeparated.lean
lemma QuasiSeparatedSpace.of_isTopologicalBasis {ι : Type*} {b : ι → Set α}
    (basis : IsTopologicalBasis (range b)) (isCompact_inter : ∀ i j, IsCompact (b i ∩ b j)) :
    QuasiSeparatedSpace α where
  inter_isCompact U V hUopen hUcomp hVopen hVcomp

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen (⋃ i ∈ t, b i)
hVcomp : IsCompact (⋃ i ∈ t, b i)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ ⋃ i ∈ t, b i)

Tactic:
rw [iUnion₂_inter_iUnion₂]

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen (⋃ i ∈ t, b i)
hVcomp : IsCompact (⋃ i ∈ t, b i)
⊢ IsCompact (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen U
hUcomp : IsCompact U
hVopen : IsOpen V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
⊢ IsCompact (U ∩ V)

Tactic:
obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩

Result:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
V : Set α
hVopen : IsOpen V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ V)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen U
hUcomp : IsCompact U
hVopen : IsOpen V
hVcomp : IsCompact V
i : ι
⊢ IsCompact (b i)

Tactic:
simpa using isCompact_inter i i

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen (⋃ i ∈ t, b i)
hVcomp : IsCompact (⋃ i ∈ t, b i)
⊢ IsCompact (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)

Tactic:
exact hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
V : Set α
hVopen : IsOpen V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ V)

Tactic:
obtain ⟨t, ht, rfl⟩ := (aux _).1 ⟨hVcomp, hVopen⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen (⋃ i ∈ t, b i)
hVcomp : IsCompact (⋃ i ∈ t, b i)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ ⋃ i ∈ t, b i)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen U
hUcomp : IsCompact U
hVopen : IsOpen V
hVcomp : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
have aux := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b basis fun i ↦ by
  simpa using isCompact_inter i i

Result:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen U
hUcomp : IsCompact U
hVopen : IsOpen V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
⊢ IsCompact (U ∩ V)