awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X)
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f))
      none =
    f.toFun none

Tactic:
f.map_fst.symm

Premises used: Bipointed.Hom.map_fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X)
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f))
      none =
    f.toFun none

Tactic:
exact f.map_fst.symm

Premises used: Bipointed.Hom.map_fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val : X.X
⊢ Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X)
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f))
      (some val) =
    f.toFun (some val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedSnd.obj Y
⊢ Eq (α := Y.X)
    (Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X')
      (({
              toFun := fun (f : pointedToBipointedSnd.obj X' ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := ⋯ : X'.Hom (bipointedToPointedSnd.obj Y) },
              invFun := fun (f : X' ⟶ bipointedToPointedSnd.obj Y) ↦
                { toFun := fun (o : (pointedToBipointedSnd.obj X').X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                  map_snd := ⋯ : (pointedToBipointedSnd.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToBipointedSnd.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedSnd.obj Y) }.symm :
          (a : X' ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X' ⟶ Y)
        (f ≫ g))
      none)
    (Bipointed.Hom.toFun
      (pointedToBipointedSnd.map f ≫
        ({
                toFun := fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
                  { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) },
                invFun := fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
                  { toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                    map_snd := ⋯ : (pointedToBipointedSnd.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToBipointedSnd.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedSnd.obj Y) }.symm :
            (a : X ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X ⟶ Y)
          g)
      none)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedSnd.obj Y
val : X'.X
⊢ Eq (α := Y.X)
    (Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X')
      (({
              toFun := fun (f : pointedToBipointedSnd.obj X' ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := ⋯ : X'.Hom (bipointedToPointedSnd.obj Y) },
              invFun := fun (f : X' ⟶ bipointedToPointedSnd.obj Y) ↦
                { toFun := fun (o : (pointedToBipointedSnd.obj X').X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                  map_snd := ⋯ : (pointedToBipointedSnd.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToBipointedSnd.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedSnd.obj Y) }.symm :
          (a : X' ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X' ⟶ Y)
        (f ≫ g))
      (some val))
    (Bipointed.Hom.toFun
      (pointedToBipointedSnd.map f ≫
        ({
                toFun := fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
                  { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) },
                invFun := fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
                  { toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                    map_snd := ⋯ : (pointedToBipointedSnd.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToBipointedSnd.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedSnd.obj Y) }.symm :
            (a : X ⟶ bipointedToPointedSnd.obj Y) → pointedToBipointedSnd.obj X ⟶ Y)
          g)
      (some val))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
F : typeToCat.obj X ⟶ C
x x_1 : (↑(of (Discrete ((fun (X : Type u) ↦ X) X))) : Type u)
as : X
f : { as := as : Discrete ((fun (X : Type u) ↦ X) X) } ⟶ { as := { as := as }.as }
⊢ Eq (α :=
    Quiver.Hom (V := (↑(of ((fun (X : Type u) ↦ X) (objects.obj C))) : Type u))
      (Functor.obj
        (Hom.toFunctor
          ((fun (f : X ⟶ objects.obj C) ↦
              (Functor.toCatHom
                  (Discrete.functor
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
            ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
        { as := as : Discrete ((fun (X : Type u) ↦ X) X) })
      (Functor.obj
        (Hom.toFunctor
          ((fun (f : X ⟶ objects.obj C) ↦
              (Functor.toCatHom
                  (Discrete.functor
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
                of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
            ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
        { as := { as := as : Discrete ((fun (X : Type u) ↦ X) X) }.as : Discrete ((fun (X : Type u) ↦ X) X) }))
    (Functor.map
      (Hom.toFunctor
        ((fun (f : X ⟶ objects.obj C) ↦
            (Functor.toCatHom
                (Discrete.functor
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (objects.obj C))) :
              of (Discrete ((fun (X : Type u) ↦ X) X)) ⟶ of ((fun (X : Type u) ↦ X) (objects.obj C))))
          ((fun (F : typeToCat.obj X ⟶ C) ↦ (↾fun (x : X) ↦ F.toFunctor.obj { as := x } : X ⟶ objects.obj C)) F)))
      f)
    (eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x x_1 : Cat
x_2 : x ⟶ x_1
as : objects.obj x
this :
  ∀ (as_1 : objects.obj x) (f : { as := as : Discrete (objects.obj x) } ⟶ { as := as_1 }),
    HEq (((objects ⋙ typeToCat).map x_2 ≫ x_1.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f) (β :=
      Quiver.Hom (V := (↑(Functor.obj (𝟭 Cat) x_1) : Type u_1))
        (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
          { as := as : Discrete (objects.obj x) })
        (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
          { as := as_1 : Discrete (objects.obj x) }))
      (Functor.map (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2)) f)
⊢ ∀ (Y : (↑((objects ⋙ typeToCat).obj x) : Type u_1)) (f : { as := as : Discrete (objects.obj x) } ⟶ Y),
    HEq (((objects ⋙ typeToCat).map x_2 ≫ x_1.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f) (β :=
      Quiver.Hom (V := (↑(Functor.obj (𝟭 Cat) x_1) : Type u_1))
        (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
          { as := as : Discrete (objects.obj x) })
        (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2)) Y))
      (Functor.map (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2)) f)

Tactic:
⟨_⟩
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x x_1 : Cat
x_2 : x ⟶ x_1
as as_1 : objects.obj x
f : { as := as : Discrete (objects.obj x) } ⟶ { as := as_1 }
obtain :
  ∀ (f : { as := as : Discrete (objects.obj x) } ⟶ { as := { as := as }.as }),
    HEq (((objects ⋙ typeToCat).map x_2 ≫ x_1.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f) (β :=
      Quiver.Hom (V := (↑(Functor.obj (𝟭 Cat) x_1) : Type u_1))
        (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
          { as := as : Discrete (objects.obj x) })
        (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
          { as := { as := as : Discrete (objects.obj x) }.as : Discrete (objects.obj x) }))
      (Functor.map (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2)) f)
⊢ HEq (((objects ⋙ typeToCat).map x_2 ≫ x_1.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f) (β :=
    Quiver.Hom (V := (↑(Functor.obj (𝟭 Cat) x_1) : Type u_1))
      (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
        { as := as : Discrete (objects.obj x) })
      (Functor.obj (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2))
        { as := as_1 : Discrete (objects.obj x) }))
    (Functor.map (Hom.toFunctor (x.typeToCatObjectsAdjCounitApp.toCatHom ≫ Functor.map (𝟭 Cat) x_2)) f)

Tactic:
obtain rfl := Discrete.eq_of_hom f

Premises used: CategoryTheory.Discrete.eq_of_hom, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x : Cat
h :
  ∀ (x_1 : ConnectedComponents.{v, u} (↑x : Type u)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(Hom.toFunctor (𝟙 x)).mapConnectedComponents)).toFun x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ConnectedComponents.{v, u} (↑x : Type u)))).toFun x_1
⊢ ↾(Hom.toFunctor (𝟙 x)).mapConnectedComponents = 𝟙 (ConnectedComponents.{v, u} (↑x : Type u))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x_1 : Cat
x : ConnectedComponents.{v, u} (↑x_1 : Type u)
x_2 : (↑x_1 : Type u)
h : ⟦x_2⟧ = x
subst :
  Eq (α := ConnectedComponents.{v, u} (↑x_1 : Type u)) (Functor.mapConnectedComponents (𝟭 (↑x_1 : Type u)) ⟦x_2⟧) ⟦x_2⟧
⊢ Functor.mapConnectedComponents (𝟭 (↑x_1 : Type u)) x = x

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x : Cat
x_1 : (↑x : Type u)
⊢ Eq (α := ConnectedComponents.{v, u} (↑x : Type u)) (Functor.mapConnectedComponents (𝟭 (↑x : Type u)) ⟦x_1⟧) ⟦x_1⟧

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x_1 : Cat
x : ConnectedComponents.{v, u} (↑x_1 : Type u)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(Hom.toFunctor (𝟙 x_1)).mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ConnectedComponents.{v, u} (↑x_1 : Type u)))).toFun x

Tactic:
simpa using (Quotient.exists_rep x).elim (fun _ h ↦ by subst h; rfl)

Premises used: Quotient.exists_rep, Exists.elim
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
X_1 Y Z : Cat
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
h :
  ∀ (x_2 : ConnectedComponents.{v, u} (↑X_1 : Type u)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(x ≫ x_1).toFunctor.mapConnectedComponents)).toFun x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾x.toFunctor.mapConnectedComponents ≫ ↾x_1.toFunctor.mapConnectedComponents)).toFun
        x_2
⊢ ↾(x ≫ x_1).toFunctor.mapConnectedComponents =
    ↾x.toFunctor.mapConnectedComponents ≫ ↾x_1.toFunctor.mapConnectedComponents

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
X_1 Y Z : Cat
x_1 : X_1 ⟶ Y
x_2 : Y ⟶ Z
x : ConnectedComponents.{v, u} (↑X_1 : Type u)
x_3 : (↑X_1 : Type u)
h : ⟦x_3⟧ = x
subst :
  (x_1.toFunctor ⋙ x_2.toFunctor).mapConnectedComponents ⟦x_3⟧ =
    x_2.toFunctor.mapConnectedComponents (x_1.toFunctor.mapConnectedComponents ⟦x_3⟧)
⊢ (x_1.toFunctor ⋙ x_2.toFunctor).mapConnectedComponents x =
    x_2.toFunctor.mapConnectedComponents (x_1.toFunctor.mapConnectedComponents x)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
X_1 Y Z : Cat
x : X_1 ⟶ Y
x_1 : Y ⟶ Z
x_2 : (↑X_1 : Type u)
⊢ (x.toFunctor ⋙ x_1.toFunctor).mapConnectedComponents ⟦x_2⟧ =
    x_1.toFunctor.mapConnectedComponents (x.toFunctor.mapConnectedComponents ⟦x_2⟧)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
X_1 Y Z : Cat
x_1 : X_1 ⟶ Y
x_2 : Y ⟶ Z
x : ConnectedComponents.{v, u} (↑X_1 : Type u)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(x_1 ≫ x_2).toFunctor.mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾x_1.toFunctor.mapConnectedComponents ≫ ↾x_2.toFunctor.mapConnectedComponents)).toFun
      x

Tactic:
simpa using (Quotient.exists_rep x).elim (fun _ h => by subst h; rfl)

Premises used: Quotient.exists_rep, Exists.elim
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X_1 : Type u
C_1 : Cat
C : Cat
X : Type u
refine : (connectedComponents.obj C → X) ≃ (C ⟶ typeToCat.obj X)
⊢ (connectedComponents.obj C ⟶ X) ≃ (C ⟶ typeToCat.obj X)

Tactic:
refine TypeCat.homEquiv.trans ?_

Premises used: Equiv.trans, TypeCat.homEquiv
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X_1 : Type u
C_1 : Cat
C : Cat
X : Type u
⊢ (connectedComponents.obj C → X) ≃ (C ⟶ typeToCat.obj X)

Tactic:
exact (ConnectedComponents.typeToCatHomEquiv _ _).trans
        (Functor.equivCatHom _ _)

Premises used: CategoryTheory.ConnectedComponents.typeToCatHomEquiv, Equiv.trans, CategoryTheory.Functor.equivCatHom
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x x_1 : Type u
x_2 : x ⟶ x_1
h :
  ∀ (xcc : (typeToCat ⋙ connectedComponents).obj x),
    Eq (α := Functor.obj (𝟭 (Type u)) x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((typeToCat ⋙ connectedComponents).map x_2 ≫
            ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x_1) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x_1))))
        xcc)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x)) ≫
            Functor.map (𝟭 (Type u)) x_2))
        xcc)
⊢ Eq (α := (typeToCat ⋙ connectedComponents).obj x ⟶ Functor.obj (𝟭 (Type u)) x_1)
    ((typeToCat ⋙ connectedComponents).map x_2 ≫
      ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x_1) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x_1)))
    (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x)) ≫
      Functor.map (𝟭 (Type u)) x_2)

Tactic:
ext xcc
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X : Type u
C : Cat
x x_1 : Type u
x_2 : x ⟶ x_1
xcc : (typeToCat ⋙ connectedComponents).obj x
h :
  ∀ (x_3 : (↑(typeToCat.obj x) : Type u)) (h : ⟦x_3⟧ = xcc),
    Eq (α := Functor.obj (𝟭 (Type u)) x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((typeToCat ⋙ connectedComponents).map x_2 ≫
            ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x_1) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x_1))))
        xcc)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x)) ≫
            Functor.map (𝟭 (Type u)) x_2))
        xcc)
⊢ Eq (α := Functor.obj (𝟭 (Type u)) x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((typeToCat ⋙ connectedComponents).map x_2 ≫
          ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x_1) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x_1))))
      xcc)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾ConnectedComponents.liftFunctor (↑(typeToCat.obj x) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj x)) ≫
          Functor.map (𝟭 (Type u)) x_2))
      xcc)

Tactic:
obtain ⟨x, h⟩ := Quotient.exists_rep xcc

Premises used: Quotient.exists_rep
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X_1 : Type u
C_1 : Cat
C : Cat
X : Type u
G : C ⟶ typeToCat.obj X
h :
  ∀ (cc : connectedComponents.obj C),
    Eq (α := X)
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((Equiv.symm
                (Equiv.trans TypeCat.homEquiv
                  (Equiv.trans (ConnectedComponents.typeToCatHomEquiv (↑C : Type u) X)
                    (Functor.equivCatHom (↑C : Type u) (Discrete X)))) :
              (a : C ⟶ typeToCat.obj X) → connectedComponents.obj C ⟶ X)
            G))
        cc)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (connectedComponents.map G ≫
            NatTrans.app
              {
                app := fun (X : Type u) ↦
                  ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj X)),
                naturality := ⋯ : NatTrans (typeToCat ⋙ connectedComponents) (𝟭 (Type u)) }
              X))
        cc)
