-- Mathlib/Topology/Constructions.lean
theorem pi_generateFrom_eq_finite {π : ι → Type*} {g : ∀ a, Set (Set (π a))} [Finite ι]
    (hg : ∀ a, ⋃₀ g a = univ) :
    (@Pi.topologicalSpace ι π fun a => generateFrom (g a)) =
      generateFrom { t | ∃ s : ∀ a, Set (π a), (∀ a, s a ∈ g a) ∧ t = pi univ s }

Proof state:
case intro.refine_2.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → π i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen (univ.pi ((↑i).piecewise t c))

Tactic:
refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩

Result:
case intro.refine_2.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → π i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
⊢ (↑i).piecewise t c a ∈ g a

Proof state:
case intro.refine_2.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → π i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ ∃ t_1 ⊆ (↑i).pi t, IsOpen t_1 ∧ f ∈ t_1

Tactic:
refine ⟨pi i t ∩ pi ((↑i)ᶜ : Set ι) c, inter_subset_left, ?_, ⟨hf, fun a _ => hfc a⟩⟩

Result:
case intro.refine_2.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (π a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → π i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → π i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (π a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen ((↑i).pi t ∩ (↑i)ᶜ.pi c)

Proof state:
case intro.refine_1
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s} ⊆ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
exact fun s ⟨t, ht, Eq⟩ => ⟨t, Finset.univ, by simp [ht, Eq]⟩

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}