awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
f : X ⟶ Y
a_1 : ((typeToPartialFun ⋙ partialFunToPointed).obj X).X
a : typeToPartialFun.obj X
h :
  Eq (α := (typeToPointed.obj Y).X)
    (Pointed.Hom.toFun
      ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (x : Type u_1) ↦
              ({
                  hom :=
                    { toFun := id, map_point := ⋯ :
                      ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                  inv :=
                    { toFun := id, map_point := ⋯ :
                      (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
            Y))
      (some a))
    (Part.toOption
      (Part.some
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) Y)
          a)))
⊢ Pointed.Hom.toFun
      ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (x : Type u_1) ↦
              ({
                  hom :=
                    { toFun := id, map_point := ⋯ :
                      ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                  inv :=
                    { toFun := id, map_point := ⋯ :
                      (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
            Y))
      (some a) =
    Pointed.Hom.toFun (X := (typeToPartialFun ⋙ partialFunToPointed).obj X)
      (Iso.hom
          ((fun (x : Type u_1) ↦
              ({
                  hom :=
                    { toFun := id, map_point := ⋯ :
                      ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                  inv :=
                    { toFun := id, map_point := ⋯ :
                      (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
            X) ≫
        typeToPointed.map f)
      (some a)

Tactic:
convert! Part.some_toOption _

Premises used: Part.some_toOption
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
f : X ⟶ Y
a_1 : ((typeToPartialFun ⋙ partialFunToPointed).obj X).X
a : typeToPartialFun.obj X
⊢ (typeToPartialFun.map f a).Dom

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
f : X ⟶ Y
a_1 : ((typeToPartialFun ⋙ partialFunToPointed).obj X).X
a : typeToPartialFun.obj X
⊢ Eq (α := (typeToPointed.obj Y).X)
    (Pointed.Hom.toFun
      ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (x : Type u_1) ↦
              ({
                  hom :=
                    { toFun := id, map_point := ⋯ :
                      ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                  inv :=
                    { toFun := id, map_point := ⋯ :
                      (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
            Y))
      (some a))
    (Part.toOption
      (Part.some
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) Y)
          a)))

Tactic:
simpa using (Part.get_eq_iff_mem (by trivial)).mp rfl

Premises used: Part.get_eq_iff_mem, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
point : X
⊢ (of point).X = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.point) = Z.point
rw₁ : g.toFun Y.point = Z.point
rw₂ rw₃ : Z.point = Z.point
⊢ (g.toFun ∘ f.toFun) X.point = Z.point

Tactic:
rw [Function.comp_apply, f.map_point, g.map_point]

Premises used: Pointed.Hom.map_point, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Pointed
⊢ toFun (𝟙 X) = _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).toFun = g.toFun ∘ f.toFun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X Y Z : Type u
x : X ⟶ Y
x_1 : Y ⟶ Z
simp :
  Eq (α := X → Z) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1)) : (a : X) → Z)
    (Function.comp (β := Y) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1) : (a : Y) → Z)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x) : (a : X) → Y))
⊢ Eq.{u + 1} (α := { X := Option X, point := none }.X → { X := Option Z, point := none }.X)
    (Pointed.Hom.toFun
      {
        toFun :=
          Option.map
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z),
        map_point := ⋯ })
    (Pointed.Hom.toFun
      (CategoryStruct.comp (Y := { X := Option Y, point := none })
        {
          toFun :=
            Option.map
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y),
          map_point := ⋯ }
        {
          toFun :=
            Option.map
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1) :
                (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z),
          map_point := ⋯ }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X Y Z : Type u
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := X → Z) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1)) : (a : X) → Z)
    (Function.comp (β := Y) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1) : (a : Y) → Z)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x) : (a : X) → Y))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
toFun :
  Pointed.Hom.toFun
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f)) =
    f.toFun
⊢ (fun
          (f :
            X ⟶
              Functor.obj
                (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                  Pointed.X))
                Y) ↦
        ({
            toFun := fun (o : (typeToPointed.obj X).X) ↦
              Option.elim o Y.point
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
            map_point := ⋯ } :
          (typeToPointed.obj X).Hom Y))
      ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f) =
    f

Tactic:
apply Pointed.Hom.ext

