Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
⊢ SecondCountableTopology (WithTop ι)

Tactic:
classical
  rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩
  · infer_instance
  /- Let `c` be a countable set in `ι` such that the topology is generated by the sets `Iio a`
  and `Ioi a` for `a ∈ c`, by second-countability. Let `c'` be a dense set in `ι`, again by
  second-countability. Let `d` in `WithTop ι` be obtained from `c ∪ c'`, by adding `⊤` and a point
  `x₁ : ι` with `Ioi x₁ = ∅` if there is one.
  We will show that the topology on `WithTop ι` is generated by the intervals `Iio a` and `Ioi a`
  for `a ∈ d`, which will conclude the proof by countability of `d`. -/
  obtain ⟨c, c_count, hc⟩ : ∃ (c : Set ι), c.Countable ∧
      ts = generateFrom { s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a } :=
    exists_countable_generateFrom_Ioi_Iio ι
  obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' :=
    SeparableSpace.exists_countable_dense
  let x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
  let d : Set (WithTop ι) := (↑) '' c ∪ (↑) '' c' ∪ {⊤} ∪ {(x₁ : WithTop ι)}
  suffices H : instWithTopOfOrderTopology
      = generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} by
    refine ⟨{s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}, ?_, by rw [← H]⟩
    have d_count : d.Countable :=
      (((c_count.image _).union (c'_count.image _)).union (by simp)).union (by simp)
    have : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d := by
      #adaptation_note /-- Before leanprover/lean4#13166, this was just `grind`.
      The new canonicalizer using `isDefEq` less,
      and so does not unify as many of the conditions that `grind` wants to case split on.
      Alternatively `ext; simp; grind` work here. -/
      grind (splits := 12)
    rw [this]
    exact (d_count.image _).union (d_count.image _)
  -- We should check the easy direction that all the elements in our generating set are open.
  -- This is trivial as these are all intervals.
  apply le_antisymm
  · apply le_generateFrom_iff_subset_isOpen.2
    grind [isOpen_Iio', isOpen_Ioi']
  /- Now, let us check that our sets indeed generates the topology. As the topology is
  generated by the open half-infinite intervals by definition, we should check that open
  half-infinite intervals are covered by finite intersections of our sets. -/
  let basis : Set (Set ι) := {s | ∃ (f g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite
      ∧ s = (⋂ a ∈ f, Ioi a) ∩ (⋂ a ∈ g, Iio a)}
  have h_basis : IsTopologicalBasis basis := isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom c hc
  rw [OrderTopology.topology_eq_generate_intervals (α := WithTop ι)]
  apply le_generateFrom_iff_subset_isOpen.2
  simp only [ofPred_subset_ofPred, forall_exists_index]
  rintro u a (rfl | rfl)
  -- Consider an interval of the form `Ioi a`. We should cover it by finite intersections of
  -- our sets.
  · induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Ioi ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Ioi a`, and seek a finite intersection of our
      -- sets containing it and contained in `Ioi a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top =>
        -- if `b = ⊤`, then either `Ioi a` is empty in `ι` and then we use `Ioi (↑x₁)` which is
        -- in our set and reduced to `⊤`
        rcases eq_empty_or_nonempty (Ioi a) with ha | ha
        · refine ⟨Ioi x₁, ?_, ?_, by simp⟩
          · have : Ioi x₁ = ∅ := by
              have h : ∃ x, Ioi x = ∅ := ⟨a, ha⟩
              simp only [x₁, h, ↓reduceDIte]
              exact h.choose_spec
            simp [WithTop.Ioi_coe, this]
          · apply isOpen_generateFrom_of_mem
            simp [d]
        -- If `Ioi a` is not empty in `ι`, it contains a point `b` in the dense set `c'`, and then
        -- we use `Ioi (↑b)` which is in our set, contained in `Ioi (↑a)` and contains `⊤`.
        · obtain ⟨b, bc', hb⟩ : ∃ b ∈ c', b ∈ Ioi a := hc'.exists_mem_open (isOpen_Ioi' a) ha
          refine ⟨Ioi b, ?_, ?_, by simp⟩
          · apply Ioi_subset_Ioi
            simpa using hb.le
          · apply isOpen_generateFrom_of_mem
            exact ⟨b, by simp [d, bc'], Or.inl rfl⟩
      | coe b =>
        -- if `b` comes from `ι`, then in `ι` we can find a finite intersection of our sets
        -- containing `b` and contained in `Ioi a`. We lift it to `WithTop ι`.
        simp only [mem_Ioi, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Ioi a := h_basis.isOpen_iff.1 (isOpen_Ioi' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp
          | coe w =>
            simp only [mem_Ioi, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
  -- Consider an interval of the form `Iio a`. We should cover it by finite intersections of
  -- our sets.
  · induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
      -- sets containing it and contained in `Iio a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind

Goal state after: