Rewrite hypothesis to `True`/negation of hypothesis to `Fals

Stream: new members

[Alex Mobius]

Wondering if there's a better way to do stuff like this. My current project has a lot of iff lemmata (soundness of transformations), and with initial case analysis they mostly boil down to True iff True and False iff False. I know I can do things like constructor; intros; assumption; intros; assumption for the true case, but false case is uglier, so I'm wondering if there's a way to perform a targeted rewrite.
(speaking about targeted rewrites, is there just no way to get up in conv?)

example (P Q: Prop) (p: P) (q: Q): P ↔ Q := by
  have : P ↔ True := by rw [iff_true]; exact p
  rw [this]
  have : Q ↔ True := by rw [iff_true]; exact q
  rw [this]

[Ruben Van de Velde]

There's docs#iff_of_true / docs#iff_of_false

[Alex Mobius]

oh nice, applying those should do the trick! thanks!

[Alex Mobius]

iff_true_intro is the thing I was looking for!