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