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₂} C D
X : F.PartialRightAdjointSource
a :
  Eq.{v₂ + 1} (α := F.obj (F.partialRightAdjointObj X) ⟶ X.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.partialRightAdjointMap (𝟙 X)) :
      F.obj (F.partialRightAdjointObj X) ⟶ X.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.obj (F.partialRightAdjointObj X) ⟶ X.obj (P := F.rightAdjointObjIsDefined))
⊢ F.partialRightAdjointMap (𝟙 X) = 𝟙 (F.partialRightAdjointObj X)

Tactic:
apply F.partialRightAdjointHomEquiv.injective

Premises used: CategoryTheory.Functor.partialRightAdjointHomEquiv, 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₂} C D
X : F.PartialRightAdjointSource
⊢ Eq.{v₂ + 1} (α := F.obj (F.partialRightAdjointObj X) ⟶ X.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.partialRightAdjointMap (𝟙 X)) :
      F.obj (F.partialRightAdjointObj X) ⟶ X.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.obj (F.partialRightAdjointObj X) ⟶ X.obj (P := F.rightAdjointObjIsDefined))

Tactic:
simp [partialRightAdjointHomEquiv_map]

Premises used: CategoryTheory.Functor.partialRightAdjointHomEquiv_map
-- 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 Z : F.PartialRightAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
a :
  Eq.{v₂ + 1} (α := F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z)
              (F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z) → F.obj (F.partialRightAdjointObj X) ⟶ Z.obj)
        (F.partialRightAdjointMap (f ≫ g)) :
      F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z)
              (F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z) → F.obj (F.partialRightAdjointObj X) ⟶ Z.obj)
        (F.partialRightAdjointMap f ≫ F.partialRightAdjointMap g) :
      F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))
⊢ F.partialRightAdjointMap (f ≫ g) = F.partialRightAdjointMap f ≫ F.partialRightAdjointMap g

Tactic:
apply F.partialRightAdjointHomEquiv.injective

Premises used: CategoryTheory.Functor.partialRightAdjointHomEquiv, 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₂} C D
X Y Z : F.PartialRightAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₂ + 1} (α := F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z)
              (F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z) → F.obj (F.partialRightAdjointObj X) ⟶ Z.obj)
        (F.partialRightAdjointMap (f ≫ g)) :
      F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z)
              (F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj X ⟶ F.partialRightAdjointObj Z) → F.obj (F.partialRightAdjointObj X) ⟶ Z.obj)
        (F.partialRightAdjointMap f ≫ F.partialRightAdjointMap g) :
      F.obj (F.partialRightAdjointObj X) ⟶ Z.obj (P := F.rightAdjointObjIsDefined))

Tactic:
simp [partialRightAdjointHomEquiv_comp, ← assoc, ← F.partialRightAdjointHomEquiv_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.partialRightAdjointHomEquiv_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₂} C D
h : F.rightAdjointObjIsDefined = ⊤
X : D
⊢ (F.op ⋙ obj yoneda X).IsRepresentable

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

Premises used: CategoryTheory.Functor.rightAdjointObjIsDefined_iff, 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₂} C D
h : F.rightAdjointObjIsDefined = ⊤
⊢ ∀ (X : D), (F.op ⋙ obj yoneda X).IsRepresentable

Tactic:
replace h : ∀ X, IsRepresentable (F.op ⋙ yoneda.obj X) := fun X ↦ by
    simp only [← rightAdjointObjIsDefined_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₂} C D
h : ∀ (X : D), (F.op ⋙ obj yoneda X).IsRepresentable
⊢ F.IsLeftAdjoint

