conditional iff

Stream: Is there code for X?

[Peter Nelson]

Is there something tantamount to the following easily proved lemma in mathlib?

example (p q r : Prop) (hpr : p → r) (hqr : q → r) (h : r → (p ↔ q)) : (p ↔ q) := sorry

It's easy enough to prove, but I'm hoping there is a prepackaged version somewhere.

[Matthew Ballard]

aesop?

[Peter Nelson]

Yes, or tauto also works. But I want to use it to introduce a hypothesis r implied by both p and q to prove a p ↔ q goal in a tactic state where r doesn't yet appear. So I can't expect a tactic just to guess r, and I don't want to give the above lemma explicitly as a type annotation.

[Matthew Ballard]

aesop? nor exact? return any exact match

[Kevin Buzzard]

If you have a genuine need for this lemma then just PR it to Logic.Basic I guess.

[Eric Wieser]

Presumably it's worth having the marginally stronger

lemma imp_iff_iff_of_imp (p q r : Prop) (hpr : p → r) (hqr : q → r) : (r → (p ↔ q)) ↔ (p ↔ q) := sorry

where the reverse direction is trivial