Let X, Y, f, g, Q, q and fac be given.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE.
Apply HE to the current goal.
Assume HE1: Obj X.
Assume HE2: Obj Y.
Assume HE3: Hom X Y f.
Assume HE4: Hom X Y g.
Assume HE5: Obj Q.
Assume HE6: Hom Q X q.
Assume HE7: comp Q X Y f q = comp Q X Y g q.
Assume HE8: ∀W : set, Obj W → ∀h : set, Hom W X h → comp W X Y f h = comp W X Y g h → Hom W Q (fac W h) ∧ comp W Q X q (fac W h) = h ∧ ∀u : set, Hom W Q u → comp W Q X q u = h → u = fac W h.
We will prove Obj Y ∧ Obj X ∧ Hom X Y f ∧ Hom X Y g ∧ Obj Q ∧ Hom Q X q ∧ comp Q X Y f q = comp Q X Y g q ∧ ∀W : set, Obj W → ∀h : set, Hom W X h → comp W X Y f h = comp W X Y g h → Hom W Q (fac W h) ∧ comp W Q X q (fac W h) = h ∧ ∀u : set, Hom W Q u → comp W Q X q u = h → u = fac W h.
Apply and8I to the current goal.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HE3.
An exact proof term for the current goal is HE4.
An exact proof term for the current goal is HE5.
An exact proof term for the current goal is HE6.
An exact proof term for the current goal is HE7.
An exact proof term for the current goal is HE8.