awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
a : Option C
none :
  Eq.{u + 1} (α := Option C)
    ((fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => Option.some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | Option.some a => of a
            | Option.none => star :
            WithInitial C))
        Option.none))
    Option.none
some :
  ∀ (val : C),
    (fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | of a => Option.some a
            | star => Option.none :
            Option C))
        ((fun (x : Option C) ↦
            (match (motive := Option C → WithInitial C) x with
              | Option.some a => of a
              | Option.none => star :
              WithInitial C))
          (Option.some val)) =
      Option.some val
⊢ (fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => Option.some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | Option.some a => of a
            | Option.none => star :
            WithInitial C))
        a) =
    a

Tactic:
cases a
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{u + 1} (α := Option C)
    ((fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => some a
          | star => none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => of a
            | none => star :
            WithInitial C))
        none))
    none

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
val : C
⊢ (fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => some a
          | star => none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => of a
            | none => star :
            WithInitial C))
        (some val)) =
    some val

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
a : WithInitial C
of :
  ∀ (a : C),
    (fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => WithInitial.of a
            | none => WithInitial.star :
            WithInitial C))
        ((fun (x : WithInitial C) ↦
            (match (motive := WithInitial C → Option C) x with
              | WithInitial.of a => some a
              | WithInitial.star => none :
              Option C))
          (WithInitial.of a)) =
      WithInitial.of a
star :
  Eq.{u + 1} (α := WithInitial C)
    ((fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => WithInitial.of a
          | none => WithInitial.star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | WithInitial.of a => some a
            | WithInitial.star => none :
            Option C))
        WithInitial.star))
    WithInitial.star
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => WithInitial.of a
          | none => WithInitial.star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | WithInitial.of a => some a
            | WithInitial.star => none :
            Option C))
        a) =
    a

Tactic:
cases a
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
a : C
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => of a
          | none => star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        (of a)) =
    of a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{u + 1} (α := WithInitial C)
    ((fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => of a
          | none => star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        star))
    star

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Lemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsFilteredOrEmpty.{v_1, u_1} C
⊢ IsFiltered.{v_1, u_1} (WithInitial C)

Tactic:
have := IsCofiltered.of_equivalence (opEquiv C).symm
  isFiltered_of_isCofiltered_op _

Premises used: CategoryTheory.WithInitial, CategoryTheory.WithInitial.opEquiv, CategoryTheory.isFiltered_of_isCofiltered_op, CategoryTheory.Equivalence.symm, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (obj (obj yoneda X) (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj yoneda X) f) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op Y)))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (obj (obj yoneda X) (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda f.unop) (op Y)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop (op Y))).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj (unop (op X))).obj (op Y)))
        (𝟙 Y) :
      (fun (X : Type v₁) ↦ X) (obj (obj yoneda (unop (op X))) (op Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : C
f : Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (obj yoneda Z) (obj yoneda W)
w :
  ∀ (X : Cᵒᵖ) (x : obj (obj yoneda Z) X),
    TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (NatTrans.app
            (map yoneda
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
                  (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj Z).obj (op Z))) →
                    (fun (X : Type v₁) ↦ X) ((yoneda.obj W).obj (op Z)))
                (𝟙 (unop (op Z)))))
            X))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x
⊢ map yoneda
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj Z).obj (op Z))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj W).obj (op Z)))
        (𝟙 (unop (op Z)))) =
    f

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : C
f : Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (obj yoneda Z) (obj yoneda W)
X : Cᵒᵖ
x : obj (obj yoneda Z) X
⊢ Eq (α := obj (obj yoneda W) (op (unop X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
          (a : (yoneda.obj Z).obj (op (unop X))) → (yoneda.obj W).obj (op (unop X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj yoneda Z) (Quiver.Hom.op x)) :
              (a : (yoneda.obj Z).obj (op Z)) → (yoneda.obj Z).obj (op (unop X)))
            (𝟙 Z) :
          obj (obj yoneda Z) (op (unop X))) :
      obj (obj yoneda W) (op (unop X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj yoneda W) (Quiver.Hom.op x)) :
          (a : (yoneda.obj W).obj (op Z)) → (yoneda.obj W).obj (op (unop X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
              (a : (yoneda.obj Z).obj (op Z)) → (yoneda.obj W).obj (op Z))
            (𝟙 Z) :
          obj (obj yoneda W) (op Z)) :
      obj (obj yoneda W) (op (unop X)))

