[GOAL]
X : Profinite
X✝ Y✝ Z✝ : DiscreteQuotient ↑X.toCompHaus.toTop
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
          map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
      (x✝¹ ≫ x✝) =
    { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
            map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
        x✝¹ ≫
      { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
            map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
X : Profinite
X✝ Y✝ Z✝ : DiscreteQuotient ↑X.toCompHaus.toTop
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ :
  ↑({ obj := fun S => FintypeCat.of (Quotient S.toSetoid),
          map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.obj
      X✝)
⊢ { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
          map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
      (x✝² ≫ x✝¹) x✝ =
    ({ obj := fun S => FintypeCat.of (Quotient S.toSetoid),
              map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
          x✝² ≫
        { obj := fun S => FintypeCat.of (Quotient S.toSetoid),
              map := fun {X_1 Y} f => DiscreteQuotient.ofLE (_ : X_1 ≤ Y) }.map
          x✝¹)
      x✝
[PROOFSTEP]
aesop_cat
[GOAL]
X : Profinite
⊢ Function.Bijective ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X))
[PROOFSTEP]
refine' ⟨fun a b h => _, fun a => _⟩
[GOAL]
case refine'_1
X : Profinite
a b : (forget Profinite).obj (asLimitCone X).pt
h :
  ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a =
    ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b
⊢ a = b
[PROOFSTEP]
refine' DiscreteQuotient.eq_of_forall_proj_eq fun S => _
[GOAL]
case refine'_1
X : Profinite
a b : (forget Profinite).obj (asLimitCone X).pt
h :
  ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a =
    ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b
S : DiscreteQuotient ((forget Profinite).obj (asLimitCone X).pt)
⊢ DiscreteQuotient.proj S a = DiscreteQuotient.proj S b
[PROOFSTEP]
apply_fun fun f : (limitCone X.diagram).pt => f.val S at h 
[GOAL]
case refine'_1
X : Profinite
a b : (forget Profinite).obj (asLimitCone X).pt
S : DiscreteQuotient ((forget Profinite).obj (asLimitCone X).pt)
h :
  ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a) S =
    ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) S
⊢ DiscreteQuotient.proj S a = DiscreteQuotient.proj S b
[PROOFSTEP]
exact h
[GOAL]
case refine'_2
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
⊢ ∃ a_1, ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a_1 = a
[PROOFSTEP]
obtain ⟨b, hb⟩ := DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)
[GOAL]
case refine'_2.intro
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ∃ a_1, ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) a_1 = a
[PROOFSTEP]
use b
[GOAL]
case h
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b = a
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case h.a
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) = ↑a
[PROOFSTEP]
apply funext
[GOAL]
case h.a.h
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
⊢ ∀ (x : DiscreteQuotient ↑X.toCompHaus.toTop),
    ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) x = ↑a x
[PROOFSTEP]
rintro S
[GOAL]
case h.a.h
X : Profinite
a : (forget Profinite).obj (limitCone (diagram X)).pt
b : ↑X.toCompHaus.toTop
hb : ∀ (Q : DiscreteQuotient ↑X.toCompHaus.toTop), DiscreteQuotient.proj Q b = ↑a Q
S : DiscreteQuotient ↑X.toCompHaus.toTop
⊢ ↑(↑(Limits.IsLimit.lift (limitConeIsLimit (diagram X)) (asLimitCone X)) b) S = ↑a S
[PROOFSTEP]
apply hb
