-- Mathlib/Topology/Constructions.lean
theorem pi_generateFrom_eq {π : ι → Type*} {g : ∀ a, Set (Set (π a))} :
    (@Pi.topologicalSpace ι π fun a => generateFrom (g a)) =
      generateFrom
        { t | ∃ (s : ∀ a, Set (π a)) (i : Finset ι), (∀ a ∈ i, s a ∈ g a) ∧ t = pi (↑i) s }

Proof state:
case refine_1.h
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ ∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}, IsOpen s

Tactic:
rintro _ ⟨s, i, hi, rfl⟩

Result:
case refine_1.h.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
s : (a : ι) → Set (π a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
⊢ IsOpen ((↑i).pi s)

Proof state:
case refine_1.h.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
s : (a : ι) → Set (π a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
⊢ IsOpen ((↑i).pi s)

Tactic:
letI := fun a => generateFrom (g a)

Result:
case refine_1.h.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
s : (a : ι) → Set (π a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
this : (a : ι) → TopologicalSpace (π a) := fun a => generateFrom (g a)
⊢ IsOpen ((↑i).pi s)

Proof state:
case refine_1
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ Pi.topologicalSpace ≤ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
apply le_generateFrom

Result:
case refine_1.h
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ ∀ s ∈ {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}, IsOpen s

Proof state:
case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
i : ι
s : Set (π i)
hs : s ∈ g i
⊢ IsOpen s

Tactic:
refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩

Result:
case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
i : ι
s : Set (π i)
hs : s ∈ g i
⊢ (∀ a ∈ {i}, update (fun i => univ) i s a ∈ g a) ∧ (fun f => f i) ⁻¹' s = (↑{i}).pi (update (fun i => univ) i s)

Proof state:
case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace

Tactic:
refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_

Result:
case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
i : ι
s : Set (π i)
hs : s ∈ g i
⊢ IsOpen s

Proof state:
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ Pi.topologicalSpace ≤ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace

Proof state:
case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace

Tactic:
classical
refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
simp [hs]

Result:
no goals

Proof state:
case refine_2
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
i : ι
s : Set (π i)
hs : s ∈ g i
⊢ (∀ a ∈ {i}, update (fun i => univ) i s a ∈ g a) ∧ (fun f => f i) ⁻¹' s = (↑{i}).pi (update (fun i => univ) i s)

Tactic:
simp [hs]

Result:
no goals

Proof state:
case refine_1.h.intro.intro.intro
ι : Type u_5
π : ι → Type u_8
g : (a : ι) → Set (Set (π a))
s : (a : ι) → Set (π a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
this : (a : ι) → TopologicalSpace (π a) := fun a => generateFrom (g a)
⊢ IsOpen ((↑i).pi s)

Tactic:
exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))

Result:
no goals