Hi,

I am proving one of my subgoals with

```
using my_inductive_case apply fast
```

however I would like to be able to do this without 'using', so that I can incorporate it into an Eisbach proof method.

It seems that the fast proof method doesn't allow you to add facts like simp/auto do, and using the insert proof method does the insert to all subgoals, which makes solving later subgoals messy. Is there a way to make insert operate only on the first subgoal, or another way to get this subgoal proof into an Eisbach method?

Thanks

Mark

IIRC `use`

works in Eisbach. In general:

```
apply (use fact* in \<open>tactic\<close>)
```

so in your case:

```
apply (use my_inductive_case in fast)
```

Thanks

Last updated: Dec 07 2023 at 20:16 UTC