Stream: Beginner Questions

Topic: Using insert on just one subgoal

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

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)

Mark Wassell (Nov 06 2020 at 13:16):

Thanks

Last updated: Dec 21 2024 at 12:33 UTC