-- Lean 4 proof step from Mathlib.Order.Category.PartOrd (goal)
Goal:
X : Preord
x :
  (↑{ 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))
have 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))
Tactic: induction x using Quotient.inductionOn'
Cleared hypotheses: x