Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ real.
Apply SepI to the current goal.
An exact proof term for the current goal is real_complex x Hx.
An exact proof term for the current goal is real_Re_eq x Hx.
Let z be given.
Assume Hz: z ∈ {z ∈ complex|Re z = z}.
Apply SepE complex (λz ⇒ Re z = z) z Hz to the current goal.
Assume Hz1: z ∈ complex.
Assume Hz2: Re z = z.
We will prove z ∈ real.
rewrite the current goal using Hz2 (from right to left).
An exact proof term for the current goal is complex_Re_real z Hz1.
∎