-- Mathlib/Topology/GDelta/Basic.lean
lemma isGδ_iff_eq_iInter_nat {s : Set X} :
    IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ n, IsOpen (f n)) ∧ s = ⋂ n, f n

Proof state:
case refine_1.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT : ∀ t ∈ T, IsOpen t
T_count : T.Countable
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
rcases Set.eq_empty_or_nonempty T with rfl|hT

Result:
case refine_1.intro.intro.intro.inl
X : Type u_1
inst✝ : TopologicalSpace X
hT : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ ∅ = ⋂ n, f n

case refine_1.intro.intro.intro.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ T = ⋂ n, f n

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n

Tactic:
rintro ⟨T, hT, T_count, rfl⟩

Result:
case refine_1.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT : ∀ t ∈ T, IsOpen t
T_count : T.Countable
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ T = ⋂ n, f n

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∀ (n : ℕ), IsOpen (f n)

Tactic:
aesop

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s ↔ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n) → IsGδ s

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n) → IsGδ s

Tactic:
rintro ⟨f, hf, rfl⟩

Result:
case refine_2.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
f : ℕ → Set X
hf : ∀ (n : ℕ), IsOpen (f n)
⊢ IsGδ (⋂ n, f n)

Proof state:
case refine_1.intro.intro.intro.inl
X : Type u_1
inst✝ : TopologicalSpace X
hT : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ ∅ = ⋂ n, f n

Tactic:
exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.inr
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT

Result:
case refine_1.intro.intro.intro.inr.intro
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ T = ⋂ n, f n

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
hT : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
⊢ ⋂₀ ∅ = ⋂ n, (fun _n => univ) n

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.inr.intro
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ ⋂₀ T = ⋂ n, f n

Tactic:
exact ⟨f, by aesop, by simp [hf]⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
T : Set (Set X)
hT✝ : ∀ t ∈ T, IsOpen t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ⋂₀ T = ⋂ n, f n

Tactic:
simp [hf]

Result:
no goals

Proof state:
case refine_2.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
f : ℕ → Set X
hf : ∀ (n : ℕ), IsOpen (f n)
⊢ IsGδ (⋂ n, f n)

Tactic:
exact .iInter_of_isOpen hf

Result:
no goals