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

State before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
⊢ p x → find p h ≤ x
Tactic:
intro hx
State after:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ find p h ≤ x

State before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ find p h ≤ x
Tactic:
apply bfind_le_of_prop
State after:
case h
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ ∃ n, decide (p n) = true

case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ decide (p x) = true

State before:
case h
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ ∃ n, decide (p n) = true
Tactic:
match h with | ⟨n, hn⟩ => exists n; exact decide_eq_true hn
State after:
no goals

State before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
n : Nat
hn : p n
⊢ ∃ n, decide (p n) = true
Tactic:
exists n
State after:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
n : Nat
hn : p n
⊢ decide (p n) = true

State before:
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
n : Nat
hn : p n
⊢ decide (p n) = true
Tactic:
exact decide_eq_true hn
State after:
no goals

State before:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ decide (p x) = true
Tactic:
exact decide_eq_true hx
State after:
no goals