awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.Lat
Goal:
X Y : Lat
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC :=
              carrier) e.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          s :
        (↑X : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Order.Category.Lat
Goal:
⊢ Lat.dual ⋙
      forget₂ Lat (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := Lat.carrier)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier) =
    forget₂ Lat (FC := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CC := Lat.carrier)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier) ⋙
      PartOrd.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, Lat.dual, OrderHomClass.toOrderHom, OrderDual, rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X : LinOrd
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y Z : LinOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : LinOrd
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget LinOrd (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget LinOrd (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)) Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget LinOrd (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget LinOrd).obj X)) → (fun (X : Type u_1) ↦ X) ((forget LinOrd).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          f) :
      (a : (↑X : Type u_1)) → (↑Y : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : LinOrd
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X : Type u
inst : LinearOrder X
⊢ (↑{ carrier := X, str := inst : LinOrd.{u} } : Type u) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X : LinOrd
⊢ Hom.hom (𝟙 X) = OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X : LinOrd
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y Z : LinOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y Z : LinOrd
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_1)
⊢ Eq (α := (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑Z : Type u_1))
        x :
      (↑Z : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier) g :
          (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
                f :
              (a : (↑X : Type u_1)) → (↑Y : Type u_1))
            x :
          (↑Y : Type u_1)) :
      (↑Z : Type u_1))

Tactic:
simp
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : LinOrd
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: LinOrd.Hom.ext
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : Type u
inst : LinearOrder X
inst_1 : LinearOrder Y
f : X →o Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : LinOrd
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X : Type u
inst : LinearOrder X
⊢ ofHom OrderHom.id = 𝟙 { carrier := X, str := inst : LinOrd.{u} }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y Z : Type u
inst : LinearOrder X
inst_1 : LinearOrder Y
inst_2 : LinearOrder Z
f : X →o Y
g : Y →o Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : Type u
inst : LinearOrder X
inst_1 : LinearOrder Y
f : X →o Y
x : X
⊢ Eq (α := (↑{ carrier := Y, str := inst_1 } : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u}) ↦ (↑x1 : Type u) →o (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑{ carrier := X, str := inst } : Type u)) → (↑{ carrier := Y, str := inst_1 } : Type u))
        x :
      (↑{ carrier := Y, str := inst_1 } : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : LinOrd
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              e.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.LinOrd
Goal:
X Y : LinOrd
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := carrier)
              e.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          s :
        (↑X : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Order.Category.LinOrd
Goal:
⊢ LinOrd.dual ⋙
      forget₂ LinOrd (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := LinOrd.carrier)
        Lat (FD := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := Lat.carrier) =
    forget₂ LinOrd (FC := fun (x1 x2 : LinOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CC := LinOrd.carrier) Lat
        (FD := fun (x1 x2 : Lat.{u_1}) ↦ LatticeHom (↑x1 : Type u_1) (↑x2 : Type u_1)) (CD := Lat.carrier) ⋙
      Lat.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, OrderHomClass.toLatticeHom, OrderDual, rfl, LinOrd.dual
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
α : Type u_1
inst : Nonempty α
inst_1 : Fintype α
inst_2 : LinearOrder α
⊢ (↑(of α).toLinOrd : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X : NonemptyFinLinOrd
⊢ LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 X)) = OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X : NonemptyFinLinOrd
x : (↑X.toLinOrd : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u_1}) ↦
          (↑x1.toLinOrd : Type u_1) →o (↑x2.toLinOrd : Type u_1)) (CC := fun (X : NonemptyFinLinOrd.{u_1}) ↦
          (↑X.toLinOrd : Type u_1)) (𝟙 X) :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) X) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) X)
      x =
    x

