LocallyFiniteOrderBot to LocallyFiniteOrder and OrderBot

Stream: Is there code for X?

[Kenny Lau]

-- shouldn't be an instnace
def LocallyFiniteOrderBot.toLocallyFiniteOrder
    (ι : Type*) [Preorder ι] [DecidableLT ι] [DecidableLE ι] [LocallyFiniteOrderBot ι] :
    LocallyFiniteOrder ι where
  finsetIcc x y := (Iic y).filter (x ≤ ·)
  finsetIco x y := (Iio y).filter (x ≤ ·)
  finsetIoc x y := (Iic y).filter (x < ·)
  finsetIoo x y := (Iio y).filter (x < ·)
  finset_mem_Icc := by simp [and_comm]
  finset_mem_Ico := by simp [and_comm]
  finset_mem_Ioc := by simp [and_comm]
  finset_mem_Ioo := by simp [and_comm]

-- shouldn't be an instnace
def LocallyFiniteOrderBot.toOrderBot
    (ι : Type*) [LinearOrder ι] [LocallyFiniteOrderBot ι] [Inhabited ι] :
    OrderBot ι where
  bot := (Iic default).min' ⟨default, by simp⟩
  bot_le i :=  le_of_not_gt fun hi ↦ not_le_of_gt hi <| min'_le _ _ <| mem_Iic.mpr <|
    hi.le.trans <| min'_le _ _ <| by simp