-- 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 : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)
he :
  ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y') ((e : (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'))
          ((e : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
        (fun (X : Type v) ↦ X) (F.obj Y'))
e' : {Y : C} → Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)
he' :
  ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y') ((e' : (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'))
          ((e' : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
        (fun (X : Type v) ↦ X) (F.obj Y'))
h :
  Eq.{v + 1} (α := F.obj X)
    ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
    ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    Eq.{v + 1} (α := F.obj Y)
      ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
            (a : X ⟶ Y) → F.obj Y)
          f :
        F.obj Y)
      ((({ homEquiv := @e', homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
            (a : X ⟶ Y) → F.obj Y)
          f :
        F.obj Y)
obtain :
  ∀
    (he' :
      ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
        Eq.{v + 1} (α := F.obj Y') ((e : (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'))
              ((e : (a : X ⟶ Y) → F.obj Y) f : F.obj Y) :
            (fun (X : Type v) ↦ X) (F.obj Y')))
    (h :
      Eq.{v + 1} (α := F.obj X)
        ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
              (a : X ⟶ X) → F.obj X)
            (𝟙 X) :
          F.obj X)
        ((({ homEquiv := @e, homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ X) (F.obj X)) :
              (a : X ⟶ X) → F.obj X)
            (𝟙 X) :
          F.obj X))
    (this :
      ∀ {Y : C} (f : X ⟶ Y),
        Eq.{v + 1} (α := F.obj Y)
          ((({ homEquiv := @e, homEquiv_comp := @he }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
                (a : X ⟶ Y) → F.obj Y)
              f :
            F.obj Y)
          ((({ homEquiv := @e, homEquiv_comp := @he' }.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj Y)) :
                (a : X ⟶ Y) → F.obj Y)
              f :
            F.obj Y)),
    { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = { homEquiv := @e, homEquiv_comp := @he' }
⊢ { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = { homEquiv := @e', homEquiv_comp := @he' }

Tactic:
obtain rfl : @e = @e' := by ext; apply this

Premises used: rfl