awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A A' : Functor.{v, w, u, w + 1} C (Type w)
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
rw :
  F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ')) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A'.map φ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A'.obj Δ'))
              a :
            (fun (X : Type w) ↦ X) (A'.obj Δ'))) =
    F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
            (a : (fun (X : Type w) ↦ X) (A.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
              a :
            (fun (X : Type w) ↦ X) (A.obj Δ)))
⊢ F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ')) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A'.map φ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A'.obj Δ'))
              a :
            (fun (X : Type w) ↦ X) (A'.obj Δ'))) =
    x.app Δ
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
          a) ≫
      G.map φ
have rw₁ : F.map φ ≫
    x.app Δ'
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) : (a : A.obj Δ) → A.obj Δ')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) : (a : A'.obj Δ) → A.obj Δ) a : A.obj Δ)) =
  F.map φ ≫
    x.app Δ'
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
          (a : (fun (X : Type w) ↦ X) (A.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
              (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
            a :
          (fun (X : Type w) ↦ X) (A.obj Δ)))
Tactic: rw [← x.naturality φ (f.app Δ a), f.naturality_apply φ a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A A' : (Functor.{v, w, u, w + 1} C (Type w))ᵒᵖ
f : A ⟶ A'
x : HomObj.{w, v', v, u, u'} F G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))) =
    x.app X
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
          a) ≫
      G.map φ
have rw : F.map φ ≫
    x.app Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))) =
  F.map φ ≫
    x.app Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)))
Tactic: rw [← HomObj.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A A' : (Functor.{v, w, u, w + 1} C (Type w))ᵒᵖ
f : A ⟶ A'
x : HomObj.{w, v', v, u, u'} F G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))) =
    F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)))
have e_a : Eq (α := (Opposite.unop A).obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
        (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
          a :
        (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) :
    (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
        (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
          a :
        (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) :
    (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
⊢ x.app = y.app
have h₁ : ∀ (x_1 : C) (x_2 : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) x_1), x.app x_1 x_2 = y.app x_1 x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X Y : C
f : X ⟶ Y
a : A.obj X
⊢ F.map f ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Y) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
              (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
            a))
        Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
          a)
        X (𝟙 (Opposite.unop (Opposite.op X))) ≫
      G.map f
have rw : Eq (α := F.obj X ⟶ G.obj Y)
  (F.map f ≫
    HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Y) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y)) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) → (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
          a))
      Y (𝟙 (Opposite.unop (Opposite.op Y))))
  (F.map f ≫
    HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
        a)
      Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) f) :
          (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
            (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
        (𝟙 (Opposite.unop (Opposite.op X)))))
Tactic: rw [← (φ.app X a).naturality f (𝟙 _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X Y : C
f : X ⟶ Y
a : A.obj X
⊢ Eq (α := F.obj X ⟶ G.obj Y)
    (F.map f ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Y) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
              (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
            a))
        Y (𝟙 (Opposite.unop (Opposite.op Y))))
    (F.map f ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
          a)
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) f) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
          (𝟙 (Opposite.unop (Opposite.op X)))))
have this : Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
  (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f ≫ φ.app Y) : (a : A.obj X) → (F.functorHom G).obj Y) a) Y
    (𝟙 (Opposite.unop (Opposite.op Y))))
  (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X ≫ (F.functorHom G).map f) :
        (a : A.obj X) → (F.functorHom G).obj Y)
      a)
    Y (𝟙 (Opposite.unop (Opposite.op Y))))
Tactic: have := HomObj.congr_app (ConcreteCategory.congr_hom (φ.naturality f) a) Y (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A : C ⥤ Type (max u v v')
x : F.HomObj G A
X Y : C
f : X ⟶ Y
⊢ (A.map f ≫
      ↾fun (a : A.obj Y) ↦
        {
          app := fun (Y_1 : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) Y_1) ↦
            x.app Y_1
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op Y)))) →
                    (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y_1))
                a),
          naturality := ⋯ }) =
    (↾fun (a : A.obj X) ↦
        {
          app := fun (Y : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) Y) ↦
            x.app Y
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op X)))) →
                    (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
                a),
          naturality := ⋯ : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) X)) }) ≫
      (F.functorHom G).map f
have h : ∀ (x_1 : A.obj X) (Y_1 : C) (f_1 : Y ⟶ Y_1),
  HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (A.map f ≫
            ↾fun (a : A.obj Y) ↦
              {
                app := fun (Y_2 : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) Y_2) ↦
                  x.app Y_2
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                        (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op Y)))) →
                          (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y_2))
                      a),
                naturality := sorry : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) }))
        x_1)
      Y_1 f_1 =
    (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (a : A.obj X) ↦
                {
                  app := fun (Y : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) Y) ↦
                    x.app Y
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                          (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op X)))) →
                            (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
                        a),
                  naturality := sorry : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) X)) }) ≫
              (F.functorHom G).map f))
          x_1).app
      Y_1 f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ F.map φ ≫
      (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        Y =
    (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        X ≫
      G.map φ
have rw : Eq (α := F.obj X ⟶ G.obj Y)
  (F.map φ ≫
    (fun (X : C) ↦
        (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                  (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
              PUnit.unit)
            X (𝟙 (Opposite.unop (Opposite.op X))) :
          F.obj X ⟶ G.obj X))
      Y)
  (F.map φ ≫
    HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
        PUnit.unit)
      Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
          (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
            (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
        (𝟙 (Opposite.unop (Opposite.op X)))))
Tactic: rw [← (f.app X (PUnit.unit)).naturality φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ Eq (α := F.obj X ⟶ G.obj Y)
    (F.map φ ≫
      (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        Y)
    (F.map φ ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
          PUnit.unit)
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
          (𝟙 (Opposite.unop (Opposite.op X)))))
have e_a : Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
  ((fun (X : C) ↦
      (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
              (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
            PUnit.unit)
          X (𝟙 (Opposite.unop (Opposite.op X))) :
        F.obj X ⟶ G.obj X))
    Y)
  (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
      PUnit.unit)
    Y
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
        (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
          (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
      (𝟙 (Opposite.unop (Opposite.op X)))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    ((fun (X : C) ↦
        (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                  (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
              PUnit.unit)
            X (𝟙 (Opposite.unop (Opposite.op X))) :
          F.obj X ⟶ G.obj X))
      Y)
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
        PUnit.unit)
      Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
          (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
            (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
        (𝟙 (Opposite.unop (Opposite.op X)))))
have this : Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
  (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) φ ≫ f.app Y) :
        (a : (𝟙_ (C ⥤ Type (max v' v u))).obj X) → (F.functorHom G).obj Y)
      PUnit.unit)
    Y (𝟙 Y))
  (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ≫ (F.functorHom G).map φ) :
        (a : (𝟙_ (C ⥤ Type (max v' v u))).obj X) → (F.functorHom G).obj Y)
      PUnit.unit)
    Y (𝟙 Y))
Tactic: have := HomObj.congr_app (ConcreteCategory.congr_hom (f.naturality φ) PUnit.unit) Y (𝟙 Y)