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

State before:
p : Nat → Bool
h : ∃ n, p n = true
⊢ p (bfind p h) = true
Tactic:
have : (first p).leNat (bfind p h) := by
  unfold bfind
  rw [leNat_toNat]
State after:
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
⊢ p (bfind p h) = true

State before:
p : Nat → Bool
h : ∃ n, p n = true
⊢ (first p).leNat (bfind p h) = true
Tactic:
unfold bfind
State after:
p : Nat → Bool
h : ∃ n, p n = true
⊢ (first p).leNat ((first p).toNat ⋯) = true

State before:
p : Nat → Bool
h : ∃ n, p n = true
⊢ (first p).leNat ((first p).toNat ⋯) = true
Tactic:
rw [leNat_toNat]
State after:
no goals

State before:
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
heq : x = bfind p h
⊢ p (bfind p h) = true
Tactic:
rw [←heq, hx]
State after:
no goals

State before:
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x = bfind p h
Tactic:
antisymmetry using (.≤.:Nat→Nat→Prop)
State after:
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x ≤ bfind p h

case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ bfind p h ≤ x

State before:
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x ≤ bfind p h
Tactic:
exact hle
State after:
no goals

State before:
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ bfind p h ≤ x
Tactic:
exact bfind_le_of_prop hx
State after:
no goals