Let X, Y, Z, f and g be given.
Assume Hf.
Apply Hf to the current goal.
Assume Hf12 Hf3.
Apply Hf12 to the current goal.
Assume Hf1 Hf2.
Assume Hg.
Apply Hg to the current goal.
Assume Hg12 Hg3.
Apply Hg12 to the current goal.
Assume Hg1 Hg2.
We will prove (∀u ∈ X, g (f u) ∈ Z) ∧ (∀u v ∈ X, g (f u) = g (f v) → u = v) ∧ (∀w ∈ Z, ∃u ∈ X, g (f u) = w).
Apply and3I to the current goal.
Let u be given.
Assume Hu: u ∈ X.
An exact proof term for the current goal is (Hg1 (f u) (Hf1 u Hu)).
Let u be given.
Assume Hu: u ∈ X.
Let v be given.
Assume Hv: v ∈ X.
Assume H1: g (f u) = g (f v).
We will prove u = v.
Apply Hf2 u Hu v Hv to the current goal.
We will prove f u = f v.
Apply Hg2 (f u) (Hf1 u Hu) (f v) (Hf1 v Hv) to the current goal.
We will prove g (f u) = g (f v).
An exact proof term for the current goal is H1.
Let w be given.
Assume Hw: w ∈ Z.
Apply Hg3 w Hw to the current goal.
Let y be given.
Assume Hy12.
Apply Hy12 to the current goal.
Assume Hy1: y ∈ Y.
Assume Hy2: g y = w.
Apply Hf3 y Hy1 to the current goal.
Let u be given.
Assume Hu12.
Apply Hu12 to the current goal.
Assume Hu1: u ∈ X.
Assume Hu2: f u = y.
We will prove ∃u ∈ X, g (f u) = w.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hu1.
rewrite the current goal using Hu2 (from left to right).
An exact proof term for the current goal is Hy2.
∎