-- Mathlib/Topology/Separation/Regular.lean
theorem regularSpace_sInf {X} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, @RegularSpace X t) :
    @RegularSpace X (sInf T)

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
a : X
⊢ (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
    ⋂ i, If.snd i

Tactic:
rw [nhds_sInf, ← iInf_subtype'']

Result:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
a : X
⊢ (⨅ i, 𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
    ⋂ i, If.snd i

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
⊢ RegularSpace X

Tactic:
have : ∀ a, (𝓝 a).HasBasis
    (fun If : Σ I : Set T, I → Set X =>
      If.1.Finite ∧ ∀ i : If.1, If.2 i ∈ @nhds X i a ∧ @IsClosed X i (If.2 i))
    fun If => ⋂ i : If.1, If.snd i := fun a ↦ by
  rw [nhds_sInf, ← iInf_subtype'']
  exact hasBasis_iInf fun t : T => @closed_nhds_basis X t (h t t.2) a

Result:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
      ⋂ i, If.snd i
⊢ RegularSpace X

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
⊢ RegularSpace X

Tactic:
let _ := sInf T

Result:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
⊢ RegularSpace X

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
      ⋂ i, If.snd i
⊢ RegularSpace X

Tactic:
refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_

Result:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
      ⋂ i, If.snd i
a : X
If : (I : Set ↑T) × (↑I → Set X)
hIf : If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)
i : ↑If.fst
⊢ IsClosed (If.snd i)

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
      ⋂ i, If.snd i
a : X
If : (I : Set ↑T) × (↑I → Set X)
hIf : If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)
i : ↑If.fst
⊢ IsClosed (If.snd i)

Tactic:
exact (hIf.2 i).2.mono (sInf_le (i : T).2)

Result:
no goals

Proof state:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x✝ : TopologicalSpace X := sInf T
a : X
⊢ (⨅ i, 𝓝 a).HasBasis (fun If => If.fst.Finite ∧ ∀ (i : ↑If.fst), If.snd i ∈ 𝓝 a ∧ IsClosed (If.snd i)) fun If =>
    ⋂ i, If.snd i

Tactic:
exact hasBasis_iInf fun t : T => @closed_nhds_basis X t (h t t.2) a

Result:
no goals