Tactic:
simp
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y Z : NonemptyFinLinOrd
f : X ⟶ Y
g : Y ⟶ Z
⊢ LinOrd.Hom.hom (f ≫ g).hom = (LinOrd.Hom.hom g.hom).comp (LinOrd.Hom.hom f.hom)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y Z : NonemptyFinLinOrd
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X.toLinOrd : Type u_1)
⊢ Eq (α := (fun (X : NonemptyFinLinOrd.{u_1}) ↦ (↑X.toLinOrd : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u_1}) ↦
            (↑x1.toLinOrd : Type u_1) →o (↑x2.toLinOrd : Type u_1)) (CC := fun (X : NonemptyFinLinOrd.{u_1}) ↦
            (↑X.toLinOrd : Type u_1)) (f ≫ g) :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) Z)
        x :
      (fun (X : NonemptyFinLinOrd.{u_1}) ↦ (↑X.toLinOrd : Type u_1)) Z)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u_1}) ↦
            (↑x1.toLinOrd : Type u_1) →o (↑x2.toLinOrd : Type u_1)) (CC := fun (X : NonemptyFinLinOrd.{u_1}) ↦
            (↑X.toLinOrd : Type u_1)) g :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) Y) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) Z)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u_1}) ↦
                (↑x1.toLinOrd : Type u_1) →o (↑x2.toLinOrd : Type u_1)) (CC := fun (X : NonemptyFinLinOrd.{u_1}) ↦
                (↑X.toLinOrd : Type u_1)) f :
              (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) X) →
                (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u_1)) Y)
            x :
          (fun (X : NonemptyFinLinOrd.{u_1}) ↦ (↑X.toLinOrd : Type u_1)) Y) :
      (fun (X : NonemptyFinLinOrd.{u_1}) ↦ (↑X.toLinOrd : Type u_1)) Z)

Tactic:
simp
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f g : X ⟶ Y
hf : LinOrd.Hom.hom f.hom = LinOrd.Hom.hom g.hom
⊢ f = g

Tactic:
InducedCategory.hom_ext (ConcreteCategory.ext hf)

Premises used: CategoryTheory.InducedCategory.hom_ext, CategoryTheory.ConcreteCategory.ext
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : Type u
inst : Nonempty X
inst_1 : LinearOrder X
inst_2 : Fintype X
inst_3 : Nonempty Y
inst_4 : LinearOrder Y
inst_5 : Fintype Y
f : X →o Y
⊢ LinOrd.Hom.hom (InducedCategory.Hom.hom (ofHom f)) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
X Y : NonemptyFinLinOrd
f : X ⟶ Y
⊢ ofHom (LinOrd.Hom.hom f.hom) = f

Tactic:
rfl

Premises used: CategoryTheory.InducedCategory.homMk, rfl
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Mono f ↔
    Function.Injective (α := (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:
⟨?_, ConcreteCategory.mono_of_injective f⟩

Premises used: Iff.intro, CategoryTheory.ConcreteCategory.mono_of_injective
-- Module: Mathlib.Order.Category.NonemptyFinLinOrd
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
refine :
  Mono f →
    Function.Injective (α := (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)
⊢ Mono f ↔
    Function.Injective (α := (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:
refine ⟨?_, ConcreteCategory.mono_of_injective f⟩
-- 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))
x x_1 : ULift.{u, 0} (Fin 1)
h_2 : x ≤ x_1
⊢ LE.le.{u} (α := (↑A.1 : Type u)) ((fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁) x) ((fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁) x)

Tactic:
rfl
-- 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' := ⋯ }
x x_1 : ULift.{u, 0} (Fin 1)
h_2 : x ≤ x_1
⊢ LE.le.{u} (α := (↑A.1 : Type u)) ((fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂) x) ((fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂) x)

Tactic:
rfl
-- 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' := ⋯ }
change :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((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)) g₁ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((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)) g₂ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
⊢ a₁ = a₂

Tactic:
change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))

Premises used: CategoryTheory.ConcreteCategory.hom, OfNat.ofNat, ULift.up, DFunLike.coe
-- 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' := ⋯ }
hf :
  ∀ (x : (↑X.toLinOrd : Type u)),
    Eq (α := (↑B.toLinOrd : Type u))
      ((LinOrd.Hom.hom (g₁ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))
      ((LinOrd.Hom.hom (g₂ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
ext
-- 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' := ⋯ }
x : (↑X.toLinOrd : Type u)
⊢ Eq (α := (↑B.toLinOrd : Type u))
    ((LinOrd.Hom.hom (g₁ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))
    ((LinOrd.Hom.hom (g₂ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))

Tactic:
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' := ⋯ }
x : (↑X.toLinOrd : Type u)
⊢ Eq (α := (↑B.toLinOrd : Type u))
    ((LinOrd.Hom.hom (g₁ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))
    ((LinOrd.Hom.hom (g₂ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))

Tactic:
exact h