Tactic:
(Adjunction.adjunctionOfEquivRight
    (fun X Y ↦ (F.op ⋙ yoneda.obj Y).representableBy.homEquiv.symm)
    (fun X Y Y' g f ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)).isLeftAdjoint

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm, CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Adjunction.adjunctionOfEquivRight, CategoryTheory.Adjunction.isLeftAdjoint, Equiv.symm, Eq.symm, CategoryTheory.Functor.RepresentableBy.homEquiv, CategoryTheory.Functor.obj, CategoryTheory.Functor.representableBy
-- 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
h : ∀ (X : D), (F.op ⋙ obj yoneda X).IsRepresentable
⊢ F.IsLeftAdjoint

Tactic:
exact (Adjunction.adjunctionOfEquivRight
    (fun X Y ↦ (F.op ⋙ yoneda.obj Y).representableBy.homEquiv.symm)
    (fun X Y Y' g f ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)).isLeftAdjoint

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm, CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Adjunction.adjunctionOfEquivRight, CategoryTheory.Adjunction.isLeftAdjoint, Equiv.symm, Eq.symm, CategoryTheory.Functor.RepresentableBy.homEquiv, CategoryTheory.Functor.obj, CategoryTheory.Functor.representableBy
-- 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
⊢ F.IsLeftAdjoint ↔ F.rightAdjointObjIsDefined = ⊤

Tactic:
⟨fun h ↦ ?_, isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top⟩

Premises used: Iff.intro, CategoryTheory.Functor.isLeftAdjoint_of_rightAdjointObjIsDefined_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₂} C D
refine : ∀ (h : F.IsLeftAdjoint), F.rightAdjointObjIsDefined = ⊤
⊢ F.IsLeftAdjoint ↔ F.rightAdjointObjIsDefined = ⊤

Tactic:
refine ⟨fun h ↦ ?_, isLeftAdjoint_of_rightAdjointObjIsDefined_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₂} C D
h : F.IsLeftAdjoint
h₁ : ∀ (X : D), F.rightAdjointObjIsDefined X ↔ ⊤ X
⊢ F.rightAdjointObjIsDefined = ⊤

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₂} C D
h : F.IsLeftAdjoint
X : D
⊢ F.rightAdjointObjIsDefined X ↔ ⊤ X

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

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, iff_true, Pi.top_apply, CategoryTheory.Functor.rightAdjointObjIsDefined_of_adjunction, 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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
dsimp :
  Eq.{v₂ + 1} (α := F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (𝟙 (F.1 Y) ≫
        ((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
                (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
            (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
          (f ≫ c'.π.app j') :
      F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
                (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
            (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
          (f ≫ c'.π.app j) ≫
        (R.map φ).hom :
      F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
⊢ Eq.{v₂ + 1} (α := obj.{v_1, v₂, u_1, u₂} (obj (const J) (F.1 Y)) j ⟶ (R ⋙ F.rightAdjointObjIsDefined.ι).obj j')
    (map (obj (const J) (F.1 Y)) φ ≫
        ((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
                (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
            (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
          (f ≫ c'.π.app j') :
      obj.{v_1, v₂, u_1, u₂} (obj (const J) (F.1 Y)) j ⟶ (R ⋙ F.rightAdjointObjIsDefined.ι).obj j')
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
                (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
            (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
          (f ≫ c'.π.app j) ≫
        (R ⋙ F.rightAdjointObjIsDefined.ι).map φ :
      obj.{v_1, v₂, u_1, u₂} (obj (const J) (F.1 Y)) j ⟶ (R ⋙ F.rightAdjointObjIsDefined.ι).obj j')

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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
rw :
  Eq.{v₂ + 1} (α := F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        ((f ≫ c'.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ)) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
⊢ Eq.{v₂ + 1} (α := F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (𝟙 (F.1 Y) ≫
        ((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
                (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
            (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
          (f ≫ c'.π.app j') :
      F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
                (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
            (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
          (f ≫ c'.π.app j) ≫
        (R.map φ).hom :
      F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))

Tactic:
rw [id_comp, ← c'.w φ, ← partialRightAdjointHomEquiv_map_comp,
              ← assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp, CategoryTheory.Category.id_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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ Eq.{v₂ + 1} (α := F.1 Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        ((f ≫ c'.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))
    (((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j'))
              (F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))) :
          (a : Y ⟶ F.partialRightAdjointObj (R.obj j')) → F.obj Y ⟶ (R.obj j').obj)
        ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ)) :
      F.obj Y ⟶ (R.obj j').obj (P := F.rightAdjointObjIsDefined))

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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ obj yoneda c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
⊢ c.π.app j ≫ (R ⋙ F.rightAdjointObjIsDefined.ι).map φ = 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₂} C D
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ hc.lift
        { pt := F.1 Y,
          π :=
            {
              app := fun (j : J) ↦
                ((F.partialRightAdjointHomEquiv :
                      Equiv.{v₁ + 1, v₂ + 1} (Y ⟶ F.partialRightAdjointObj (R.obj j))
                        (F.obj Y ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
                    (a : Y ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y ⟶ (R.obj j).obj)
                  ((g ≫ f) ≫ c'.π.app j),
              naturality := ⋯ } } ≫
      c.π.app j =
    (F.map g ≫
        hc.lift
          { pt := F.1 Y',
            π :=
              {
                app := fun (j : J) ↦
                  ((F.partialRightAdjointHomEquiv :
                        Equiv.{v₁ + 1, v₂ + 1} (Y' ⟶ F.partialRightAdjointObj (R.obj j))
                          (F.obj Y' ⟶ (R.obj j).obj (P := F.rightAdjointObjIsDefined))) :
                      (a : Y' ⟶ F.partialRightAdjointObj (R.obj j)) → F.obj Y' ⟶ (R.obj j).obj)
                    (f ≫ c'.π.app j),
                naturality := ⋯ : NatTrans (obj (const J) (F.1 Y')) (R ⋙ F.rightAdjointObjIsDefined.ι) } :
            Cone (R ⋙ F.rightAdjointObjIsDefined.ι) }) ≫
      c.π.app j

Tactic:
simp only [IsLimit.fac, partialRightAdjointHomEquiv_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp, CategoryTheory.Limits.IsLimit.fac
-- 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
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J D
c : Cone R
hc : IsLimit c
inst_3 : HasLimitsOfShape.{v_1, u_1, v₁, u₁} J C
h : ∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)
⊢ F.rightAdjointObjIsDefined c.pt

Tactic:
(representableByCompYonedaObjOfIsLimit
    (R := ObjectProperty.lift _ R h) hc (limit.isLimit _)).isRepresentable

Premises used: CategoryTheory.Functor.representableByCompYonedaObjOfIsLimit, CategoryTheory.Functor.RepresentableBy.isRepresentable, CategoryTheory.Limits.limit.isLimit, 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
J : Type u_1
inst_2 : Category.{v_1, u_1} J
R : Functor.{v_1, v₂, u_1, u₂} J D
inst_3 : HasLimit R
inst_4 : HasLimitsOfShape.{v_1, u_1, v₁, u₁} J C
h : ∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)
⊢ F.rightAdjointObjIsDefined (limit R)

Tactic:
rightAdjointObjIsDefined_of_isLimit (limit.isLimit R) h

Premises used: CategoryTheory.Functor.rightAdjointObjIsDefined_of_isLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
⊢ q.op.leftTriple = q.rightTriple.op

Tactic:
rfl

Premises used: CategoryTheory.Adjunction.op, CategoryTheory.Adjunction.Triple.op, CategoryTheory.Adjunction.Quadruple.leftTriple, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
⊢ q.op.rightTriple = q.leftTriple.op

Tactic:
rfl

Premises used: CategoryTheory.Adjunction.op, CategoryTheory.Adjunction.Triple.op, CategoryTheory.Adjunction.Quadruple.rightTriple, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
simp_rw :
  (∀ (X : C),
      Epi
        ((G.rightUnitor.inv ≫
              inv (G.whiskerLeft q.leftTriple.adj₁.counit) ≫
                (G.associator F L).inv ≫ whiskerRight q.leftTriple.adj₂.counit L ≫ L.leftUnitor.hom).app
          X)) ↔
    ∀ (X : D), Mono (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (F.obj X)) (q.rightTriple.adj₂.unit.app (F.obj X))
⊢ (∀ (X : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.leftToRight.app X)

Tactic:
simp_rw [mono_leftToRight_app_iff_mono_adj₂_unit_app, rightToLeft_eq_counits]

Premises used: CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits, CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₂_unit_app
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
dsimp :
  (∀ (X : C),
      Epi
        (𝟙 (G.obj X) ≫
          (inv (G.whiskerLeft q.adj₁.counit)).app X ≫
            𝟙 (L.obj (F.obj (G.obj X))) ≫ L.map (q.adj₂.counit.app X) ≫ 𝟙 (L.obj X))) ↔
    ∀ (X : D), Mono (X := F.obj X) (q.adj₃.unit.app (F.obj X))
⊢ (∀ (X : C),
      Epi
        ((G.rightUnitor.inv ≫
              inv (G.whiskerLeft q.leftTriple.adj₁.counit) ≫
                (G.associator F L).inv ≫ whiskerRight q.leftTriple.adj₂.counit L ≫ L.leftUnitor.hom).app
          X)) ↔
    ∀ (X : D), Mono (X := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (F.obj X)) (q.rightTriple.adj₂.unit.app (F.obj X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Quadruple
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₁, u₂, u₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
q : Quadruple L F G R
inst_2 : F.Full
inst_3 : F.Faithful
simp :
  (∀ (X : C), Epi (inv (q.adj₁.counit.app (G.obj X)) ≫ L.map (q.adj₂.counit.app X))) ↔
    ∀ (X : D), Mono (X := F.obj X) (q.adj₃.unit.app (F.obj X))
⊢ (∀ (X : C),
      Epi
        (𝟙 (G.obj X) ≫
          (inv (G.whiskerLeft q.adj₁.counit)).app X ≫
            𝟙 (L.obj (F.obj (G.obj X))) ≫ L.map (q.adj₂.counit.app X) ≫ 𝟙 (L.obj X))) ↔
    ∀ (X : D), Mono (X := F.obj X) (q.adj₃.unit.app (F.obj X))

Tactic:
simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.id_obj,
    whiskerLeft_app, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.id_obj, CategoryTheory.NatIso.isIso_inv_app, CategoryTheory.Category.id_comp