exists iff exists

Stream: Is there code for X?

[Moritz Doll]

Is there a more concise way to prove the following? I would expect that there is a lemma for that, but library_search did not find anything.

example {R : Type*} {p q : R → Prop} (h : ∀ (r : R), p r ↔ q r) :
  (∃ (r : R), p r) ↔ ∃ (r : R), q r :=
begin
  split; rintro ⟨r, hr⟩; use r,
  { exact (h r).mp hr },
  { exact (h r).mpr hr }
end

[Yaël Dillies]

docs#exists_congr or simp_rw h

[Yaël Dillies]

There are also variants for nested existentials. See docs#exists₂_congr. Each direction is docs#Exists.imp (and variants docs#Exists₂.imp, etc...).

[Moritz Doll]

I had no idea that simp_rw is so powerful, thank you.