Intro-have

Stream: new members

[Wojciech Nawrocki]

Is there a tactic to go from the goal ⊢ P → Q to h : myThm P ⊢ Q in a single step?

[Eric Wieser]

Can you write that as a #mwe? Right now what you've written is false if myThm = λ _, false, so I suspect you meant something different to what you wrote

[Wojciech Nawrocki]

Oh :face_palm: I meant h : _ := myThm (hP : P) ⊢ Q.

[Wojciech Nawrocki]

In other words, a shorthand for

example {P Q R : Prop} (myThm : P → R) : P → Q := by
  intro hP
  have h := myThm hP
  clear hP
  ...

[Jireh Loreaux]

well, it's still two tactics, but intro h; replace h := myThm h works (if replace has been ported, I'm not sure).

[Jireh Loreaux]

Of course, you could just do it with refine

example {P Q R : Prop} (myThm : P → R) : P → Q := by
  refine (fun hr => ?_).comp myThm
  sorry

[Eric Wieser]

There is a thread proposing an apply at tactic such that you could write apply myThm at hP, but you'd still need a separate intro tactic