awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Type u
inst_1 : Groupoid.{v, u} G
F : Functor.{v, w, u, w + 1} G (Type w)
X Y : F.Elements
x : X ⟶ Y
⊢ x ≫
      Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
            (Y.snd (β := fun (c : G) ↦ F.obj c)) =
          X.snd (β := fun (c : G) ↦ F.obj c))
        (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) ⋯ =
    𝟙 X
have w : (↑(x ≫
        Subtype.mk (p := fun (f : Y.fst (β := fun (c : G) ↦ F.obj c) ⟶ X.fst (β := fun (c : G) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj Y.fst)) → (fun (X : Type w) ↦ X) (F.obj X.fst))
              (Y.snd (β := fun (c : G) ↦ F.obj c)) =
            X.snd (β := fun (c : G) ↦ F.obj c))
          (Groupoid.inv (↑x : X.fst ⟶ Y.fst)) sorry) :
    X.fst ⟶ X.fst) =
  (↑(𝟙 X) : X.fst ⟶ X.fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : F.Elements
f : A ⟶ B
h : IsIso ((π F).map f)
⊢ IsIso f
have refine_1 : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (inv ((π F).map f))) :
      (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
    (B.snd (β := fun (c : C) ↦ F.obj c)) =
  A.snd (β := fun (c : C) ↦ F.obj c)
Tactic: refine ⟨⟨(inv ((π F).map f) :), ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : F.Elements
f : A ⟶ B
h : IsIso ((π F).map f)
refine_1 :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (inv ((π F).map f))) :
        (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
      (B.snd (β := fun (c : C) ↦ F.obj c)) =
    A.snd (β := fun (c : C) ↦ F.obj c)
⊢ IsIso f
have refine_2 : f ≫
    Subtype.mk (p := fun (f : B.fst (β := fun (c : C) ↦ F.obj c) ⟶ A.fst (β := fun (c : C) ↦ F.obj c)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
          (B.snd (β := fun (c : C) ↦ F.obj c)) =
        A.snd (β := fun (c : C) ↦ F.obj c))
      (inv ((π F).map f)) sorry =
  𝟙 A
Tactic: refine ⟨⟨(inv ((π F).map f) :), ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : F.Elements
f : A ⟶ B
h : IsIso ((π F).map f)
refine_1 :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (inv ((π F).map f))) :
        (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
      (B.snd (β := fun (c : C) ↦ F.obj c)) =
    A.snd (β := fun (c : C) ↦ F.obj c)
refine_2 :
  f ≫
      Subtype.mk (p := fun (f : B.fst (β := fun (c : C) ↦ F.obj c) ⟶ A.fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
            (B.snd (β := fun (c : C) ↦ F.obj c)) =
          A.snd (β := fun (c : C) ↦ F.obj c))
        (inv ((π F).map f)) ⋯ =
    𝟙 A
⊢ IsIso f
have refine_3 : Subtype.mk (p := fun (f : B.fst (β := fun (c : C) ↦ F.obj c) ⟶ A.fst (β := fun (c : C) ↦ F.obj c)) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w) ↦ X) (F.obj B.fst)) → (fun (X : Type w) ↦ X) (F.obj A.fst))
          (B.snd (β := fun (c : C) ↦ F.obj c)) =
        A.snd (β := fun (c : C) ↦ F.obj c))
      (inv ((π F).map f)) sorry ≫
    f =
  𝟙 B
Tactic: refine ⟨⟨(inv ((π F).map f) :), ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : F.Elements
f : X ⟶ Y
⊢ StructuredArrow.hom
        (StructuredArrow.mk (Y := X.fst (β := fun (c : C) ↦ F.obj c))
          (↾fun (x : PUnit.{w + 1}) ↦ X.snd (β := fun (c : C) ↦ F.obj c))) ≫
      F.map (↑f : X.fst ⟶ Y.fst) =
    StructuredArrow.hom
      (StructuredArrow.mk (Y := Y.fst (β := fun (c : C) ↦ F.obj c))
        (↾fun (x : PUnit.{w + 1}) ↦ Y.snd (β := fun (c : C) ↦ F.obj c)))
