-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
set set₁ : SeparableSpace ((i : ι) → X i)
set₂ :
  let f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
    fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ =>
      if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i;
  ∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
    U.Nonempty → ∀ (g : (i : ι) → X i) (hg : g ∈ U), (U ∩ range f).Nonempty
set₃ :
  let f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
    fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ =>
      if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i;
  ∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
    U.Nonempty →
      ∀ (g : (i : ι) → X i) (hg : g ∈ U) (I : Finset ι) (u : (a : ι) → Set (X a))
        (huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a) (huU : (↑I : Set ι).pi (α := X) u ⊆ U), (U ∩ range f).Nonempty
⊢ SeparableSpace ((i : ι) → X i)
have set₄ : let f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
  match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
  | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i;
∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
  U.Nonempty →
    ∀ (g : (i : ι) → X i) (hg : g ∈ U) (I : Finset ι) (u : (a : ι) → Set (X a))
      (huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a) (huU : (↑I : Set ι).pi (α := X) u ⊆ U)
      (this :
        ∀ (i : ↥I),
          ∃ (y : X (↑i : ι)),
            Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) y ∧
              Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) y),
      (U ∩ range f).Nonempty
Tactic: classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