awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
e_a :
  Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (ofHom
                { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 },
                  monotone' := ⋯ })) :
          (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
      (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (ofHom
                { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 },
                  monotone' := ⋯ })) :
          (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
      (↑Y.toLinOrd : Type u))
⊢ Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (f ≫ p₁).hom : (a : (↑A.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) a : (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (f ≫ p₂).hom : (a : (↑A.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) a : (↑Y.toLinOrd : Type u))

Tactic:
simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]

Premises used: OrderHom.comp_coe, NonemptyFinLinOrd.hom_hom_comp, Function.comp_apply
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
e_a :
  Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
    else { down := 1 })
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
    else { down := 1 })
⊢ Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (ofHom
                { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 },
                  monotone' := ⋯ })) :
          (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
      (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (ofHom
                { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 },
                  monotone' := ⋯ })) :
          (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
      (↑Y.toLinOrd : Type u))

Tactic:
change ite _ _ _ = ite _ _ _

Premises used: ite
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
pos :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 0 }
neg :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 1 }
pos₁ :
  ∀ (h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 1 } { down := 0 }
neg₁ :
  ∀ (h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 1 } { down := 1 }
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
    else { down := 1 })
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
    else { down := 1 })

Tactic:
split_ifs with h₁ h₂ h₂
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 0 }

Tactic:
rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 1 } { down := 1 }

Tactic:
rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
neg : False
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 1 }

Tactic:
exfalso
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ False

Tactic:
h₂ (le_of_lt h₁)

Premises used: le_of_lt
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ False

Tactic:
exact h₂ (le_of_lt h₁)

Premises used: le_of_lt
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
pos : False
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 1 } { down := 0 }

Tactic:
exfalso
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ False

Tactic:
hm a (eq_of_le_of_not_lt h₂ h₁)

Premises used: eq_of_le_of_not_lt
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ False

Tactic:
exact hm a (eq_of_le_of_not_lt h₂ h₁)

Premises used: eq_of_le_of_not_lt
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
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' := ⋯ }
⊢ 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₁)
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : 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' := ⋯ }
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)
⊢ False

Tactic:
simp [Y, p₁, p₂, ConcreteCategory.hom_ofHom] at h

Premises used: CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h :
  Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    (⇑(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)) A) →
        (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
⊢ Epi f

Tactic:
ConcreteCategory.epi_of_surjective f h

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h :
  Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    (⇑(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)) A) →
        (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
⊢ Epi f

Tactic:
exact ConcreteCategory.epi_of_surjective f h

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
⊢ 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

Premises used: NonemptyFinLinOrd.epi_iff_surjective
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
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)
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:
Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩

Premises used: Exists.choose_spec, Nonempty.intro, Subtype.mk, Exists.choose
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
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)
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:
exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩

Premises used: Nonempty.intro