difficulty with topology lemma and topological bases

Stream: maths

[Panagiotis Angelinos]

I am trying to prove a little lemma: If X is a compact-open of a quasi-separated space Y and the set of compact-opens (in Y) forms a basis of Y, then the set of compact-opens (in X) forms a basis of X. Here is my code:

import Mathlib.Topology.QuasiSeparated
import Mathlib.Topology.Compactness.Compact
import Mathlib.Topology.ContinuousOn

variable (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] (f: X → Y)

theorem topology_lemma (X Y: Type*) [TopologicalSpace X] [TopologicalSpace Y]
  (hX : CompactSpace X) (hY : QuasiSeparatedSpace Y) (hf : OpenEmbedding f)
  (hYb: TopologicalSpace.IsTopologicalBasis {S : Set Y | IsOpen S ∧ IsCompact S}) :
  (TopologicalSpace.IsTopologicalBasis {S : Set X | IsOpen S ∧ IsCompact S}) := by
    constructor
    sorry
    sorry
    ext U
    constructor

The first constructor turns my goal TopologicalSpace.IsTopologicalBasis {S | IsOpen S ∧ IsCompact S} into three different subgoals exists_subset_inter, sUnion_eq, and eq_generateFrom, as per the definition of IsTopologicalBasis. I can prove the first two subgoals, so I've put in sorrys just to get rid of extraneous information.

The third subgoal turns out to be inst✝¹ = TopologicalSpace.generateFrom {S | IsOpen S ∧ IsCompact S} which as far as I know means I am in serious trouble because \textdied kills Lean. However, I tried ext U and got a goal of the form IsOpen U ↔ IsOpen U, which seems promising, but both implications seem to lead to dead ends. (You can't tell here, but these IsOpens refer to different topologies, and this is only made clear when you mouse over them in the tactics panel).

Anyway, is there something I can do with the subgoal inst✝¹ = TopologicalSpace.generateFrom {S | IsOpen S ∧ IsCompact S} that isn't ext? Or is it over once I have a \textdied in the goal? I've tried a few things and didn't manage to get them to work. If it helps, here's the definition of TopologicalSpace.generateFrom:

/-- The open sets of the least topology containing a collection of basic sets. -/
inductive GenerateOpen (g : Set (Set α)) : Set α → Prop
  | basic : ∀ s ∈ g, GenerateOpen g s
  | univ : GenerateOpen g univ
  | inter : ∀ s t, GenerateOpen g s → GenerateOpen g t → GenerateOpen g (s ∩ t)
  | sUnion : ∀ S : Set (Set α), (∀ s ∈ S, GenerateOpen g s) → GenerateOpen g (⋃₀ S)
#align topological_space.generate_open TopologicalSpace.GenerateOpen

/-- The smallest topological space containing the collection `g` of basic sets -/
def generateFrom (g : Set (Set α)) : TopologicalSpace α where
  IsOpen := GenerateOpen g
  isOpen_univ := GenerateOpen.univ
  isOpen_inter := GenerateOpen.inter
  isOpen_sUnion := GenerateOpen.sUnion
#align topological_space.generate_from TopologicalSpace.generateFrom

[Filippo A. E. Nuccio]

Some comments: first, it is nice (both for the style and because it simplifies the infoview) to split your subgoals using dots, obtained by typing \.. So you would get

theorem topology_lemma (X Y: Type*) [TopologicalSpace X] [TopologicalSpace Y]
  (hX : CompactSpace X) (hY : QuasiSeparatedSpace Y) (hf : OpenEmbedding f)
  (hYb: TopologicalSpace.IsTopologicalBasis {S : Set Y | IsOpen S ∧ IsCompact S}) :
  (TopologicalSpace.IsTopologicalBasis {S : Set X | IsOpen S ∧ IsCompact S}) := by
    constructor
    · sorry
    · sorry
    · sorry

In this way, each time you try to solve one goal, you also see this one (and local hypothesis get discharged once this is closed). Secondly, it is often a good idea to avoid using definitions directly: athough this is a normal mathematicians' habit, the way mathlib is constructed is to provide a bunch of theorems that allow to interact with definitions, rather than going back to the basic one. For instance, you can do

theorem topology_lemma (X Y: Type*) [TopologicalSpace X] [TopologicalSpace Y]
  (hX : CompactSpace X) (hY : QuasiSeparatedSpace Y) (hf : OpenEmbedding f)
  (hYb: TopologicalSpace.IsTopologicalBasis {S : Set Y | IsOpen S ∧ IsCompact S}) :
  (TopologicalSpace.IsTopologicalBasis {S : Set X | IsOpen S ∧ IsCompact S}) := by
    apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
    · intro U hU
      sorry
    · intro x S hx hS
      sorry

Finally, going back to your original question (which, as explained above, I would discourage to follow) you should first think at what the pen-and-paper proof would be: the isOpen U <-> isOpen U suggests that you need to show that something that was open in Y stays open in X...

[Panagiotis Angelinos]

Thanks for the help, I've managed to get this to work. And I've removed some unnecessary assumptions!