-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone X.diagram).pt
b : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hb :
  ∀
    (Q :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Q.proj b =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        Q
h :
  ∀
    (x :
      DiscreteQuotient (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    (↑((ConcreteCategory.hom (FC :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                    (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                  (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
                  X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
                (a :
                    (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                        (↑X.toTop : Type u))
                      X.asLimitCone.pt) →
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (limitCone X.diagram).pt)
              b) :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        x =
      (↑a :
          (j : DiscreteQuotient (↑X.toTop : Type u)) →
            (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        x
⊢ (↑((ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
              X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  X.asLimitCone.pt) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                (limitCone X.diagram).pt)
          b) :
      (j : DiscreteQuotient (↑X.toTop : Type u)) →
        (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) =
    (↑a :
      (j : DiscreteQuotient (↑X.toTop : Type u)) →
        (↑(((X.diagram ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))

Tactic:
apply funext

Premises used: funext