FormalConjecturesForMathlib/Order/Nat.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Nat.find_of_isLeast line 25 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, DecidablePred, IsLeast, Set.ofPred, Eq, Nat.find, Exists.intro, And.left, Membership.mem, Set, lowerBounds

   Proof uses: Eq.mpr, And, LT.lt, Not, id, congrArg, propext, Nat.find_eq_iff, And.intro, LT.lt.not_ge, And.right

   6 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.