Set g to be the term inv_fun_graph X f Y.

We use g to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (compact_to_Hausdorff_inverse_continuous X Tx Y Ty f Hcomp HH Hcont Hbij).

Let x be given.

Assume Hx: x ∈ X.

We will prove apply_fun g (apply_fun f x) = x.

We prove the intermediate claim Hfun: function_on f X Y.

An exact proof term for the current goal is (andEL (function_on f X Y) (∀y : set, y ∈ Y → ∃x0 : set, x0 ∈ X ∧ apply_fun f x0 = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x0)) Hbij).

We prove the intermediate claim HyY: apply_fun f x ∈ Y.

An exact proof term for the current goal is (Hfun x Hx).

We prove the intermediate claim Hginv: apply_fun g (apply_fun f x) = inv X (λu : set ⇒ apply_fun f u) (apply_fun f x).

An exact proof term for the current goal is (inv_fun_graph_apply X Y f (apply_fun f x) HyY).

rewrite the current goal using Hginv (from left to right).

We prove the intermediate claim Hinj: ∀u v ∈ X, apply_fun f u = apply_fun f v → u = v.

Let u be given.

Assume Hu: u ∈ X.

Let v be given.

Assume Hv: v ∈ X.

Assume Heq.

An exact proof term for the current goal is (bijection_inj X Y f u v Hbij Hu Hv Heq).

An exact proof term for the current goal is (inj_linv X (λu : set ⇒ apply_fun f u) Hinj x Hx).

Let y be given.

Assume Hy: y ∈ Y.

We will prove apply_fun f (apply_fun g y) = y.

We prove the intermediate claim Hginv: apply_fun g y = inv X (λu : set ⇒ apply_fun f u) y.

An exact proof term for the current goal is (inv_fun_graph_apply X Y f y Hy).

rewrite the current goal using Hginv (from left to right).

We prove the intermediate claim Hsurj: ∀w ∈ Y, ∃u ∈ X, apply_fun f u = w.

Let w be given.

Assume Hw: w ∈ Y.

We prove the intermediate claim Hex: ∃u : set, u ∈ X ∧ apply_fun f u = w.

An exact proof term for the current goal is (bijection_surj X Y f w Hbij Hw).

An exact proof term for the current goal is Hex.

We prove the intermediate claim Hpair: inv X (λu : set ⇒ apply_fun f u) y ∈ X ∧ apply_fun f (inv X (λu : set ⇒ apply_fun f u) y) = y.

An exact proof term for the current goal is (surj_rinv X Y (λu : set ⇒ apply_fun f u) Hsurj y Hy).

An exact proof term for the current goal is (andER (inv X (λu : set ⇒ apply_fun f u) y ∈ X) (apply_fun f (inv X (λu : set ⇒ apply_fun f u) y) = y) Hpair).