awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
j : J
rw :
  ((adj₂.homEquiv :
          Equiv.{v_3 + 1, v_2 + 1} ((F.obj (unop (P.obj j))).obj s.pt ⟶ X₃)
            (s.pt ⟶ (G.obj (op (unop (P.obj j)))).obj X₃)) :
        (a : (F.obj (unop (P.obj j))).obj s.pt ⟶ X₃) → s.pt ⟶ (G.obj (P.obj j)).obj X₃)
      ((cocone s).ι.app (op j)) =
    s.π.app j
⊢ ((adj₂.homEquiv :
            Equiv.{v_3 + 1, v_2 + 1} ((F.obj (unop c.1)).obj s.pt ⟶ X₃) (s.pt ⟶ (G.obj (op (unop c.1))).obj X₃)) :
          (a : (F.obj (unop c.1)).obj s.pt ⟶ X₃) → s.pt ⟶ (G.obj c.1).obj X₃)
        ((hc' s).desc (cocone s)) ≫
      (G.map (c.π.app j)).app X₃ =
    s.π.app j

Tactic:
rw [← dsimp% adj₂.homEquiv_naturality_one (c.π.app j).unop,
          dsimp% (hc' s).fac (cocone s) (op j)]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cone.π, Quiver.Hom.unop, Opposite.op, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
j : J
⊢ ((adj₂.homEquiv :
          Equiv.{v_3 + 1, v_2 + 1} ((F.obj (unop (P.obj j))).obj s.pt ⟶ X₃)
            (s.pt ⟶ (G.obj (op (unop (P.obj j)))).obj X₃)) :
        (a : (F.obj (unop (P.obj j))).obj s.pt ⟶ X₃) → s.pt ⟶ (G.obj (P.obj j)).obj X₃)
      ((cocone s).ι.app (op j)) =
    s.π.app j

Tactic:
simp [cocone]
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
m : s.pt ⟶ ((G.flip.obj X₃).mapCone c).pt
hm : ∀ (j : J), m ≫ ((G.flip.obj X₃).mapCone c).π.app j = s.π.app j
simp :
  Eq.{v_3 + 1} (α := (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    (((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj c.1).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
          (a : s.pt ⟶ (G.obj c.1).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
        m :
      (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    ((hc' s).desc (cocone s) : ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)).pt ⟶ (cocone s).pt)
⊢ Eq.{v_3 + 1} (α := (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    (((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj (op (unop c.1))).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
          (a : s.pt ⟶ (G.obj (op (unop c.1))).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
        m :
      (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    (((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj (op (unop c.1))).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
          (a : s.pt ⟶ (G.obj (op (unop c.1))).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
        (((adj₂.homEquiv :
              Equiv.{v_3 + 1, v_2 + 1} ((F.obj (unop c.1)).obj s.pt ⟶ X₃) (s.pt ⟶ (G.obj (op (unop c.1))).obj X₃)) :
            (a : (F.obj (unop c.1)).obj s.pt ⟶ X₃) → s.pt ⟶ (G.obj (op (unop c.1))).obj X₃)
          ((hc' s).desc (cocone s))) :
      (F.obj (unop c.1)).obj s.pt ⟶ X₃)

Tactic:
simp only [op_unop, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Opposite.op_unop
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
m : s.pt ⟶ ((G.flip.obj X₃).mapCone c).pt
hm : ∀ (j : J), m ≫ ((G.flip.obj X₃).mapCone c).π.app j = s.π.app j
⊢ Eq.{v_3 + 1} (α := (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    (((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj c.1).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
          (a : s.pt ⟶ (G.obj c.1).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
        m :
      (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    ((hc' s).desc (cocone s) : ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)).pt ⟶ (cocone s).pt)

Tactic:
(hc' s).uniq (cocone s) _ (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
m : s.pt ⟶ ((G.flip.obj X₃).mapCone c).pt
hm : ∀ (j : J), m ≫ ((G.flip.obj X₃).mapCone c).π.app j = s.π.app j
refine :
  ∀ (j : Jᵒᵖ),
    ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)).ι.app j ≫
        ((Equiv.symm adj₂.homEquiv :
              Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj c.1).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
            (a : s.pt ⟶ (G.obj c.1).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
          m =
      (cocone s).ι.app j
⊢ Eq.{v_3 + 1} (α := (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    (((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj c.1).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
          (a : s.pt ⟶ (G.obj c.1).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
        m :
      (F.obj (unop c.1)).obj s.pt ⟶ X₃)
    ((hc' s).desc (cocone s) : ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)).pt ⟶ (cocone s).pt)

Tactic:
refine (hc' s).uniq (cocone s) _ (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
m : s.pt ⟶ ((G.flip.obj X₃).mapCone c).pt
hm : ∀ (j : J), m ≫ ((G.flip.obj X₃).mapCone c).π.app j = s.π.app j
j : Jᵒᵖ
⊢ ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)).ι.app j ≫
      ((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1} (s.pt ⟶ (G.obj c.1).obj X₃) ((F.obj (unop c.1)).obj s.pt ⟶ X₃)) :
          (a : s.pt ⟶ (G.obj c.1).obj X₃) → (F.obj (unop c.1)).obj s.pt ⟶ X₃)
        m =
    (cocone s).ι.app j

Tactic:
simp [cocone, ← hm,
          dsimp% adj₂.homEquiv_symm_naturality_one (c.π.app j.unop).unop]

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one, Quiver.Hom.unop, Opposite.unop, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
⊢ IsLimit ((G.flip.obj X₃).mapCone c)

Tactic:
exact {
      lift s := adj₂.homEquiv ((hc' s).desc (cocone s))
      fac s j := by
        dsimp
        rw [← dsimp% adj₂.homEquiv_naturality_one (c.π.app j).unop,
          dsimp% (hc' s).fac (cocone s) (op j)]
        simp [cocone]
      uniq s m hm := adj₂.homEquiv.symm.injective (by
        simp only [op_unop, Equiv.symm_apply_apply]
        refine (hc' s).uniq (cocone s) _ (fun j ↦ ?_)
        simp [cocone, ← hm,
          dsimp% adj₂.homEquiv_symm_naturality_one (c.π.app j.unop).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₁} D C
X : C
⊢ F.leftAdjointObjIsDefined X ↔ (F ⋙ obj coyoneda (op X)).IsCorepresentable

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₁} D C
G : Functor.{v₁, v₂, u₁, u₂} C D
adj : G ⊣ F
X : C
⊢ F.leftAdjointObjIsDefined X

Tactic:
(adj.corepresentableBy X).isCorepresentable

Premises used: CategoryTheory.Adjunction.corepresentableBy, CategoryTheory.Functor.CorepresentableBy.isCorepresentable, 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
X : F.PartialLeftAdjointSource
⊢ (F ⋙ obj coyoneda (op (X.obj (P := F.leftAdjointObjIsDefined)))).IsCorepresentable

Tactic:
X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, 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
X : F.PartialLeftAdjointSource
Y Y' : D
f : F.partialLeftAdjointObj X ⟶ Y
g : Y ⟶ Y'
⊢ Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ Y')
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')) :
          (a : F.partialLeftAdjointObj X ⟶ Y') → X.obj ⟶ F.obj Y')
        (f ≫ g) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
    (((F.partialLeftAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ Y)
                (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)) :
            (a : F.partialLeftAdjointObj X ⟶ Y) → X.obj ⟶ F.obj Y)
          f ≫
        F.map g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ 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
X Y : F.PartialLeftAdjointSource
f : X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Y))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Y)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Y))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Y) → X.obj ⟶ F.obj (F.partialLeftAdjointObj Y))
        (F.partialLeftAdjointMap f) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Y))
    (f.hom ≫
        ((F.partialLeftAdjointHomEquiv :
              Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj Y ⟶ F.partialLeftAdjointObj Y)
                (Y.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Y))) :
            (a : F.partialLeftAdjointObj Y ⟶ F.partialLeftAdjointObj Y) → Y.obj ⟶ F.obj (F.partialLeftAdjointObj Y))
          (𝟙 (F.partialLeftAdjointObj Y)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj Y))

Tactic:
simp [partialLeftAdjointMap]

Premises used: CategoryTheory.Functor.partialLeftAdjointMap
-- 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 : F.PartialLeftAdjointSource
Y Y' : D
f : X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y
g : Y ⟶ Y'
⊢ Eq.{v₂ + 1} (α := F.partialLeftAdjointObj X ⟶ Y')
    (((Equiv.symm F.partialLeftAdjointHomEquiv :
              Equiv.{v₁ + 1, v₂ + 1} (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
                (F.partialLeftAdjointObj X ⟶ Y)) :
            (a : X.obj ⟶ F.obj Y) → F.partialLeftAdjointObj X ⟶ Y)
          f ≫
        g :
      F.partialLeftAdjointObj X ⟶ Y')
    (((Equiv.symm F.partialLeftAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y')
              (F.partialLeftAdjointObj X ⟶ Y')) :
          (a : X.obj ⟶ F.obj Y') → F.partialLeftAdjointObj X ⟶ Y')
        (f ≫ F.map g) :
      F.partialLeftAdjointObj X ⟶ Y')

Tactic:
CorepresentableBy.homEquiv_symm_comp ..

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_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
X : F.PartialLeftAdjointSource
a :
  Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X) → X.obj ⟶ F.obj (F.partialLeftAdjointObj X))
        (F.partialLeftAdjointMap (𝟙 X)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X) → X.obj ⟶ F.obj (F.partialLeftAdjointObj X))
        (𝟙 (F.partialLeftAdjointObj X)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))
⊢ F.partialLeftAdjointMap (𝟙 X) = 𝟙 (F.partialLeftAdjointObj X)

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 : F.PartialLeftAdjointSource
⊢ Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X) → X.obj ⟶ F.obj (F.partialLeftAdjointObj X))
        (F.partialLeftAdjointMap (𝟙 X)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X)
              (X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))) :
          (a : F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj X) → X.obj ⟶ F.obj (F.partialLeftAdjointObj X))
        (𝟙 (F.partialLeftAdjointObj X)) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (F.partialLeftAdjointObj X))

Tactic:
simp [partialLeftAdjointHomEquiv_map]

Premises used: CategoryTheory.Functor.partialLeftAdjointHomEquiv_map