-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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))
⊢ { homEquiv := @e, homEquiv_comp := @he : F.RepresentableBy Y } = { homEquiv := @e', homEquiv_comp := @he' }
have 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' }
Tactic: obtain rfl : @e = @e' := by ext; apply this
Cleared hypotheses: e', he', h, this