have h : ∀ (x : PUnit.{w + 1}),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (StructuredArrow.hom
              (StructuredArrow.mk (Y := X.fst (β := fun (c : C) ↦ F.obj c))
                (↾fun (x : PUnit.{w + 1}) ↦ X.snd (β := fun (c : C) ↦ F.obj c))) ≫
            F.map (↑f : X.fst ⟶ Y.fst))).toFun
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (StructuredArrow.hom
          (StructuredArrow.mk (Y := Y.fst (β := fun (c : C) ↦ F.obj c))
            (↾fun (x : PUnit.{w + 1}) ↦ Y.snd (β := fun (c : C) ↦ F.obj c)))))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
        (a :
            (fun (X : Type w) ↦ X)
              (F.obj
                (F.elementsMk X.right
                    ((ConcreteCategory.hom X.hom :
                        (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj X.right))
                      PUnit.unit)).fst)) →
          (fun (X : Type w) ↦ X)
            (F.obj
              (F.elementsMk Y.right
                  ((ConcreteCategory.hom Y.hom :
                      (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj Y.right))
                    PUnit.unit)).fst))
      ((F.elementsMk X.right
            ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom :
                (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj X.right))
              PUnit.unit)).snd
        (β := fun (c : C) ↦ F.obj c)) =
    (F.elementsMk Y.right
          ((ConcreteCategory.hom (FC := TypeCat.Fun) Y.hom :
              (a : (fun (X : Type w) ↦ X) PUnit.{w + 1}) → (fun (X : Type w) ↦ X) (F.obj Y.right))
            PUnit.unit)).snd
      (β := fun (c : C) ↦ F.obj c)
have simp : Eq (α := F.obj Y.right)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
        (a : F.obj X.right) → F.obj Y.right)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom : (a : PUnit.{w + 1}) → F.obj X.right) PUnit.unit :
        F.obj X.right) :
    F.obj Y.right)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.hom ≫ F.map (StructuredArrow.Hom.right f)) :
        (a : PUnit.{w + 1}) → F.obj Y.right)
      PUnit.unit :
    F.obj Y.right)
Tactic: simp [ConcreteCategory.congr_hom f.w.symm .unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
        (a : (fun (X : Type w) ↦ X) (F.obj ((fromStructuredArrow F).obj X).fst)) →
          (fun (X : Type w) ↦ X) (F.obj ((fromStructuredArrow F).obj Y).fst))
      (((fromStructuredArrow F).obj X).snd (β := fun (c : C) ↦ F.obj c)) =
    ((fromStructuredArrow F).obj Y).snd (β := fun (c : C) ↦ F.obj c)
have simp : Eq (α := F.obj Y.right)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (StructuredArrow.Hom.right f)) :
        (a : F.obj X.right) → F.obj Y.right)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) X.hom : (a : PUnit.{w + 1}) → F.obj X.right) PUnit.unit :
        F.obj X.right) :
    F.obj Y.right)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.hom ≫ F.map (StructuredArrow.Hom.right f)) :
        (a : PUnit.{w + 1}) → F.obj Y.right)
      PUnit.unit :
    F.obj Y.right)
Tactic: simp [ConcreteCategory.congr_hom f.w.symm PUnit.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj yoneda
        (CostructuredArrow.left (S := (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)))
          (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
            CostructuredArrow yoneda F)) ⟶
      F)
    (Functor.map yoneda (↑f.unop : (unop Y).fst ⟶ (unop X).fst).unop ≫
      CostructuredArrow.hom
        (CostructuredArrow.mk (Y := unop (unop Y).1)
          ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop Y).1))) → yoneda.obj (unop (unop Y).1) ⟶ F)
            ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
have w : ∀ (Z : Cᵒᵖ)
  (y :
    Functor.obj
      (Functor.obj yoneda
        (CostructuredArrow.left (S := (yoneda : C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)))
          (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
            CostructuredArrow yoneda F)))
      Z),
  Eq (α := F.obj Z)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map yoneda (↑f.unop : (unop Y).fst ⟶ (unop X).fst).unop ≫
            CostructuredArrow.hom
              (CostructuredArrow.mk (Y := unop (unop Y).1)
                ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop Y).1))) → yoneda.obj (unop (unop Y).1) ⟶ F)
                  ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
          Z))
      y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CostructuredArrow.hom
            (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm yonedaEquiv : (a : F.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
          Z))
      y)
Tactic: ext Z y
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (Iso.hom
              (Iso.refl
                (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                  F.obj c))))) :
        (a : (fun (X : Type v) ↦ X) (F.obj ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst)) →
          (fun (X : Type v) ↦ X) (F.obj (unop X).fst))
      (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)
have simp : (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (unop X).1)) : (a : F.obj (unop X).1) → F.obj (unop X).fst)
    ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
  (unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
x y : F.Elements
f : y ⟶ x
⊢ Eq (α :=
    unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y)) ⟶
      unop (Functor.obj (𝟭 F.Elementsᵒᵖ) (op x)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := Functor.obj (𝟭 F.Elementsᵒᵖ) (op y)) (Functor.map (𝟭 F.Elementsᵒᵖ) (op f))
        (Iso.hom
          ((fun (X : F.Elementsᵒᵖ) ↦
              (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                  (Iso.refl
                    (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                      F.obj c)))
                  ⋯).op)
            (op y)))))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : F.Elementsᵒᵖ) ↦
              (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                  (Iso.refl
                    (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                      F.obj c)))
                  ⋯).op)
            (op x)) ≫
        (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)))
