Let X, Y, f and y be given.
Assume Hbij: bijection X Y f.
Assume Hy: y ∈ Y.
We will prove apply_fun f (apply_fun (inv_fun_graph X f Y) y) = y.
We prove the intermediate claim Hginv: apply_fun (inv_fun_graph X f Y) 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).
∎