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

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

State before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < bfind p h✝
h : p x = true
⊢ False
Tactic:
unfold bfind at hlt
State after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ False

State before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ False
Tactic:
apply Nat.not_le.2 hlt
State after:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).toNat ⋯ ≤ x

State before:
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).toNat ⋯ ≤ x
Tactic:
apply toNat_le_of_leNat
State after:
case h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).leNat x = true

State before:
case h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).leNat x = true
Tactic:
apply first_leNat_of
State after:
case h.h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ p x = true

State before:
case h.h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ p x = true
Tactic:
exact h
State after:
no goals