IsLeast Nat.find

Stream: mathlib4

[Jireh Loreaux]

Should we have these, or is it pointless?

import Mathlib

lemma Nat.isLeast_find {p : ℕ → Prop} [DecidablePred p] (hp : ∃ n, p n) :
    IsLeast {n | p n} (Nat.find hp) :=
  ⟨Nat.find_spec hp, fun _ ↦ Nat.find_min' hp⟩

lemma Set.Nonempty.isLeast_natFind {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : s.Nonempty) :
    IsLeast s (Nat.find hs) :=
  Nat.isLeast_find hs

[Johan Commelin]

lgtm

[Jireh Loreaux]

Happy to do it, but not sure where to put it. #min_imports says:

import Mathlib.Data.Nat.Find
import Mathlib.Order.Bounds.Defs

and it doesn't look like either of those should import the other. Meanwhile #find_home Nat.isLeast_find returns

[Mathlib.Logic.Encodable.Basic, Mathlib.GroupTheory.FreeGroup.Reduce,
Mathlib.Data.Finset.Powerset, Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv,
Mathlib.Algebra.ContinuedFractions.Determinant, Mathlib.Algebra.CharP.Defs,
Mathlib.Data.Countable.Basic, Mathlib.Tactic.IntervalCases, Mathlib.Data.Sym.Basic,
Mathlib.Algebra.Group.Pointwise.Set.ListOfFn, Mathlib.Algebra.ContinuedFractions.Computation.Basic,
Mathlib.Algebra.Order.Archimedean.Basic, Mathlib.Data.Num.Prime,
Mathlib.Data.Int.ConditionallyCompleteOrder, Mathlib.Order.SuccPred.Tree, Mathlib.Data.Fintype.Sigma,
Mathlib.Order.Fin.Tuple, Mathlib.SetTheory.ZFC.Basic, Mathlib.CategoryTheory.Limits.Shapes.SingleObj,
Mathlib.CategoryTheory.ComposableArrows, Mathlib.Control.LawfulFix, Mathlib.Data.List.Sort]

and none of those look good.

[Ruben Van de Velde]

Yeah. New file?

[Eric Wieser]

Can we do the same for docs#Int.greatestOfBdd ?

[Yaël Dillies]

This should be in Order.Nat

[Jireh Loreaux]

Oh, I didn't realize we hit 20000 PRs overnight. Woot!

[Jireh Loreaux]

#20010 for the IsLeast lemmas. There were new imports needed, but for the most part it was just Order.Bounds.Defs, which is only a Defsfile.