-- Module: Mathlib.Order.Category.PartOrd
Goal:
X : Preord
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 (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
      ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          (Quotient.mk'' a) :
        (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
      ((PartOrd.Hom.hom
              (𝟙
                { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization : PartOrd.{u} }) :
            (a :
                (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                      str := instPartialOrderAntisymmetrization } :
                  Type u)) →
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u))
          (Quotient.mk'' a) :
        (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
              str := instPartialOrderAntisymmetrization } :
          Type u))
⊢ Eq (α :=
    (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
          str := instPartialOrderAntisymmetrization } :
      Type u))
    ((PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        x :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))
    ((PartOrd.Hom.hom
            (𝟙
              { carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                str := instPartialOrderAntisymmetrization : PartOrd.{u} }) :
          (a :
              (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                    str := instPartialOrderAntisymmetrization } :
                Type u)) →
            (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
                  str := instPartialOrderAntisymmetrization } :
              Type u))
        x :
      (↑{ carrier := Antisymmetrization (↑X : Type u) fun (x1 x2 : (↑X : Type u)) ↦ x1 ≤ x2,
            str := instPartialOrderAntisymmetrization } :
        Type u))

Tactic:
induction x using Quotient.inductionOn'