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

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

Premises used: rfl