awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
X Y Z : F.PartialLeftAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
a :
  Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z) → X.obj ⟶ F.obj (F.partialLeftAdjointObj Z))
        (F.partialLeftAdjointMap (f ≫ g)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z) → X.obj ⟶ F.obj (F.partialLeftAdjointObj Z))
        (F.partialLeftAdjointMap f ≫ F.partialLeftAdjointMap g) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))
⊢ F.partialLeftAdjointMap (f ≫ g) = F.partialLeftAdjointMap f ≫ F.partialLeftAdjointMap g

Tactic:
apply F.partialLeftAdjointHomEquiv.injective

Premises used: CategoryTheory.Functor.partialLeftAdjointHomEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
X Y Z : F.PartialLeftAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z) → X.obj ⟶ F.obj (F.partialLeftAdjointObj Z))
        (F.partialLeftAdjointMap (f ≫ g)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Z) → X.obj ⟶ F.obj (F.partialLeftAdjointObj Z))
        (F.partialLeftAdjointMap f ≫ F.partialLeftAdjointMap g) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Z))

Tactic:
simp [partialLeftAdjointHomEquiv_comp, ← F.partialLeftAdjointHomEquiv_comp]

Premises used: CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
h : F.leftAdjointObjIsDefined = ⊤
X : C
⊢ (F ⋙ obj coyoneda (op X)).IsCorepresentable

Tactic:
simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]

Premises used: Pi.top_apply, CategoryTheory.Functor.leftAdjointObjIsDefined_iff, Prop.top_eq_true
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
h : F.leftAdjointObjIsDefined = ⊤
⊢ ∀ (X : C), (F ⋙ obj coyoneda (op X)).IsCorepresentable

Tactic:
replace h : ∀ X, IsCorepresentable (F ⋙ coyoneda.obj (op X)) := fun X ↦ by
    simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
