-- Module: Mathlib.Order.Category.PartOrd
Goal:
X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
x :
  (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
        str := instPartialOrderAntisymmetrization } :
    Type u)
hf :
  ∀ (a : (↑X : Type u)),
    Eq (α :=
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
      ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          (Quotient.mk'' a) :
        (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
      ((PartOrd.Hom.hom
              (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫
                PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          (Quotient.mk'' a) :
        (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
⊢ Eq (α :=
    (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      Type u))
    ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        x :
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
    ((PartOrd.Hom.hom
            (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫
              PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        x :
      (↑{ carrier := Antisymmetrization (↑Z : Type u) fun (x1 x2 : (↑Z : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))

Tactic:
induction x using Quotient.inductionOn'