-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Sphere (goal)
Goal:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x
y : EuclideanSpace ℝ (Fin n)
hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) y
h :
  Eq (α := (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (diskBoundaryInclusion n) :
          (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (diskBoundaryInclusion n) :
          (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
        {
          down :=
            Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
              Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) y hy :
          ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
      (↑(𝔻 n) : Type u_1))
⊢ {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
      ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } =
    {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) y hy }
have obtain : ∀ (hy : Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x)
  (h :
    Eq (α := (↑(𝔻 n) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (diskBoundaryInclusion n) :
            (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
          {
            down :=
              Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
            ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
        (↑(𝔻 n) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (diskBoundaryInclusion n) :
            (a : (↑(∂𝔻 n) : Type u_1)) → (↑(𝔻 n) : Type u_1))
          {
            down :=
              Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
                Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hy :
            ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } :
        (↑(𝔻 n) : Type u_1))),
  {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hx :
      ULift.{u_1, 0} (↑(Metric.sphere 0 1) : Type) } =
    {
      down :=
        Subtype.mk (p := fun (x : EuclideanSpace ℝ (Fin n)) ↦
          Membership.mem (γ := Set (EuclideanSpace ℝ (Fin n))) (Metric.sphere 0 1) x) x hy }
Tactic: obtain rfl : x = y := by simpa [diskBoundaryInclusion, disk] using h
Cleared hypotheses: y, hy, h