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

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

State before:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ decide (p (find p h)) = true
Tactic:
apply bfind_prop (λ n => decide (p n))
State after:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ ∃ n, decide (p n) = true

State before:
case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ ∃ 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
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
n : Nat
hn : p n
⊢ decide (p n) = true

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