awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.ParametrizedLimits (goal)
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 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)) ≫
      ((G.flip.obj X₃).mapCone c).π.app j =
    s.π.app j
have dsimp : ((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: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.ParametrizedLimits (goal)
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 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
have 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
Tactic: rw [← dsimp% adj₂.homEquiv_naturality_one (c.π.app j).unop,
          dsimp% (hc' s).fac (cocone s) (op j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.ParametrizedLimits (goal)
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 (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₃)
have 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)
Tactic: simp only [op_unop, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.ParametrizedLimits (goal)
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)
have 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
Tactic: refine (hc' s).uniq (cocone s) _ (fun j ↦ ?_)
-- 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 X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ 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.partialLeftAdjointMap f ≫ g) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (f.hom ≫
        ((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)
          g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
have rw : Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
  (((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 f) ≫
      F.map g :
    X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
  (f.hom ≫
      ((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)
        g :
    X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
Tactic: rw [partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc,
    ← partialLeftAdjointHomEquiv_comp, id_comp]
-- 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 X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
rw :
  Eq.{v₁ + 1} (α := X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (((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 f) ≫
        F.map g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (f.hom ≫
        ((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)
          g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj 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.partialLeftAdjointMap f ≫ g) :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
    (f.hom ≫
        ((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)
          g :
      X.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y)
have rw₁ : (f.hom ≫
      ((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'))) ≫
    F.map g =
  f.hom ≫
    ((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)
      g
Tactic: rw [partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc,
    ← partialLeftAdjointHomEquiv_comp, id_comp]
-- 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 X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y
g : X ⟶ X'
⊢ Eq (α := F.partialLeftAdjointObj X ⟶ Y)
    (F.partialLeftAdjointMap g ≫
      ((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)
    (((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)
      (g.hom ≫ f))
have rw : ((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.partialLeftAdjointMap g ≫
      ((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.hom ≫ f
Tactic: rw [Equiv.eq_symm_apply, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map,
    assoc, ← partialLeftAdjointHomEquiv_comp, id_comp, Equiv.apply_symm_apply]
-- 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 X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y
g : X ⟶ X'
rw :
  ((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.partialLeftAdjointMap g ≫
        ((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.hom ≫ f
⊢ Eq (α := F.partialLeftAdjointObj X ⟶ Y)
    (F.partialLeftAdjointMap g ≫
      ((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)
    (((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)
      (g.hom ≫ f))
have rw₁ : CategoryStruct.comp (Y := 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 g))
    (F.map
      (((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.hom ≫ f
Tactic: rw [Equiv.eq_symm_apply, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map,
    assoc, ← partialLeftAdjointHomEquiv_comp, id_comp, Equiv.apply_symm_apply]
-- 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 X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj (P := F.leftAdjointObjIsDefined) ⟶ F.obj Y
g : X ⟶ X'
rw :
  ((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.partialLeftAdjointMap g ≫
        ((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.hom ≫ f
rw₁ :
  CategoryStruct.comp (Y := 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 g))
      (F.map
        (((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.hom ≫ f
⊢ Eq (α := F.partialLeftAdjointObj X ⟶ Y)
    (F.partialLeftAdjointMap g ≫
      ((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)
    (((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)
      (g.hom ≫ f))
have rw₂ : CategoryStruct.comp (Y := F.obj (F.partialLeftAdjointObj X'))
    (g.hom ≫
      ((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')))
    (F.map
      (((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.hom ≫ f
Tactic: rw [Equiv.eq_symm_apply, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map,
    assoc, ← partialLeftAdjointHomEquiv_comp, id_comp, Equiv.apply_symm_apply]
-- 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 : F.PartialLeftAdjointSource
⊢ F.partialLeftAdjointMap (𝟙 X) = 𝟙 (F.partialLeftAdjointObj X)
have 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))
Tactic: apply F.partialLeftAdjointHomEquiv.injective