extracting information from hypothesis

Stream: new members

[Elias Fåkvam]

Given the two hypotheses:

x: Z
h1: x ∈ {b : Z | ∃ (a : X), a ∈ S ∧ (g ∘ f) a = b}

I would like to extract the following hypothesis:

∃ (a : X), a ∈ S ∧ (g ∘ f) a = x

How can i do this?

[Kevin Buzzard]

cases h1 with a ha shows you that h1 is already this.

[Kevin Buzzard]

#mwe is best btw

[Kevin Buzzard]

Oh if you just want the existence statement, that is by definition h1 so you can just use change. Alternatively you can just pretend that h1 is what you want it to say. Can you write a #mwe? i.e. put in all the imports and the variables etc