# Re: [isabelle] "PROOF FAILED for depth4"

```Hi Steve,

```
```lemma te_zero: "EX func t. func t = 0"
proof
show "F s = 0"

*** Local statement will fail to refine any pending goal
```
```
```
The implicit step at the "proof" command introduces one existential quantifier. Thus, in the body, you are expected to prove "EX t. ?func t = 0" which does not match what you have in your show-statement. When experimenting, you can look at the goal state to see what you are expected to prove at a given point.
```
Here are a few options that work:

```
* Replace the implicit step with an explicit method, which does what you need:
```
lemma te_zero: "EX func t. func t = 0"
proof (intro exI)
show "F s = 0"

* Explicitly decompose the goal step by step (tedious):

lemma te_zero: "EX func t. func t = 0"
proof
show "EX t. F t = 0"
proof
show "F s = 0"
...

qed
qed

* Use an intermediate statement and let automation deal with quantifiers:

lemma te_zero: "EX func t. func t = 0"
proof -
have "F s = 0"
...

then show ?thesis by blast
qed

What you use depends on taste and the concrete problem.

```
```