-- Mathlib/Topology/Bases.lean
theorem IsSeparable.univ_pi {ι : Type*} [Countable ι] {X : ι → Type*} {s : ∀ i, Set (X i)}
    [∀ i, TopologicalSpace (X i)] (h : ∀ i, IsSeparable (s i)) :
    IsSeparable (univ.pi s)

Proof state:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
i : ι
hi : i ∈ I
⊢ g ⟨I, fun i => ⟨f ↑i ⋯, ⋯⟩⟩ i ∈ u i

Tactic:
simpa only [g, dif_pos hi] using hfu i hi

Result:
no goals

Proof state:
case inr.intro
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f ∈ o
⊢ (o ∩ range g).Nonempty

Tactic:
rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩

Result:
case inr.intro.intro.intro.intro
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
⊢ (o ∩ range g).Nonempty

Proof state:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
i : ι
hi : i ∈ I
⊢ (u i ∩ c i).Nonempty

Tactic:
exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Result:
no goals

Proof state:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u

Tactic:
refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩

Result:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
i : ι
hi : i ∈ I
⊢ g ⟨I, fun i => ⟨f ↑i ⋯, ⋯⟩⟩ i ∈ u i

Proof state:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
H : ∀ i ∈ I, (u i ∩ c i).Nonempty
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u

Tactic:
choose f hfu hfc using H

Result:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u

Proof state:
case inr.intro.intro.intro.intro.intro
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f✝ : (i : ι) → X i
hf✝ : f✝ ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f✝ ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f✝ a ∈ u a
hI : (↑I).pi u ⊆ o
f : (i : { x // x ∈ I }) → ↑(c ↑i)
hf : g ⟨I, f⟩ ∈ (↑I).pi u
⊢ (o ∩ range g).Nonempty

Tactic:
exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩

Result:
no goals