iff with ∃ on both sides

Stream: new members

[Heather Macbeth]

Is there a more efficient way to do this?

import data.equiv.basic

example (A : Type*) (B : Type*) (f : equiv A B) (P : B → Prop) : (∃ a, P (f a)) ↔ (∃ b, P b) :=
begin
  split,
  { rintros ⟨a, ha⟩,
    use [f a, ha] },
  { rintros ⟨b, hb⟩,
    use f.symm b,
    simpa using hb }
end

[Patrick Massot]

tauto can do the first implication.

[Heather Macbeth]

I was hoping for something that doesn't involve a split ...

[Patrick Massot]

I was hoping equiv_rw would help, but it doesn't.

[Yury G. Kudryashov]

There should be a lemma in data.equiv.basic

[Yury G. Kudryashov]

And there should be a lemma in the namespace function.surjective

[Yury G. Kudryashov]

Let's try docs#function.surjective.exists

[Yury G. Kudryashov]

(deleted)

[Yury G. Kudryashov]

We have docs#equiv.forall_congr but not equiv.exists_congr.

[Heather Macbeth]

I guess that's ok?

example (A : Type*) (B : Type*) (f : equiv A B) (P : B → Prop) : (∃ b, P b) ↔ (∃ a, P (f a)) :=
function.surjective.exists (equiv.surjective f)

is pretty short!

[Rob Lewis]

Or even shorter, f.surjective.exists?

[Heather Macbeth]

Oops, yes!

[Anatole Dedecker]

Dot notation is awesome

[Yury G. Kudryashov]

Rob Lewis said:

Or even shorter, f.surjective.exists?

That's why the lemma is called function.surjective.exists instead of exists_congr_of_surjective.

[Rob Lewis]

Yury G. Kudryashov said:

That's why the lemma is called function.surjective.exists instead of exists_congr_of_surjective.

Yeah, proofs like that really show off all the work you put into renaming and refactoring!