Induction on new variable

Stream: Berkeley Lean Seminar

[Thomas Browning]

If my goal is x and I have a hypothesis h, is there a way to turn the goal into h -> x ?

[Patrick Lutz]

This doesn't exactly answer your question, but you could first use have h' : h \to x and then supply a proof and then exact h' h

[Patrick Lutz]

well, more like have h' : A \to B where A and B are the types of h and x

[Patrick Lutz]

but maybe there's a better way to do it

[Pedro Minicz]

You can use revert h, this will eliminate the hypothesis from the context and "add" it to the goal.