awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
⊢ ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)

Tactic:
have H : ∀ y : Y, Nonempty (f ⁻¹' {y}) := by
      rw [epi_iff_surjective] at hf
      intro y
      exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
⊢ ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y

Tactic:
have hφ : ∀ y : Y, f (φ y) = y := fun y => (H y).some.2
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
⊢ IsSplitEpi f

Tactic:
IsSplitEpi.mk' ⟨ofHom ⟨φ, ?_⟩, ?_⟩

Premises used: NonemptyFinLinOrd.ofHom, CategoryTheory.SplitEpi.mk, OrderHom.mk, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
refine_1 : Monotone φ
refine_2 : ofHom { toFun := φ, monotone' := ⋯ } ≫ f = 𝟙 Y
⊢ IsSplitEpi f

Tactic:
refine IsSplitEpi.mk' ⟨ofHom ⟨φ, ?_⟩, ?_⟩

Premises used: NonemptyFinLinOrd.ofHom, CategoryTheory.SplitEpi.mk, OrderHom.mk, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
refine_2 :
  ∀ (b : (↑Y.toLinOrd : Type u)),
    Eq (α := (↑Y.toLinOrd : Type u))
      ((LinOrd.Hom.hom (InducedCategory.Hom.hom (ofHom { toFun := φ, monotone' := ⋯ } ≫ f)) :
            (a : (↑Y.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
          b :
        (↑Y.toLinOrd : Type u))
      ((LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 Y)) : (a : (↑Y.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) b :
        (↑Y.toLinOrd : Type u))
⊢ ofHom { toFun := φ, monotone' := ⋯ } ≫ f = 𝟙 Y

Tactic:
ext b
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
b : (↑Y.toLinOrd : Type u)
⊢ Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (InducedCategory.Hom.hom (ofHom { toFun := φ, monotone' := ⋯ } ≫ f)) :
          (a : (↑Y.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        b :
      (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 Y)) : (a : (↑Y.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) b :
      (↑Y.toLinOrd : Type u))

Tactic:
apply hφ
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
a b : (↑Y.1 : Type u)
refine_1 : ¬φ a ≤ φ b → ¬a ≤ b
⊢ a ≤ b → φ a ≤ φ b

Tactic:
contrapose
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
a b : (↑Y.1 : Type u)
h : ¬φ a ≤ φ b
refine_1 : ∀ (h : φ b < φ a), b < a
⊢ ¬a ≤ b

Tactic:
simp only [not_le] at h ⊢

Premises used: not_le
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
a b : (↑Y.1 : Type u)
h : φ b < φ a
this : b ≤ a
apply : b ≠ a
⊢ b < a

Tactic:
apply lt_of_le_of_ne this

Premises used: lt_of_le_of_ne
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
b : (↑Y.1 : Type u)
h : φ b < φ b
this : b ≤ b
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
a b : (↑Y.1 : Type u)
h : φ b < φ a
refine_1 : b ≤ a
⊢ b < a

Tactic:
suffices b ≤ a by
        apply lt_of_le_of_ne this
        rintro rfl
        exfalso
        simp at h
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
a b : (↑Y.1 : Type u)
h : φ b < φ a
⊢ LE.le (α := (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)
        (φ b) :
      (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)
        (φ a) :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)

Tactic:
have H : f (φ b) ≤ f (φ a) := f.hom.hom.monotone (le_of_lt h)
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H_1 :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    Nonempty.{u + 1}
      (↑(Set.preimage (β := (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)
            {y}) :
        Type u)
φ : (↑Y.toLinOrd : Type u) → (↑X.toLinOrd : Type u) :=
  fun (y : (↑Y.toLinOrd : Type u)) ↦ (↑⋯.some : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X)
hφ :
  ∀ (y : (↑Y.toLinOrd : Type u)),
    (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)
        (φ y) =
      y
a b : (↑Y.1 : Type u)
h : φ b < φ a
H :
  LE.le (α := (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)
        (φ b) :
      (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)
        (φ a) :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
⊢ b ≤ a

Tactic:
simpa only [hφ] using H
-- 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)
e : X ⟶ I :=
  ofHom
    {
      toFun := fun (x : (↑X.1 : Type u)) ↦
        Subtype.mk (p := fun (x : (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y) ↦
          Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y))
            (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)
              ⊤)
            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)
            x)
          ⋯,
      monotone' := ⋯ }
m : I ⟶ Y :=
  ofHom
    {
      toFun :=
        fun
          (y :
            (↑(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)) ↦
        (↑y : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y),
      monotone' := ⋯ }
rw :
  Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X) (β :=
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) I)
    (⇑(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)) e) :
      (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
        (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) I)
⊢ Epi e

Tactic:
rw [epi_iff_surjective]

Premises used: NonemptyFinLinOrd.epi_iff_surjective