Stream: Beginner Questions

Topic: Using insert on just one subgoal


view this post on Zulip Mark Wassell (Nov 06 2020 at 12:14):

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

view this post on Zulip Mathias Fleury (Nov 06 2020 at 12:42):

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)

view this post on Zulip Mark Wassell (Nov 06 2020 at 13:16):

Thanks


Last updated: Aug 15 2022 at 02:13 UTC