⊢ Eq (α := connectedComponents.obj C ⟶ X)
    ((Equiv.symm
            (Equiv.trans TypeCat.homEquiv
              (Equiv.trans (ConnectedComponents.typeToCatHomEquiv (↑C : Type u) X)
                (Functor.equivCatHom (↑C : Type u) (Discrete X)))) :
          (a : C ⟶ typeToCat.obj X) → connectedComponents.obj C ⟶ X)
        G :
      connectedComponents.obj C ⟶ X)
    (connectedComponents.map G ≫
        NatTrans.app
          {
            app := fun (X : Type u) ↦
              ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj X)),
            naturality := ⋯ }
          X :
      connectedComponents.obj C ⟶ Functor.obj (𝟭 (Type u)) X)

Tactic:
ext cc
-- Module: Mathlib.CategoryTheory.Category.Cat.Adjunction
Goal:
X_1 : Type u
C_1 : Cat
C : Cat
X : Type u
G : C ⟶ typeToCat.obj X
cc : connectedComponents.obj C
h :
  ∀ (w : (↑C : Type u)),
    ⟦w⟧ = cc →
      Eq (α := X)
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((Equiv.symm
                  (Equiv.trans TypeCat.homEquiv
                    (Equiv.trans (ConnectedComponents.typeToCatHomEquiv (↑C : Type u) X)
                      (Functor.equivCatHom (↑C : Type u) (Discrete X)))) :
                (a : C ⟶ typeToCat.obj X) → connectedComponents.obj C ⟶ X)
              G))
          cc)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (connectedComponents.map G ≫
              NatTrans.app
                {
                  app := fun (X : Type u) ↦
                    ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj X)),
                  naturality := ⋯ : NatTrans (typeToCat ⋙ connectedComponents) (𝟭 (Type u)) }
                X))
          cc)
