awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (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)
        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)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
have eq : g₁ ≫ f = g₂ ≫ f := by
    ext
    exact h
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (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)
        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)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
eq : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
rw [cancel_mono] at eq

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
mp :
  Epi f →
    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)
mpr :
  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
⊢ Epi f ↔
    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)

Tactic:
constructor
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : Epi f
mp :
  ∀ (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),
    False
⊢ ∀ (b : (↑B.toLinOrd : Type u)),
    ∃ (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 =
        b

Tactic:
by_contra! ⟨m, hm⟩
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
simp :
  LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ < m then { down := 0 } else { down := 1 })
    (if x₂ < m then { down := 0 } else { down := 1 })
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2))
    ((fun (b : (↑B.1 : Type u)) ↦ (if b < m then { down := 0 } else { down := 1 } : ULift.{u, 0} (Fin 2))) x₁)
    ((fun (b : (↑B.1 : Type u)) ↦ (if b < m then { down := 0 } else { down := 1 } : ULift.{u, 0} (Fin 2))) x₂)

Tactic:
simp only
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
pos : ∀ (h₁ : x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }
neg : ∀ (h₁ : x₁ < m) (h₂ : ¬x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }
pos₁ : ∀ (h₁ : ¬x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }
neg₁ : ∀ (h₁ : ¬x₁ < m) (h₂ : ¬x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 1 }
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ < m then { down := 0 } else { down := 1 })
    (if x₂ < 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_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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }

Tactic:
apply Fin.zero_le

Premises used: Fin.zero_le
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : ¬x₂ < m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }

Tactic:
apply Fin.zero_le

Premises used: Fin.zero_le
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
pos : False
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }

Tactic:
exfalso
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ False

Tactic:
h₁ (lt_of_le_of_lt h h₂)

Premises used: lt_of_le_of_lt
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ False

Tactic:
exact h₁ (lt_of_le_of_lt h h₂)

Premises used: lt_of_le_of_lt
-- 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))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 1 }

Tactic:
rfl
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
simp :
  LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ ≤ m then { down := 0 } else { down := 1 })
    (if x₂ ≤ m then { down := 0 } else { down := 1 })
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2))
    ((fun (b : (↑B.1 : Type u)) ↦ (if b ≤ m then { down := 0 } else { down := 1 } : ULift.{u, 0} (Fin 2))) x₁)
    ((fun (b : (↑B.1 : Type u)) ↦ (if b ≤ m then { down := 0 } else { down := 1 } : ULift.{u, 0} (Fin 2))) x₂)

Tactic:
simp only
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
pos : ∀ (h₁ : x₁ ≤ m) (h₂ : x₂ ≤ m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }
neg : ∀ (h₁ : x₁ ≤ m) (h₂ : ¬x₂ ≤ m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }
pos₁ : ∀ (h₁ : ¬x₁ ≤ m) (h₂ : x₂ ≤ m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }
neg₁ : ∀ (h₁ : ¬x₁ ≤ m) (h₂ : ¬x₂ ≤ m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 1 }
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ ≤ m then { down := 0 } else { down := 1 })
    (if x₂ ≤ 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_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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }

Tactic:
apply Fin.zero_le

Premises used: Fin.zero_le
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }

Tactic:
apply Fin.zero_le

Premises used: Fin.zero_le
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
pos : False
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }

Tactic:
exfalso
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ False

Tactic:
h₁ (h.trans h₂)

Premises used: LE.le.trans
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ False

Tactic:
exact h₁ (h.trans h₂)

Premises used: LE.le.trans
-- 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' := ⋯ }
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { 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' := ⋯ }
e_a : p₁ = p₂
⊢ 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:
congr
-- 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' := ⋯ }
e_a : f ≫ p₁ = f ≫ p₂
⊢ p₁ = p₂

Tactic:
rw [← cancel_epi f]

Premises used: CategoryTheory.cancel_epi
-- 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' := ⋯ }
e_a :
  ∀ (a : (↑A.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))
⊢ f ≫ p₁ = f ≫ p₂

Tactic:
ext a : 3