-- Mathlib/Topology/Constructions.lean
theorem prod_generateFrom_generateFrom_eq {X Y : Type*} {s : Set (Set X)} {t : Set (Set Y)}
    (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
    @instTopologicalSpaceProd X Y (generateFrom s) (generateFrom t) =
      generateFrom (image2 (·  ×ˢ ·) s t) :=
  let G := generateFrom (image2  (·  ×ˢ ·) s t)
  le_antisymm
    (le_generateFrom fun _ ⟨_, hu, _, hv, g_eq⟩ =>
      g_eq.symm ▸
        @IsOpen.prod _ _ (generateFrom s) (generateFrom t) _ _ (GenerateOpen.basic _ hu)
          (GenerateOpen.basic _ hv))
    (le_inf
      (coinduced_le_iff_le_induced.mp <|
        le_generateFrom fun u hu =>
          have : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u

Proof state:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u
⊢ TopologicalSpace.IsOpen (Prod.fst ⁻¹' u)

Tactic:
rw [← this]

Result:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u
⊢ TopologicalSpace.IsOpen (⋃ v ∈ t, u ×ˢ v)

Proof state:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
⊢ ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v

Tactic:
simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]

Result:
no goals

Proof state:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u

Tactic:
simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]

Result:
no goals

Proof state:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u
⊢ TopologicalSpace.IsOpen (⋃ v ∈ t, u ×ˢ v)

Tactic:
exact
  isOpen_iUnion fun v =>
    isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Result:
no goals

Proof state:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (Prod.snd ⁻¹' v)

Tactic:
rw [← this]

Result:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (⋃ u ∈ s, u ×ˢ v)

Proof state:
X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 => x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (⋃ u ∈ s, u ×ˢ v)

Tactic:
exact
  isOpen_iUnion fun u =>
    isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Result:
no goals