awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : Epi f
m : (↑B.toLinOrd : Type u)
hm :
  ∀ (a : (↑A.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 : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
        a ≠
      m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ False
have h : 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)) p₁ :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
      m :
    (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)) p₂ :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
      m :
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
Tactic: have h : p₁ m = p₂ m := by
      congr
      rw [← cancel_epi f]
      ext a : 3
      simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]
      change ite _ _ _ = ite _ _ _
      split_ifs with h₁ h₂ h₂
      any_goals rfl
      · exfalso
        exact h₂ (le_of_lt h₁)
      · exfalso
        exact hm a (eq_of_le_of_not_lt h₂ h₁)
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
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)
have hf₁ : Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) 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)
Tactic: rw [epi_iff_surjective] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
⊢ IsSplitEpi f
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
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)
⊢ IsSplitEpi f
have 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
Tactic: have hφ : ∀ y : Y, f (φ y) = y := fun y => (H y).some.2
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
have refine_1 : Monotone φ
Tactic: refine IsSplitEpi.mk' ⟨ofHom ⟨φ, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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 φ
⊢ IsSplitEpi f
have refine_2 : ofHom { toFun := φ, monotone' := sorry } ≫ f = 𝟙 Y
Tactic: refine IsSplitEpi.mk' ⟨ofHom ⟨φ, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
⊢ ofHom { toFun := φ, monotone' := ⋯ } ≫ f = 𝟙 Y
have refine_2 : ∀ (b : (↑Y.toLinOrd : Type u)),
  Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (InducedCategory.Hom.hom (ofHom { toFun := φ, monotone' := sorry } ≫ 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: ext b
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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)
⊢ a ≤ b → φ a ≤ φ b
have refine_1 : ¬φ a ≤ φ b → ¬a ≤ b
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
⊢ ¬a ≤ b
have refine_1 : ∀ (h : φ b < φ a), b < a
Tactic: simp only [not_le] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
⊢ b < a
have apply : b ≠ a
Tactic: apply lt_of_le_of_ne this
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
⊢ b < a
have refine_1 : b ≤ a
Tactic: suffices b ≤ a by
        apply lt_of_le_of_ne this
        rintro rfl
        exfalso
        simp at h
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
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
⊢ b ≤ a
have 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)
Tactic: have H : f (φ b) ≤ f (φ a) := f.hom.hom.monotone (le_of_lt h)
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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)
⊢ 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)
have left : Membership.mem (γ := Set ((fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) X)) ⊤ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
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
⊢ 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)
have 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)
Tactic: tauto