awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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
⊢ F.partialLeftAdjointMap (f ≫ g) = F.partialLeftAdjointMap f ≫ F.partialLeftAdjointMap g
have 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))
Tactic: apply F.partialLeftAdjointHomEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (hypothesis)
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 = ⊤
⊢ F.IsRightAdjoint
have h₁ : ∀ (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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 = ⊤
have refine : ∀ (h : F.IsRightAdjoint), F.leftAdjointObjIsDefined = ⊤
Tactic: refine ⟨fun h ↦ ?_, isRightAdjoint_of_leftAdjointObjIsDefined_eq_top⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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
⊢ F.leftAdjointObjIsDefined = ⊤
have h₁ : ∀ (X : C), F.leftAdjointObjIsDefined X ↔ ⊤ X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 (α := (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)) φ)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 (α := (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))
have 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)
Tactic: rw [comp_id, ← c'.w φ, ← partialLeftAdjointHomEquiv_map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (hypothesis)
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'
⊢ Eq.{v₁ + 1} (α :=
    (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j') →
            (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j'))
        ((R ⋙ F.partialLeftAdjoint).map φ ≫
          ((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1}
                  ((R.obj j').obj (P := F.leftAdjointObjIsDefined) ⟶
                    F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
                  (F.partialLeftAdjointObj (R.obj j') ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')) :
              (a : (R.obj j').obj ⟶ F.obj (((const J).obj Y).obj j')) →
                F.partialLeftAdjointObj (R.obj j') ⟶ ((const J).obj Y).obj j')
            (c.ι.app j' ≫ g)) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
    (((F.partialLeftAdjointHomEquiv :
            Equiv.{v₂ + 1, v₁ + 1} (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j')
              ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))) :
          (a : F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j') →
            (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j'))
        (((Equiv.symm F.partialLeftAdjointHomEquiv :
                Equiv.{v₁ + 1, v₂ + 1}
                  ((R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j))
                  (F.partialLeftAdjointObj (R.obj j) ⟶ obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j)) :
              (a : (R.obj j).obj ⟶ F.obj (((const J).obj Y).obj j)) →
                F.partialLeftAdjointObj (R.obj j) ⟶ ((const J).obj Y).obj j)
            (c.ι.app j ≫ g) ≫
          map (obj (const J) Y) φ) :
      (R.obj j).obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj (obj.{v_1, v₂, u_1, u₂} (obj (const J) Y) j'))
have this : (R ⋙ F.leftAdjointObjIsDefined.ι).map φ ≫ c.ι.app j' = c.ι.app j
Tactic: have := c.w φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ 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)
        (f ≫ F.partialRightAdjointMap g) :
      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)
          f ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
have rw : Eq (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
  (F.map f ≫
    ((F.partialRightAdjointHomEquiv :
          Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y')
            (F.obj (F.partialRightAdjointObj Y) ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))) :
        (a : F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y') → F.obj (F.partialRightAdjointObj Y) ⟶ Y'.obj)
      (F.partialRightAdjointMap 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 ≫
    g.hom)
Tactic: rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map,
    ← assoc, ← partialRightAdjointHomEquiv_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
rw :
  Eq (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
    (F.map f ≫
      ((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y')
              (F.obj (F.partialRightAdjointObj Y) ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y') → F.obj (F.partialRightAdjointObj Y) ⟶ Y'.obj)
        (F.partialRightAdjointMap 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 ≫
      g.hom)
⊢ 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)
        (f ≫ F.partialRightAdjointMap g) :
      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)
          f ≫
        g.hom :
      F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
have rw₁ : Eq (α := F.obj X ⟶ Y'.obj (P := F.rightAdjointObjIsDefined))
  (F.map f ≫
    ((F.partialRightAdjointHomEquiv :
            Equiv.{v₁ + 1, v₂ + 1} (F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y)
              (F.obj (F.partialRightAdjointObj Y) ⟶ Y.obj (P := F.rightAdjointObjIsDefined))) :
          (a : F.partialRightAdjointObj Y ⟶ F.partialRightAdjointObj Y) → F.obj (F.partialRightAdjointObj Y) ⟶ Y.obj)
        (𝟙 (F.partialRightAdjointObj Y)) ≫
      g.hom)
  (((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 ≫
    g.hom)
Tactic: rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map,
    ← assoc, ← partialRightAdjointHomEquiv_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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
⊢ F.partialRightAdjointMap (𝟙 X) = 𝟙 (F.partialRightAdjointObj X)
have 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))
Tactic: apply F.partialRightAdjointHomEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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
⊢ F.partialRightAdjointMap (f ≫ g) = F.partialRightAdjointMap f ≫ F.partialRightAdjointMap g
have 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))
Tactic: apply F.partialRightAdjointHomEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (hypothesis)
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 = ⊤
⊢ F.IsLeftAdjoint
have h₁ : ∀ (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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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 = ⊤
have refine : ∀ (h : F.IsLeftAdjoint), F.rightAdjointObjIsDefined = ⊤
Tactic: refine ⟨fun h ↦ ?_, isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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
⊢ F.rightAdjointObjIsDefined = ⊤
have h₁ : ∀ (X : D), F.rightAdjointObjIsDefined X ↔ ⊤ X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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} (α := 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')
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.PartialAdjoint (goal)
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.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))
have 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))
Tactic: rw [id_comp, ← c'.w φ, ← partialRightAdjointHomEquiv_map_comp,
              ← assoc]