Tactic:
have := f.naturality_apply x.op (𝟙 Z)
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (obj yoneda X) (obj yoneda Y)
⊢ FullyFaithful.preimage fullyFaithful f =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
        (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj Y).obj (op X)))
      (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Full (C := C) yoneda

Tactic:
fullyFaithful.full

Premises used: CategoryTheory.Yoneda.fullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Faithful (C := C) yoneda

Tactic:
fullyFaithful.faithful

Premises used: CategoryTheory.Yoneda.fullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso (X := obj yoneda X) (map yoneda f)
⊢ IsIso f

Tactic:
isIso_of_fully_faithful yoneda f

Premises used: CategoryTheory.isIso_of_fully_faithful, CategoryTheory.yoneda
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Full (C := C) uliftYoneda.{w, v₁, u₁}

Tactic:
(fullyFaithful C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.ULiftYoneda.fullyFaithful
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Faithful (C := C) uliftYoneda.{w, v₁, u₁}

Tactic:
(fullyFaithful C).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.ULiftYoneda.fullyFaithful
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : Quiver.Hom (V := C ⥤ Type v₁) (obj coyoneda Z) (obj coyoneda W)
w :
  ∀ (X : C) (x : obj (obj coyoneda Z) X),
    TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (NatTrans.app
            (map coyoneda
              (Quiver.Hom.op
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
                    (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj Z).obj (unop Z))) →
                      (fun (X : Type v₁) ↦ X) ((coyoneda.obj W).obj (unop Z)))
                  (𝟙 (unop Z)))))
            X))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x
⊢ map coyoneda
      (Quiver.Hom.op
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj Z).obj (unop Z))) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj W).obj (unop Z)))
          (𝟙 (unop Z)))) =
    f

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : Quiver.Hom (V := C ⥤ Type v₁) (obj coyoneda Z) (obj coyoneda W)
X : C
x : obj (obj coyoneda Z) X
⊢ Eq (α := obj (obj coyoneda W) X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : (coyoneda.obj Z).obj X) → (coyoneda.obj W).obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda Z) x) :
              (a : (coyoneda.obj Z).obj (unop Z)) → (coyoneda.obj Z).obj X)
            (𝟙 (unop Z)) :
          obj (obj coyoneda Z) X) :
      obj (obj coyoneda W) X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda W) x) :
          (a : (coyoneda.obj W).obj (unop Z)) → (coyoneda.obj W).obj X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
              (a : (coyoneda.obj Z).obj (unop Z)) → (coyoneda.obj W).obj (unop Z))
            (𝟙 (unop Z)) :
          obj (obj coyoneda W) (unop Z)) :
      obj (obj coyoneda W) X)

