Let X, Y and g be given.
Assume HgBij: bij X Y g.
We prove the intermediate claim Hmap: ∀u ∈ X, g u ∈ Y.
An exact proof term for the current goal is (and3E (∀u ∈ X, g u ∈ Y) (∀u v ∈ X, g u = g v → u = v) (∀w ∈ Y, ∃u ∈ X, g u = w) HgBij (∀u ∈ X, g u ∈ Y) (λH1 H2 H3 ⇒ H1)).
We prove the intermediate claim Hinj: ∀u v ∈ X, g u = g v → u = v.
An exact proof term for the current goal is (and3E (∀u ∈ X, g u ∈ Y) (∀u v ∈ X, g u = g v → u = v) (∀w ∈ Y, ∃u ∈ X, g u = w) HgBij (∀u v ∈ X, g u = g v → u = v) (λH1 H2 H3 ⇒ H2)).
We prove the intermediate claim Hsurj: ∀w ∈ Y, ∃u ∈ X, g u = w.
An exact proof term for the current goal is (and3E (∀u ∈ X, g u ∈ Y) (∀u v ∈ X, g u = g v → u = v) (∀w ∈ Y, ∃u ∈ X, g u = w) HgBij (∀w ∈ Y, ∃u ∈ X, g u = w) (λH1 H2 H3 ⇒ H3)).
We will prove function_on (graph X g) X Y ∧ (∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun (graph X g) x = y ∧ (∀x' : set, x' ∈ X → apply_fun (graph X g) x' = y → x' = x)).
Apply andI to the current goal.
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using (apply_fun_graph X g x HxX) (from left to right).
An exact proof term for the current goal is (Hmap x HxX).
Let y be given.
Assume HyY: y ∈ Y.
We prove the intermediate claim Hex: ∃x0 : set, x0 ∈ X ∧ g x0 = y.
An exact proof term for the current goal is (Hsurj y HyY).
Apply Hex to the current goal.
Let x0 be given.
Assume Hx0pair.
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (x0 ∈ X) (g x0 = y) Hx0pair).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (andEL (x0 ∈ X) (g x0 = y) Hx0pair).
rewrite the current goal using (apply_fun_graph X g x0 Hx0X) (from left to right).
An exact proof term for the current goal is (andER (x0 ∈ X) (g x0 = y) Hx0pair).
Let x' be given.
Assume Hx'X: x' ∈ X.
Assume Hx'Eq: apply_fun (graph X g) x' = y.
We prove the intermediate claim Hgx': g x' = y.
rewrite the current goal using (apply_fun_graph X g x' Hx'X) (from right to left).
An exact proof term for the current goal is Hx'Eq.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (andEL (x0 ∈ X) (g x0 = y) Hx0pair).
We prove the intermediate claim Hgx0: g x0 = y.
An exact proof term for the current goal is (andER (x0 ∈ X) (g x0 = y) Hx0pair).
We prove the intermediate claim Hgx'x0: g x' = g x0.
rewrite the current goal using Hgx0 (from left to right).
An exact proof term for the current goal is Hgx'.
An exact proof term for the current goal is (Hinj x' Hx'X x0 Hx0X Hgx'x0).
∎