have w : Eq (α :=
  (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c) ⟶
    (unop (Functor.obj (𝟭 F.Elementsᵒᵖ) (op x))).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))
  (↑(Quiver.Hom.unop
        (CategoryStruct.comp (Y := Functor.obj (𝟭 F.Elementsᵒᵖ) (op y)) (Functor.map (𝟭 F.Elementsᵒᵖ) (op f))
          (Iso.hom
            ((fun (X : F.Elementsᵒᵖ) ↦
                (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                    (Iso.refl
                      (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                        F.obj c)))
                    sorry).op)
              (op y))))) :
    (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst ⟶
      (unop ((𝟭 F.Elementsᵒᵖ).obj (op x))).fst)
  (↑(Quiver.Hom.unop
        (Iso.hom
            ((fun (X : F.Elementsᵒᵖ) ↦
                (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                    (Iso.refl
                      (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                        F.obj c)))
                    sorry).op)
              (op x)) ≫
          (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f))) :
    (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst ⟶
      (unop ((𝟭 F.Elementsᵒᵖ).obj (op x))).fst)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : CostructuredArrow yoneda F
⊢ Functor.map yoneda (Iso.hom (Iso.refl (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).left)) ≫
      (Functor.obj (𝟭 (CostructuredArrow yoneda F)) X).hom =
    (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).hom
have dsimp : Functor.map yoneda (𝟙 X.left) ≫ X.hom =
  (Equiv.symm yonedaEquiv : (a : F.obj (op X.left)) → yoneda.obj X.left ⟶ F)
    ((yonedaEquiv : (a : yoneda.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α
have h_obj : ∀ (X : F₁.Elementsᵒᵖ),
  ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
h_obj :
  ∀ (X : F₁.Elementsᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α
have h_map : autoParam
  (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
    ((map α).op ⋙ toCostructuredArrow F₂).map f =
      eqToHom sorry ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom sorry)
  Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
have h_obj : Eq (α := CostructuredArrow yoneda F₂)
  (CostructuredArrow.mk (Y := unop ((map α).obj (unop X)).1)
      ((Equiv.symm yonedaEquiv :
          (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
        (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c))) :
    CostructuredArrow yoneda F₂)
  (CostructuredArrow.mk (Y := unop (unop X).1)
      ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
        α) :
    CostructuredArrow yoneda F₂)
Tactic: simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
      Functor.comp_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ Eq (α := CostructuredArrow yoneda F₂)
    (CostructuredArrow.mk (Y := unop ((map α).obj (unop X)).1)
        ((Equiv.symm yonedaEquiv :
            (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
          (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c))) :
      CostructuredArrow yoneda F₂)
    (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
            ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
          α) :
      CostructuredArrow yoneda F₂)
have h_obj : Eq (α := Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
  ((Equiv.symm yonedaEquiv :
        (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
      (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)) :
    Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
  ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
        ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
      α :
    Functor.obj yoneda (unop (unop X).1) ⟶ F₂)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ Eq (α := Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
    ((Equiv.symm yonedaEquiv :
          (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
        (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)) :
      Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
    ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
        α :
      Functor.obj yoneda (unop (unop X).1) ⟶ F₂)
have h_obj : ∀ (x : Cᵒᵖ) (f : Functor.obj (Functor.obj yoneda (unop ((map α).obj (unop X)).1)) x),
  Eq (α := F₂.obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm yonedaEquiv :
              (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
            (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)))
          x))
      f)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
              ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
            α)
          x))
      f)
Tactic: ext _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj uliftYoneda.{w, v, u}
        (CostructuredArrow.left (S := (uliftYoneda.{w, v, u} : C ⥤ Cᵒᵖ ⥤ Type (max w v)))
          (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm uliftYonedaEquiv :
                  (a : F.obj (op (unop (unop X).1))) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
            CostructuredArrow uliftYoneda.{w, v, u} F)) ⟶
      F)
    (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
      CostructuredArrow.hom
        (CostructuredArrow.mk (Y := unop (unop Y).1)
          ((Equiv.symm uliftYonedaEquiv :
              (a : F.obj (op (unop (unop Y).1))) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
            ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm uliftYonedaEquiv :
            (a : F.obj (op (unop (unop X).1))) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
have dsimp : Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
  (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
    (Equiv.symm uliftYonedaEquiv : (a : F.obj (unop Y).1) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
      ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
  ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
    ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
⊢ Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : F.obj (unop Y).1) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
        ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
have rw : Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
  ((Equiv.symm uliftYonedaEquiv :
        (a : F.obj (op (unop (unop X).fst))) → uliftYoneda.{w, v, u}.obj (unop (unop X).fst) ⟶ F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑(unop f) : (unop Y).fst ⟶ (unop X).fst)) :
          (a : (fun (X : Type (max v w)) ↦ X) (F.obj (unop Y).fst)) →
            (fun (X : Type (max v w)) ↦ X) (F.obj (unop X).fst))
        ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
    Functor.obj uliftYoneda.{w, v, u} (unop ((unop X).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))) ⟶ F)
  ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) :
    Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
Tactic: rw [← uliftYonedaEquiv_symm_map, map_snd]