⊢ Eq (α := X)
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((Equiv.symm
              (Equiv.trans TypeCat.homEquiv
                (Equiv.trans (ConnectedComponents.typeToCatHomEquiv (↑C : Type u) X)
                  (Functor.equivCatHom (↑C : Type u) (Discrete X)))) :
            (a : C ⟶ typeToCat.obj X) → connectedComponents.obj C ⟶ X)
          G))
      cc)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (connectedComponents.map G ≫
          NatTrans.app
            {
              app := fun (X : Type u) ↦
                ↾ConnectedComponents.liftFunctor (↑(typeToCat.obj X) : Type u) (Hom.toFunctor (𝟙 typeToCat.obj X)),
              naturality := ⋯ : NatTrans (typeToCat ⋙ connectedComponents) (𝟭 (Type u)) }
            X))
      cc)

Tactic:
obtain ⟨_, _⟩ := Quotient.exists_rep cc

Premises used: Quotient.exists_rep
-- Module: Mathlib.CategoryTheory.Category.Cat.CartesianClosed
Goal:
C : Type u
inst : Category.{u, u} C
D : Type u
inst_1 : Category.{u, u} D
⊢ obj (ihom (of C)) (of D) = of (C ⥤ D)

Tactic:
rfl

Premises used: CategoryTheory.Cat.of, CategoryTheory.Bundled.of, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.CartesianClosed
Goal:
C : Type u
inst : Category.{u, u} C
D E : Type u
inst_1 : Category.{u, u} D
inst_2 : Category.{u, u} E
F : D ⥤ E
⊢ Eq (α := obj (ihom (of C)) (of D) ⟶ obj (ihom (of C)) (of E)) (map (ihom (of C)) F.toCatHom)
    (toCatHom (obj (whiskeringRight C D E) F))

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.Colimit
Goal:
⊢ HasColimits Cat

Tactic:
hasColimits_of_reflective nerveFunctor

Premises used: CategoryTheory.hasColimits_of_reflective, CategoryTheory.nerveFunctor
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X_1 Y_1 : J
f : X_1 ⟶ Y_1
g :
  Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) X_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
        X :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) X_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
        Y :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
refine_1 :
  (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
      X =
    (F.map f).toFunctor.obj
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) X_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
        X)
refine_2 :
  (F.map f).toFunctor.obj
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) X_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj X_1))
        Y) =
    (hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
        (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
      Y
⊢ Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
        X :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) Y_1) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))
        Y :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj Y_1))

Tactic:
refine eqToHom ?_ ≫ (F.map f).toFunctor.map g ≫ eqToHom ?_

Premises used: CategoryTheory.eqToHom, CategoryTheory.Functor.map, CategoryTheory.Cat.Hom.toFunctor