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?
use works in Eisbach. In general:
apply (use fact* in \<open>tactic\<close>)
so in your case:
apply (use my_inductive_case in fast)
Last updated: Dec 07 2023 at 20:16 UTC