-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
I : NonemptyFinLinOrd :=
  of
    (↑(Set.image (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
                (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
                (↑X.toLinOrd : Type u)) f) :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          ⊤) :
      Type u)
x : (↑X.1 : Type u)
left : Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)) ⊤ x
right :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        x :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        x :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
left₁ left₂ left₃ : Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)) ⊤ x
right₁ right₂ right₃ :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        x :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        x :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
left₄ left₅ : Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)) ⊤ x
right₄ :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        x :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        x :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
⊢ Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)) ⊤ x ∧
    Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
              (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
              (↑X.toLinOrd : Type u)) f :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          x :
        (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
              (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
              (↑X.toLinOrd : Type u)) f :
            (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
              (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
          x :
        (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)

Tactic:
tauto