theorem littlestone_characterization (X : Type)
    (C : ConceptClass X Bool) :
    OnlineLearnable X Bool C (*@$\leftrightarrow$@*) LittlestoneDim X C < (*@$\top$@*) :=
  (*@$\langle$@*)forward_direction X C, backward_direction X C(*@$\rangle$@*)

theorem gold_theorem (X : Type u) [Countable X] [DecidableEq X]
    (C : ConceptClass X Bool)
    (h_finite : forall (S : Finset X), (fun x => decide (x (*@$\in$@*) S)) (*@$\in$@*) C)
    (h_infinite : exists c (*@$\in$@*) C, Set.Infinite { x | c x = true }) :
    (*@$\neg$@*) EXLearnable X C := by
  intro (*@$\langle$@*)L, hL(*@$\rangle$@*)
  obtain (*@$\langle$@*)c_inf, hc_inf_mem, hc_inf_inf(*@$\rangle$@*) := h_infinite
  let phi := hc_inf_inf.natEmbedding
  have hpos_ne : Nonempty { x : X | c_inf x = true } :=
    hc_inf_inf.nonempty.to_subtype
  obtain (*@$\langle$@*)enum, henum(*@$\rangle$@*) :=
    exists_surjective_nat ({ x : X | c_inf x = true })
  let S : N -> Finset X := fun n =>
    ((Finset.range (n + 1)).image (fun i => (phi i).val)) (*@$\cup$@*)
    ((Finset.range (n + 1)).image (fun i => (enum i).val))
  -- ... (152 more lines: constructs locking sequence via
  --      interleaving enumeration of c_inf's support with
  --      finite-set indicators, derives contradiction)