h : ∀ (X : C), (F ⋙ obj coyoneda (op X)).IsCorepresentable
X : C
Y Y' : D
g : Y ⟶ Y'
f : (F ⋙ obj coyoneda (op X)).coreprX ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ F.obj Y')
    ((((fun (X : C) (Y : D) ↦
                (CorepresentableBy.homEquiv (F ⋙ obj coyoneda (op X)).corepresentableBy :
                  Equiv.{v₂ + 1, v₁ + 1} ((F ⋙ obj coyoneda (op X)).coreprX ⟶ Y) ((F ⋙ obj coyoneda (op X)).obj Y)))
              X Y' :
            Equiv.{v₂ + 1, v₁ + 1} ((F ⋙ obj coyoneda (op X)).coreprX ⟶ Y') ((F ⋙ obj coyoneda (op X)).obj Y')) :
          (a : (F ⋙ coyoneda.obj (op X)).coreprX ⟶ Y') → X ⟶ F.obj Y')
        (f ≫ g) :
      X ⟶ F.obj Y')
    ((((fun (X : C) (Y : D) ↦
                  (CorepresentableBy.homEquiv (F ⋙ obj coyoneda (op X)).corepresentableBy :
                    Equiv.{v₂ + 1, v₁ + 1} ((F ⋙ obj coyoneda (op X)).coreprX ⟶ Y) ((F ⋙ obj coyoneda (op X)).obj Y)))
                X Y :
              Equiv.{v₂ + 1, v₁ + 1} ((F ⋙ obj coyoneda (op X)).coreprX ⟶ Y) ((F ⋙ obj coyoneda (op X)).obj Y)) :
            (a : (F ⋙ coyoneda.obj (op X)).coreprX ⟶ Y) → X ⟶ F.obj Y)
          f ≫
        F.map g :
      X ⟶ F.obj Y')

Tactic:
apply CorepresentableBy.homEquiv_comp

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
h : ∀ (X : C), (F ⋙ obj coyoneda (op X)).IsCorepresentable
⊢ F.IsRightAdjoint

Tactic:
exact (Adjunction.adjunctionOfEquivLeft
    (fun X Y ↦ (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv)
    (fun X Y Y' g f ↦ by apply CorepresentableBy.homEquiv_comp)).isRightAdjoint

Premises used: CategoryTheory.coyoneda, CategoryTheory.Functor.CorepresentableBy.homEquiv, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.adjunctionOfEquivLeft, CategoryTheory.Functor.corepresentableBy, CategoryTheory.Adjunction.isRightAdjoint, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
⊢ F.IsRightAdjoint ↔ F.leftAdjointObjIsDefined = ⊤

Tactic:
⟨fun h ↦ ?_, isRightAdjoint_of_leftAdjointObjIsDefined_eq_top⟩

Premises used: CategoryTheory.Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top, Iff.intro
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
refine : ∀ (h : F.IsRightAdjoint), F.leftAdjointObjIsDefined = ⊤
⊢ F.IsRightAdjoint ↔ F.leftAdjointObjIsDefined = ⊤

Tactic:
refine ⟨fun h ↦ ?_, isRightAdjoint_of_leftAdjointObjIsDefined_eq_top⟩
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
h : F.IsRightAdjoint
h₁ : ∀ (X : C), F.leftAdjointObjIsDefined X ↔ ⊤ X
⊢ F.leftAdjointObjIsDefined = ⊤

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
h : F.IsRightAdjoint
X : C
⊢ F.leftAdjointObjIsDefined X ↔ ⊤ X

Tactic:
simpa only [Pi.top_apply, Prop.top_eq_true, iff_true]
    using leftAdjointObjIsDefined_of_adjunction (Adjunction.ofIsRightAdjoint F) X

Premises used: iff_true, CategoryTheory.Functor.leftAdjointObjIsDefined_of_adjunction, Pi.top_apply, CategoryTheory.Adjunction.ofIsRightAdjoint, Prop.top_eq_true
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
dsimp :
  Eq (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.1 Y)
    ((R.map φ).hom ≫
      ((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j') ⟶ Y)
              ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j') ⟶ Y) → (R.obj j').obj ⟶ F.obj Y)
        (c'.ι.app j' ≫ f))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        (c'.ι.app j ≫ f) ≫
      𝟙 (F.1 Y))
⊢ Eq (α := (R ⋙ F.leftAdjointObjIsDefined.ι).obj j ⟶ obj.{v_1, v₁, u_1, u₁} (obj (const J) (F.1 Y)) j')
    ((R ⋙ F.leftAdjointObjIsDefined.ι).map φ ≫
      ((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j') ⟶ Y)
              ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j') ⟶ Y) → (R.obj j').obj ⟶ F.obj Y)
        (c'.ι.app j' ≫ f))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        (c'.ι.app j ≫ f) ≫
      map (obj (const J) (F.1 Y)) φ)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
rw :
  Eq.{v₁ + 1} (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.1 Y)
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        (F.partialLeftAdjointMap (R.map φ) ≫ c'.ι.app j' ≫ f) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        ((R ⋙ F.partialLeftAdjoint).map φ ≫ c'.ι.app j' ≫ f) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
⊢ Eq (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.1 Y)
    ((R.map φ).hom ≫
      ((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j') ⟶ Y)
              ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j') ⟶ Y) → (R.obj j').obj ⟶ F.obj Y)
        (c'.ι.app j' ≫ f))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        (c'.ι.app j ≫ f) ≫
      𝟙 (F.1 Y))

Tactic:
rw [comp_id, ← c'.w φ, ← partialLeftAdjointHomEquiv_map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp, CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
⊢ Eq.{v₁ + 1} (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.1 Y)
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        (F.partialLeftAdjointMap (R.map φ) ≫ c'.ι.app j' ≫ f) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
        ((R ⋙ F.partialLeftAdjoint).map φ ≫ c'.ι.app j' ≫ f) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ obj coyoneda (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
⊢ (R ⋙ F.leftAdjointObjIsDefined.ι).map φ ≫ c.ι.app j' = c.ι.app j

Tactic:
have := c.w φ
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y Y' : D
g : Y ⟶ Y'
f : c'.pt ⟶ Y
j : J
⊢ Eq (α := (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
    (c.ι.app j ≫
        hc.desc
          { pt := F.1 Y',
            ι :=
              {
                app := fun (j : J) ↦
                  ((F.partialLeftAdjointHomEquiv :
                        Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y')
                          ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')) :
                      (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y') → (R.obj j).obj ⟶ F.obj Y')
                    (c'.ι.app j ≫ f ≫ g),
                naturality := ⋯ } } :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
    (c.ι.app j ≫
        hc.desc
            { pt := F.1 Y,
              ι :=
                {
                  app := fun (j : J) ↦
                    ((F.partialLeftAdjointHomEquiv :
                          Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ Y)
                            ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
                        (a : F.partialLeftAdjointObj (R.obj j) ⟶ Y) → (R.obj j).obj ⟶ F.obj Y)
                      (c'.ι.app j ≫ f),
                  naturality := ⋯ } } ≫
          F.map g :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')

Tactic:
simp only [IsColimit.fac, IsColimit.fac_assoc, partialLeftAdjointHomEquiv_comp,
      F.map_comp, assoc]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp, CategoryTheory.Limits.IsColimit.fac_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J C
c : Cocone R
hc : IsColimit c
inst_3 : HasColimitsOfShape.{v_1, u_1, v₂, u₂} J D
h : ∀ (j : J), F.leftAdjointObjIsDefined (R.obj j)
⊢ F.leftAdjointObjIsDefined c.pt

Tactic:
(corepresentableByCompCoyonedaObjOfIsColimit
    (R := ObjectProperty.lift _ R h) hc (colimit.isColimit _)).isCorepresentable

Premises used: CategoryTheory.Functor.CorepresentableBy.isCorepresentable, CategoryTheory.Functor.corepresentableByCompCoyonedaObjOfIsColimit, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Functor.leftAdjointObjIsDefined
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₁, u_1, u₁} J C
inst_3 : HasColimit R
inst_4 : HasColimitsOfShape.{v_1, u_1, v₂, u₂} J D
h : ∀ (j : J), F.leftAdjointObjIsDefined (R.obj j)
⊢ F.leftAdjointObjIsDefined (colimit R)

Tactic:
leftAdjointObjIsDefined_of_isColimit (colimit.isColimit R) h

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Functor.leftAdjointObjIsDefined_of_isColimit
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : D
⊢ F.rightAdjointObjIsDefined Y ↔ (F.op ⋙ obj yoneda Y).IsRepresentable

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
Y : D
⊢ F.rightAdjointObjIsDefined Y

Tactic:
(adj.representableBy Y).isRepresentable

Premises used: CategoryTheory.Adjunction.representableBy, CategoryTheory.Functor.RepresentableBy.isRepresentable, CategoryTheory.Functor.rightAdjointObjIsDefined
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : F.PartialRightAdjointSource
⊢ (F.op ⋙ obj yoneda (Y.obj (P := F.rightAdjointObjIsDefined))).IsRepresentable

Tactic:
Y.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.rightAdjointObjIsDefined
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X X' : C
Y : F.PartialRightAdjointSource
f : X' ⟶ F.partialRightAdjointObj Y
g : X ⟶ X'
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (X ⟶ F.partialRightAdjointObj Y)
              (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
          (a : X ⟶ F.partialRightAdjointObj Y) → F.obj X ⟶ Y.obj)
        (g ≫ f) :
      F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))
    (F.map g ≫
        ((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X' ⟶ F.partialRightAdjointObj Y)
                (F.obj X' ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
            (a : X' ⟶ F.partialRightAdjointObj Y) → F.obj X' ⟶ Y.obj)
          f :
      F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))

Tactic:
RepresentableBy.homEquiv_comp ..

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.RepresentableBy.homEquiv_comp, CategoryTheory.Functor.partialRightAdjointObj
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : F.PartialRightAdjointSource
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := F.obj (F.partialRightAdjointObj X) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Y)
              (F.obj (F.partialRightAdjointObj X) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Y) → F.obj (F.partialRightAdjointObj X) ⟶ Y.obj)
        (F.partialRightAdjointMap f) :
      F.obj (F.partialRightAdjointObj X) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj X)
                (F.obj (F.partialRightAdjointObj X) ⟶ X.obj (P := F.rightAdjointObjIsDefined))) :
            (a : F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj X) → F.obj (F.partialRightAdjointObj X) ⟶ X.obj)
          (𝟙 (F.partialRightAdjointObj X)) ≫
        f.hom :
      F.obj (F.partialRightAdjointObj X) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))

Tactic:
simp [partialRightAdjointMap]

Premises used: CategoryTheory.Functor.partialRightAdjointMap
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X X' : C
Y : F.PartialRightAdjointSource
f : F.obj X' ⟶ Y.obj (P := F.rightAdjointObjIsDefined)
g : X ⟶ X'
⊢ Eq (α := X ⟶ F.partialRightAdjointObj Y)
    (g ≫
      ((Equiv.symm F.partialRightAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj X' ⟶ Y.obj (P := F.rightAdjointObjIsDefined))
              (X' ⟶ F.partialRightAdjointObj Y)) :
          (a : F.obj X' ⟶ Y.obj) → X' ⟶ F.partialRightAdjointObj Y)
        f)
    (((Equiv.symm F.partialRightAdjointHomEquiv :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined)) (X ⟶ F.partialRightAdjointObj Y)) :
        (a : F.obj X ⟶ Y.obj) → X ⟶ F.partialRightAdjointObj Y)
      (F.map g ≫ f))

Tactic:
RepresentableBy.comp_homEquiv_symm ..

Premises used: CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm, Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y Y' : F.PartialRightAdjointSource
f : F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined)
g : Y ⟶ Y'
⊢ Eq.{v₁ + 1} (α := X ⟶ F.partialRightAdjointObj Y')
    (((Equiv.symm F.partialRightAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y.obj (P := F.rightAdjointObjIsDefined))
                (X ⟶ F.partialRightAdjointObj Y)) :
            (a : F.obj X ⟶ Y.obj) → X ⟶ F.partialRightAdjointObj Y)
          f ≫
        F.partialRightAdjointMap g :
      X ⟶ F.partialRightAdjointObj Y')
    (((Equiv.symm F.partialRightAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
              (X ⟶ F.partialRightAdjointObj Y')) :
          (a : F.obj X ⟶ Y'.obj) → X ⟶ F.partialRightAdjointObj Y')
        (f ≫ g.hom) :
      X ⟶ F.partialRightAdjointObj Y')

Tactic:
simp [Equiv.eq_symm_apply, partialRightAdjointHomEquiv_map_comp]

Premises used: CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp, Equiv.eq_symm_apply