Tactic:
have := f.naturality_apply x (𝟙 (unop Z))
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : Quiver.Hom (V := C ⥤ Type v₁) (obj coyoneda X) (obj coyoneda Y)
⊢ FullyFaithful.preimage fullyFaithful f =
    Quiver.Hom.op
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop X)) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj X).obj (unop X))) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj Y).obj (unop X)))
        (𝟙 (unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Full (C := Cᵒᵖ) coyoneda

Tactic:
fullyFaithful.full

Premises used: CategoryTheory.Coyoneda.fullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Faithful (C := Cᵒᵖ) coyoneda

Tactic:
fullyFaithful.faithful

Premises used: CategoryTheory.Coyoneda.fullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso (X := obj coyoneda X) (map coyoneda f)
⊢ IsIso.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
isIso_of_fully_faithful coyoneda f

Premises used: CategoryTheory.isIso_of_fully_faithful, CategoryTheory.coyoneda
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Full (C := Cᵒᵖ) uliftCoyoneda.{w, v₁, u₁}

Tactic:
(fullyFaithful C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Coyoneda.ULiftCoyoneda.fullyFaithful
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Faithful (C := Cᵒᵖ) uliftCoyoneda.{w, v₁, u₁}

Tactic:
(fullyFaithful C).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.Coyoneda.ULiftCoyoneda.fullyFaithful
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y : C
e : F.RepresentableBy Y
X X' : C
x : F.obj (op X')
f : X ⟶ X'
⊢ Eq.{v + 1} (α := F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X))
        (f ≫
          ((Equiv.symm e.homEquiv : Equiv.{v + 1, v₁ + 1} (F.obj (op X')) (X' ⟶ Y)) : (a : F.obj (op X')) → X' ⟶ Y) x) :
      F.obj (op X))
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X))
        (((Equiv.symm e.homEquiv : Equiv.{v + 1, v₁ + 1} (F.obj (op X)) (X ⟶ Y)) : (a : F.obj (op X)) → X ⟶ Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X'))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
            x)) :
      F.obj (op X))

Tactic:
simp [homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
Y : C
h : F.RepresentableBy Y
X : Cᵒᵖ
X' : C
f : op X' ⟶ X
g : X' ⟶ Y
⊢ Eq.{u_1 + 1} (α := F.obj (op (unop X)))
    (((h.homEquiv : Equiv.{v₁ + 1, u_1 + 1} (unop X ⟶ Y) (F.obj (op (unop X)))) :
          (a : unop X ⟶ Y) → F.obj (op (unop X)))
        (f.unop ≫ g) :
      F.obj (op (unop X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj (op X'))) → (fun (X : Type u_1) ↦ X) (F.obj X))
        (((h.homEquiv : Equiv.{v₁ + 1, u_1 + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
          F.obj (op X')) :
      (fun (X : Type u_1) ↦ X) (F.obj X))

Tactic:
h.homEquiv_comp _ _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
dsimp :
  Eq (α := F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) :
          F.obj (op X)) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          F'.obj (op X')) :
      F'.obj (op X))
⊢ Eq.{v + 1} (α := F'.obj (op X))
    (((Equiv.trans e.homEquiv (Iso.toEquiv (e'.app (op X))) : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F'.obj (op X))) :
          (a : X ⟶ Y) → F'.obj (op X))
        (f ≫ g) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F'.obj (op X'))) → (fun (X : Type v) ↦ X) (F'.obj (op X)))
        (((Equiv.trans e.homEquiv (Iso.toEquiv (e'.app (op X'))) : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F'.obj (op X'))) :
              (a : X' ⟶ Y) → F'.obj (op X'))
            g :
          F'.obj (op X')) :
      (fun (X : Type v) ↦ X) (F'.obj (op X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
rw :
  Eq (α := F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X'))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          (fun (X : Type v) ↦ X) (F.obj (op X))) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          F'.obj (op X')) :
      F'.obj (op X))
⊢ Eq (α := F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) :
          F.obj (op X)) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          F'.obj (op X')) :
      F'.obj (op X))

Tactic:
rw [e.homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ Eq (α := F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X'))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          (fun (X : Type v) ↦ X) (F.obj (op X))) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          F'.obj (op X')) :
      F'.obj (op X))

Tactic:
apply e'.hom.naturality_apply

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e : F.CorepresentableBy X
Y Y' : C
y : F.obj Y
g : Y ⟶ Y'
⊢ Eq.{v + 1} (α := F.obj Y')
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y') (F.obj Y')) : (a : X ⟶ Y') → F.obj Y')
        (((Equiv.symm e.homEquiv : Equiv.{v + 1, v₁ + 1} (F.obj Y) (X ⟶ Y)) : (a : F.obj Y) → X ⟶ Y) y ≫ g) :
      F.obj Y')
    (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y') (F.obj Y')) : (a : X ⟶ Y') → F.obj Y')
        (((Equiv.symm e.homEquiv : Equiv.{v + 1, v₁ + 1} (F.obj Y') (X ⟶ Y')) : (a : F.obj Y') → X ⟶ Y')
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj Y'))
            y)) :
      F.obj Y')

Tactic:
simp [homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
dsimp :
  Eq (α := F'.obj Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y') : (a : F.obj Y') → F'.obj Y')
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y') (F.obj Y')) : (a : X ⟶ Y') → F.obj Y') (f ≫ g) : F.obj Y') :
      F'.obj Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map g) : (a : F'.obj Y) → F'.obj Y')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app Y) : (a : F.obj Y) → F'.obj Y)
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
          F'.obj Y) :
      F'.obj Y')
⊢ Eq.{v + 1} (α := F'.obj Y')
    ((Equiv.trans e.homEquiv (e'.app Y').toEquiv : (a : X ⟶ Y') → F'.obj Y') (f ≫ g) : F'.obj Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map g) :
          (a : (fun (X : Type v) ↦ X) (F'.obj Y)) → (fun (X : Type v) ↦ X) (F'.obj Y'))
        ((Equiv.trans e.homEquiv (e'.app Y).toEquiv : (a : X ⟶ Y) → F'.obj Y) f : F'.obj Y) :
      (fun (X : Type v) ↦ X) (F'.obj Y'))

Tactic:
dsimp