tree orders: `IsPredArchimedean` vs `LocallyFiniteOrderBot`

Stream: mathlib4

[Bernhard Reinke]

I think there are two major ways to talk about a partial ordering where every every lower interval is a finite linear ordered subset: one is to use [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α], the other one is to use [PartialOrder α] [PredOrder α] [LocallyFiniteOrderBot α] [DecidableEq α]. The second one is slightly more general as multiply minimal elements are allowed. Here is a snippet deriving one from the other

import Mathlib.Order.Interval.Finset.SuccPred
import Mathlib.Order.Grade
import Mathlib.Order.Interval.Finset.Basic

section
variable {α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [OrderBot α] [DecidableEq α]

def height (a : α) := Nat.find (exists_pred_iterate_of_le (bot_le (a := a)))

@[simp]
theorem pred_iterate_height_eq_bot (a : α) : Order.pred^[height a] a = ⊥ :=
  Nat.find_spec (exists_pred_iterate_of_le (bot_le (a := a)))

theorem pred_iterate_eq_bot_of_height_le {a : α} {n : ℕ} (h : height a ≤ n) :
    Order.pred^[n] a = ⊥ := by
  induction h
  case refl => simp
  case step _ ih =>
    rw [Nat.succ_eq_one_add, Function.iterate_add]
    simp [ih]

theorem exists_pred_iterate_le_height_of_le {a b : α} (h : a ≤ b) :
    ∃ (n : ℕ), Order.pred^[n] b = a ∧ n ≤ height b := by
  use Nat.find (exists_pred_iterate_of_le h), Nat.find_spec (exists_pred_iterate_of_le h)
  apply le_of_not_gt
  intro h'
  have eq : a = ⊥ := by
    rw [← pred_iterate_eq_bot_of_height_le h'.le, Nat.find_spec (exists_pred_iterate_of_le h)]
  apply Nat.find_min (exists_pred_iterate_of_le h) h'
  simp [eq]

instance : LocallyFiniteOrderBot α := LocallyFiniteOrderBot.ofIic
  (finsetIic := fun (b : α) =>
    Finset.image (fun (n : Fin ((height b) + 1)) => Order.pred^[n] b) Finset.univ)
  (mem_Iic := by
    intro a b
    simp only [Finset.mem_image, Finset.mem_univ, true_and]
    constructor
    · rintro ⟨n, h⟩
      simp [← h, Order.pred_iterate_le]
    · intro h
      obtain ⟨n, eq, ineq⟩ := exists_pred_iterate_le_height_of_le h
      use ⟨n, by omega⟩, eq
  )
end

section
variable {α} [PartialOrder α] [PredOrder α] [LocallyFiniteOrderBot α] [DecidableEq α]

instance : GradeMinOrder ℕ α where
  grade b := (Finset.Iio b).card
  grade_strictMono a b h := Finset.card_lt_card (Finset.Iio_ssubset_Iio h)
  covBy_grade {a b} h := by
    have eq : Order.pred b = a := Order.pred_eq_of_covBy h
    rw [← eq]
    have eq' : Finset.Iio b = Finset.Iic (Order.pred b) := by
      ext x
      symm
      simp
      apply Order.le_pred_iff_of_not_isMin
      simp only [not_isMin_iff]
      use a, h.lt
    rw [eq', Finset.card_Iio_eq_card_Iic_sub_one,Order.covBy_iff_add_one_eq]
    simp
  isMin_grade a := by simp

instance instPred : IsPredArchimedean α := inferInstance
end

does it make sense to add one of the instances to mathlib? If so, which one? Probably adding both might add some complications.

[Bernhard Reinke]

Any thoughts on this? I had some PRs related to these snippets, one of them is already merged, but #23810 hasn't been reviewed yet.