Theorem: Nat.bfind_le_of_prop (GMLInit/Data/Nat/Find.lean)

State before:
p : Nat → Bool
h : ∃ n, p n = true
x : Nat
⊢ p x = true → bfind p h ≤ x
Tactic:
intro h
State after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ bfind p h✝ ≤ x

State before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ bfind p h✝ ≤ x
Tactic:
apply Nat.le_of_not_gt
State after:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ ¬bfind p h✝ > x

State before:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
⊢ ¬bfind p h✝ > x
Tactic:
intro (hlt:_ < _)
State after:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ False

State before:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ False
Tactic:
apply not_prop_of_lt_bfind hlt
State after:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ p x = true

State before:
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ p x = true
Tactic:
exact h
State after:
no goals