-- 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)
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)
⊢ { homEquiv := @e, homEquiv_comp := @he : F.CorepresentableBy X } = { homEquiv := @e', homEquiv_comp := @he' }
have 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' }
Tactic: obtain rfl : @e = @e' := by ext; apply this
Cleared hypotheses: e', he', h, this