Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : WithTop ι
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi a)

Tactic:
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

Goal state after: