Is there something like `apply` for Exists?

Stream: new members

[Dan Abramov]

Here's a little example where I need to present a certain B which I can obtain by transforming some A through f:

def A : Type := sorry
def B : Type := sorry
def makeA : A := sorry
def f : A → B := sorry
def P : B → Prop := sorry
def proofP b : P b := sorry

theorem foo : (∃ (b: B), P b) := by
  use f makeA
  apply proofP

What I'm wondering is, is there some built-in way or convention to turn goals like ∃ (b: B) into ∃ (a: A) automatically given f?

I can do this manually of course:

theorem foo' : (∃ (b: B), P b) := by
  -- change the goal:
  suffices : ∃ (a: A), P (f a); choose a ha using this; use f a
  -- keep going:
  use makeA
  apply proofP

but I was wondering if there's any idiom for that. This is similar to how I could just apply f if my goal was just B.

[Paul Reichert]

I wouldn't say it's an idiom, you could use Exists.imp':

theorem foo'' : (∃ (b: B), P b) := by
  apply Exists.imp' f (fun _ => id) -- after this, the goal is what you desire
  exact ⟨makeA, proofP _⟩