extract `imp` from `iff`

Stream: general

[Scott Morrison]

I'd like a function meta imp_of_iff : expr -> tactic expr, that takes a lemma that says, \Pi (...), P \iff Q, and gives me instead the lemma \Pi (...), P \to Q. Has anyone seen this lying around somewhere in mathlib? It's probably not too hard, I'm just hoping it's already done!

[Scott Morrison]

Ugh, okay, I revise that, I'm finding it hard. :-)

[Scott Morrison]

Ah, maybw tactic/alias.lean has mk_iff_mp_app, which seems promising.

[Scott Morrison]

Hmm, not clear that helps, it seems tied to actual declarations.

[Scott Morrison]

Sorted it out. tactic/alias.lean has everything I need.