-- Module: Mathlib.Topology.Category.TopCat.Sphere
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))
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 }
⊢ {
      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 }

Tactic:
obtain rfl : x = y := by simpa [diskBoundaryInclusion, disk] using h

Premises used: rfl