-- 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
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
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)
        (y : (i : ↥I) → X (↑i : ι)) (hyt : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) (y i))
        (hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) (y i)), (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)
        (y : (i : ↥I) → (↑(t (↑i : ι)) : Type u_3))
        (hyu :
          ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) ((fun (i : ↥I) ↦ (↑(y i) : X (↑i : ι))) i)),
        (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)
        (y : (i : ↥I) → (↑(t (↑i : ι)) : Type u_3))
        (hyu :
          ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) ((fun (i : ↥I) ↦ (↑(y i) : X (↑i : ι))) i))
        (i : ι) (hi : i ∈ I), f (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) I y) i ∈ u i
⊢ SeparableSpace ((i : ι) → X i)
have set₈ : ∀ (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)
      (y : (i : ↥I) → (↑(t (↑i : ι)) : Type u_3))
      (hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) ((fun (i : ↥I) ↦ (↑(y i) : X (↑i : ι))) i))
      (i : ι) (hi : i ∈ I),
      Membership.mem (α := X i) (u i) ((↑(y (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i sorry)) : X i) : X i)
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, _⟩