exists_greedy_chain experiment

Stream: Equational

[Michael Bucko]

A small experiment (#mwe) with exists_greedy_chain.

import equational_theories.Mathlib.Order.Greedy
import Mathlib.Order.Basic

universe u₁ u₂

theorem Exists.greedyChainRec
  {α : Type u₁} {β : Type u₂} [Preorder α] [Countable β]
  (task : β → Set α)
  (h : ∀ (a : α) (b : β), ∃ (a' : α), a ≤ a' ∧ a' ∈ task b)
  : ∀ (a₀ : α), ∃ (c : Set α),
    IsChain (· ≤ ·) c ∧
    a₀ ∈ c ∧
    (∀ x ∈ c, a₀ ≤ x) ∧
    ∀ (b : β), ∃ a ∈ c, a ∈ task b := by
  intro a₀
  let chain_build := λ (a : α) =>
    exists_greedy_chain task h a
  have build_step := λ (a : α) =>
    ∃ (a' : α), a ≤ a' ∧ ∀ (b : β), ∃ (x : α), x ∈ task b ∧ a ≤ x
  have chain := chain_build a₀
  obtain ⟨c, hc_chain, hc_mem, hc_bound, hc_task⟩ := chain
  exact ⟨c,
    hc_chain,
    hc_mem,
    hc_bound,
    hc_task⟩

[Michael Bucko]

@Amir Livne Bar-on have a look here. I already experimented with exists_greedy_chain