Zulip Chat Archive

Stream: new members

Topic: Intro-have


Wojciech Nawrocki (Nov 23 2022 at 23:43):

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

Eric Wieser (Nov 24 2022 at 00:35):

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 (Nov 24 2022 at 02:03):

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

Wojciech Nawrocki (Nov 24 2022 at 02:04):

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 (Nov 24 2022 at 03:02):

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 (Nov 24 2022 at 07:17):

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 (Nov 24 2022 at 09:19):

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


Last updated: Dec 20 2023 at 11:08 UTC