Premises used: Pointed.Hom.ext
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
toFun :
  ∀ (x : (typeToPointed.obj X).X),
    Pointed.Hom.toFun
        ((fun
              (f :
                X ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) ↦
            ({
                toFun := fun (o : (typeToPointed.obj X).X) ↦
                  Option.elim o Y.point
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                map_point := ⋯ } :
              (typeToPointed.obj X).Hom Y))
          ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
        x =
      f.toFun x
⊢ Pointed.Hom.toFun
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f)) =
    f.toFun

Tactic:
funext x
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
x : (typeToPointed.obj X).X
toFun :
  Pointed.Hom.toFun (X := typeToPointed.obj X)
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
      none =
    f.toFun none
toFun₁ :
  ∀ (val : X),
    Pointed.Hom.toFun (X := typeToPointed.obj X)
        ((fun
              (f :
                X ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) ↦
            ({
                toFun := fun (o : (typeToPointed.obj X).X) ↦
                  Option.elim o Y.point
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                map_point := ⋯ } :
              (typeToPointed.obj X).Hom Y))
          ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
        (some val) =
      f.toFun (some val)
⊢ Pointed.Hom.toFun
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
      x =
    f.toFun x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ Pointed.Hom.toFun (X := typeToPointed.obj X)
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
      none =
    f.toFun none

Tactic:
f.map_point.symm

Premises used: Pointed.Hom.map_point, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ Pointed.Hom.toFun (X := typeToPointed.obj X)
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
      none =
    f.toFun none

Tactic:
exact f.map_point.symm

Premises used: Pointed.Hom.map_point, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val : X
⊢ Pointed.Hom.toFun (X := typeToPointed.obj X)
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                    Pointed.X))
                  Y) ↦
          ({
              toFun := fun (o : (typeToPointed.obj X).X) ↦
                Option.elim o Y.point
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
              map_point := ⋯ } :
            (typeToPointed.obj X).Hom Y))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
      (some val) =
    f.toFun (some val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X' X : Type u_1
Y : Pointed
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)) Y
⊢ Eq (α := Y.X)
    (Pointed.Hom.toFun (X := typeToPointed.obj X')
      (({ toFun := fun (f : typeToPointed.obj X' ⟶ Y) ↦ ↾(f.toFun ∘ some),
              invFun :=
                fun
                  (f :
                    X' ⟶
                      Functor.obj
                        (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                          (CC := Pointed.X))
                        Y) ↦
                {
                  toFun := fun (o : (typeToPointed.obj X').X) ↦
                    Option.elim o Y.point
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u_1) ↦ X) X') → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                  map_point := ⋯ : (typeToPointed.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (typeToPointed.obj X' ⟶ Y) ≃
                (X' ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) }.symm :
          (a : X' ⟶ (forget Pointed).obj Y) → typeToPointed.obj X' ⟶ Y)
        (f ≫ g))
      none)
    (Pointed.Hom.toFun
      (typeToPointed.map f ≫
        ({ toFun := fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some),
                invFun :=
                  fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                            (CC := Pointed.X))
                          Y) ↦
                  {
                    toFun := fun (o : (typeToPointed.obj X).X) ↦
                      Option.elim o Y.point
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                    map_point := ⋯ : (typeToPointed.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (typeToPointed.obj X ⟶ Y) ≃
                  (X ⟶
                    Functor.obj
                      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                        (CC := Pointed.X))
                      Y) }.symm :
            (a : X ⟶ (forget Pointed).obj Y) → typeToPointed.obj X ⟶ Y)
          g)
      none)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Pointed
Goal:
X' X : Type u_1
Y : Pointed
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)) Y
val : X'
⊢ Eq (α := Y.X)
    (Pointed.Hom.toFun (X := typeToPointed.obj X')
      (({ toFun := fun (f : typeToPointed.obj X' ⟶ Y) ↦ ↾(f.toFun ∘ some),
              invFun :=
                fun
                  (f :
                    X' ⟶
                      Functor.obj
                        (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                          (CC := Pointed.X))
                        Y) ↦
                {
                  toFun := fun (o : (typeToPointed.obj X').X) ↦
                    Option.elim o Y.point
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u_1) ↦ X) X') → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                  map_point := ⋯ : (typeToPointed.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (typeToPointed.obj X' ⟶ Y) ≃
                (X' ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) }.symm :
          (a : X' ⟶ (forget Pointed).obj Y) → typeToPointed.obj X' ⟶ Y)
        (f ≫ g))
      (some val))
    (Pointed.Hom.toFun
      (typeToPointed.map f ≫
        ({ toFun := fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some),
                invFun :=
                  fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                            (CC := Pointed.X))
                          Y) ↦
                  {
                    toFun := fun (o : (typeToPointed.obj X).X) ↦
                      Option.elim o Y.point
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                    map_point := ⋯ : (typeToPointed.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (typeToPointed.obj X ⟶ Y) ≃
                  (X ⟶
                    Functor.obj
                      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                        (CC := Pointed.X))
                      Y) }.symm :
            (a : X ⟶ (forget Pointed).obj Y) → typeToPointed.obj X ⟶ Y)
          g)
      (some val))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
α : Type u
inst : Preorder α
U V : α
⊢ Subsingleton.{u + 1} (U ⟶ V)

Tactic:
⟨fun _ _ => ULift.ext _ _ (Subsingleton.elim _ _ )⟩

Premises used: ULift.ext, Subsingleton.intro, Subsingleton.elim, ULift.down
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x : X
h : x ≤ x
⊢ h.hom = 𝟙 x

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y z : X
h : x ≤ y
k : y ≤ z
⊢ homOfLE h ≫ homOfLE k = homOfLE ⋯

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y : X
h : x ⟶ y
⊢ x ≤ y

Tactic:
h.down.down

Premises used: PLift.down, ULift.down
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
⊢ ∀ {X : Type u_1} [inst : Preorder X] {x y : X} (h : x ⟶ y), x ≤ y

Tactic:
@leOfHom

Premises used: CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y : X
h : x ⟶ y
⊢ ⋯.hom = h

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y : X
h : x ≤ y
heq : x = y
⊢ homOfLE h ≫ homOfLE ⋯ = 𝟙 x ∧ homOfLE ⋯ ≫ homOfLE h = 𝟙 y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y : X
h : x = y
rw rw₁ : y ≤ y
⊢ x ≤ y

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y : X
h : x = y
subst : IsIso (homOfLE ⋯)
⊢ IsIso (homOfLE ⋯)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x : X
⊢ IsIso (𝟙 x)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
a b c : X
hab : a ≤ b
hbc : b = c
⊢ homOfLE hab ≫ eqToHom hbc = homOfLE ⋯

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
a b c : X
hab : a = b
hbc : b ≤ c
⊢ eqToHom hab ≫ homOfLE hbc = homOfLE ⋯

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
a b c : X
hab : b ≤ a
hbc : op b = op c
⊢ (homOfLE hab).op ≫ eqToHom hbc = (homOfLE ⋯).op

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
a b c : X
hab : op a = op b
hbc : c ≤ b
⊢ eqToHom hab ≫ (homOfLE hbc).op = (homOfLE ⋯).op

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
x y : Xᵒᵖ
h : x ⟶ y
⊢ unop y ≤ unop x

Tactic:
h.unop.le

Premises used: Quiver.Hom.le, Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
inst_1 : OrderTop X
x : X
a : x ⟶ ⊤
⊢ a = homOfLE ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : Preorder X
inst_1 : OrderBot X
x : X
a : ⊥ ⟶ x
⊢ a = homOfLE ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
Y : Type v
inst : Preorder X
inst_1 : Preorder Y
f : X → Y
h : Monotone f
⊢ h.functor.obj = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
Y : Type v
inst : Preorder X
inst_1 : Preorder Y
e : X ≃o Y
x : X
⊢ Functor.obj (𝟭 X) x = (⋯.functor ⋙ ⋯.functor).obj x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
Y : Type v
inst : Preorder X
inst_1 : Preorder Y
e : X ≃o Y
x : Y
⊢ (⋯.functor ⋙ ⋯.functor).obj x = Functor.obj (𝟭 Y) x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
Y : Type v
inst : Preorder X
inst_1 : Preorder Y
f : X ⥤ Y
⊢ Monotone f.obj

Tactic:
fun _ _ hxy => (f.map hxy.hom).le

Premises used: Quiver.Hom.le, Monotone, LE.le.hom, CategoryTheory.Functor.map