Let X, Y, f and x be given.

Assume Hbij: bijection X Y f.

Assume Hx: x ∈ X.

We will prove apply_fun (inv_fun_graph X f Y) (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 (inv_fun_graph X f Y) (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).

∎