[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
have hB :=
  TopCat.isTopologicalBasis_cofiltered_limit.{u, u} (F ⋙ Profinite.toTopCat) (Profinite.toTopCat.mapCone C)
    (isLimitOfPreserves _ hC) (fun j => {W | IsClopen W}) ?_ (fun i => isClopen_univ)
    (fun i U1 U2 hU1 hU2 => hU1.inter hU2) ?_
[GOAL]
case refine_3
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
hB :
  TopologicalSpace.IsTopologicalBasis
    {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
case refine_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (j : J), TopologicalSpace.IsTopologicalBasis ((fun j => {W | IsClopen W}) j)
case refine_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (i j : J) (f : i ⟶ j) (V : Set ↑((F ⋙ toTopCat).obj j)),
    V ∈ (fun j => {W | IsClopen W}) j → ↑((F ⋙ toTopCat).map f) ⁻¹' V ∈ (fun j => {W | IsClopen W}) i
[PROOFSTEP]
rotate_left
[GOAL]
case refine_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (j : J), TopologicalSpace.IsTopologicalBasis ((fun j => {W | IsClopen W}) j)
[PROOFSTEP]
intro i
[GOAL]
case refine_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
i : J
⊢ TopologicalSpace.IsTopologicalBasis ((fun j => {W | IsClopen W}) i)
[PROOFSTEP]
change TopologicalSpace.IsTopologicalBasis {W : Set (F.obj i) | IsClopen W}
[GOAL]
case refine_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
i : J
⊢ TopologicalSpace.IsTopologicalBasis {W | IsClopen W}
[PROOFSTEP]
apply isTopologicalBasis_clopen
[GOAL]
case refine_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (i j : J) (f : i ⟶ j) (V : Set ↑((F ⋙ toTopCat).obj j)),
    V ∈ (fun j => {W | IsClopen W}) j → ↑((F ⋙ toTopCat).map f) ⁻¹' V ∈ (fun j => {W | IsClopen W}) i
[PROOFSTEP]
rintro i j f V (hV : IsClopen _)
[GOAL]
case refine_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set ↑((F ⋙ toTopCat).obj j)
hV : IsClopen V
⊢ ↑((F ⋙ toTopCat).map f) ⁻¹' V ∈ (fun j => {W | IsClopen W}) i
[PROOFSTEP]
exact
  ⟨hV.1.preimage ((F ⋙ toTopCat).map f).continuous, hV.2.preimage ((F ⋙ toTopCat).map f).continuous⟩
    -- Porting note: `<;> continuity` fails
      -- Using this, since `U` is open, we can write `U` as a union of clopen sets all of which
      -- are preimages of clopens from the factors in the limit.
[GOAL]
case refine_3
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
hB :
  TopologicalSpace.IsTopologicalBasis
    {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
obtain ⟨S, hS, h⟩ := hB.open_eq_sUnion hU.1
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
hB :
  TopologicalSpace.IsTopologicalBasis
    {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
clear hB
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
let j : S → J := fun s => (hS s.2).choose
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
let V : ∀ s : S, Set (F.obj (j s)) := fun s => (hS s.2).choose_spec.choose
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
have hV : ∀ s : S, IsClopen (V s) ∧ s.1 = C.π.app (j s) ⁻¹' V s := fun s => (hS s.2).choose_spec.choose_spec
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
have hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i)
[GOAL]
case hUo
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
⊢ ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
[PROOFSTEP]
intro s
[GOAL]
case hUo
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
s : ↑S
⊢ IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) s)
[PROOFSTEP]
exact (hV s).1.1.preimage (C.π.app (j s)).continuous
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
have hsU : U ⊆ ⋃ (i : ↑S), (fun s ↦ (forget Profinite).map (C.π.app (j s)) ⁻¹' V s) i
[GOAL]
case hsU
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
⊢ U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
[PROOFSTEP]
dsimp only
[GOAL]
case hsU
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
⊢ U ⊆
    ⋃ (i : ↑S),
      (forget Profinite).map
          (NatTrans.app C.π
            (Exists.choose
              (_ :
                ↑i ∈
                  {U |
                    ∃ j V,
                      V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
        Exists.choose
          (_ :
            ∃ V,
              V ∈ {W | IsClopen W} ∧
                ↑i =
                  ↑(NatTrans.app (toTopCat.mapCone C).π
                        (Exists.choose
                          (_ :
                            ↑i ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                    V)
[PROOFSTEP]
rw [h]
[GOAL]
case hsU
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
⊢ ⋃₀ S ⊆
    ⋃ (i : ↑S),
      (forget Profinite).map
          (NatTrans.app C.π
            (Exists.choose
              (_ :
                ↑i ∈
                  {U |
                    ∃ j V,
                      V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
        Exists.choose
          (_ :
            ∃ V,
              V ∈ {W | IsClopen W} ∧
                ↑i =
                  ↑(NatTrans.app (toTopCat.mapCone C).π
                        (Exists.choose
                          (_ :
                            ↑i ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                    V)
[PROOFSTEP]
rintro x ⟨T, hT, hx⟩
[GOAL]
case hsU.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
x : ↑C.pt.toCompHaus.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈
    ⋃ (i : ↑S),
      (forget Profinite).map
          (NatTrans.app C.π
            (Exists.choose
              (_ :
                ↑i ∈
                  {U |
                    ∃ j V,
                      V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
        Exists.choose
          (_ :
            ∃ V,
              V ∈ {W | IsClopen W} ∧
                ↑i =
                  ↑(NatTrans.app (toTopCat.mapCone C).π
                        (Exists.choose
                          (_ :
                            ↑i ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                    V)
[PROOFSTEP]
refine' ⟨_, ⟨⟨T, hT⟩, rfl⟩, _⟩
[GOAL]
case hsU.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
x : ↑C.pt.toCompHaus.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈
    (fun i =>
        (forget Profinite).map
            (NatTrans.app C.π
              (Exists.choose
                (_ :
                  ↑i ∈
                    {U |
                      ∃ j V,
                        V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
          Exists.choose
            (_ :
              ∃ V,
                V ∈ {W | IsClopen W} ∧
                  ↑i =
                    ↑(NatTrans.app (toTopCat.mapCone C).π
                          (Exists.choose
                            (_ :
                              ↑i ∈
                                {U |
                                  ∃ j V,
                                    V ∈ (fun j => {W | IsClopen W}) j ∧
                                      U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                      V))
      { val := T, property := hT }
[PROOFSTEP]
dsimp only [forget_map_eq_coe]
[GOAL]
case hsU.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
x : ↑C.pt.toCompHaus.toTop
T : Set ↑(toTopCat.mapCone C).pt
hT : T ∈ S
hx : x ∈ T
⊢ x ∈
    ↑(NatTrans.app C.π
          (Exists.choose
            (_ :
              T ∈
                {U |
                  ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
      Exists.choose
        (_ :
          ∃ V,
            V ∈ {W | IsClopen W} ∧
              T =
                ↑(NatTrans.app (toTopCat.mapCone C).π
                      (Exists.choose
                        (_ :
                          T ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                  V)
[PROOFSTEP]
rwa [← (hV ⟨T, hT⟩).2]
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
have := hU.2.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU
[GOAL]
case refine_3.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
this : ∃ t, U ⊆ ⋃ (i : ↑S) (_ : i ∈ t), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
obtain ⟨G, hG⟩ := this
[GOAL]
case refine_3.intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists (G.image j)
[GOAL]
case refine_3.intro.intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
let f : ∀ (s : S) (_ : s ∈ G), j0 ⟶ j s := fun s hs => (hj0 (Finset.mem_image.mpr ⟨s, hs, rfl⟩)).some
[GOAL]
case refine_3.intro.intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
let W : S → Set (F.obj j0) := fun s => if hs : s ∈ G then F.map (f s hs) ⁻¹' V s else Set.univ
[GOAL]
case refine_3.intro.intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
⊢ ∃ j V x, U = ↑(NatTrans.app C.π j) ⁻¹' V
[PROOFSTEP]
refine' ⟨j0, ⋃ (s : S) (_ : s ∈ G), W s, _, _⟩
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
⊢ IsClopen (⋃ (s : ↑S) (_ : s ∈ G), W s)
[PROOFSTEP]
apply isClopen_biUnion_finset
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_1.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
⊢ ∀ (i : ↑S), i ∈ G → IsClopen (W i)
[PROOFSTEP]
intro s hs
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_1.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
s : ↑S
hs : s ∈ G
⊢ IsClopen (W s)
[PROOFSTEP]
dsimp
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_1.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
s : ↑S
hs : s ∈ G
⊢ IsClopen
    (if hs : s ∈ G then
      ↑(F.map
            (Nonempty.some
              (_ :
                Nonempty
                  (j0 ⟶
                    Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))))) ⁻¹'
        Exists.choose
          (_ :
            ∃ V,
              IsClopen V ∧
                ↑s =
                  ↑(NatTrans.app C.π
                        (Exists.choose
                          (_ :
                            ↑s ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                    V)
    else Set.univ)
[PROOFSTEP]
rw [dif_pos hs]
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_1.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
s : ↑S
hs : s ∈ G
⊢ IsClopen
    (↑(F.map
          (Nonempty.some
            (_ :
              Nonempty
                (j0 ⟶
                  Exists.choose
                    (_ :
                      ↑s ∈
                        {U |
                          ∃ j V,
                            V ∈ (fun j => {W | IsClopen W}) j ∧
                              U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))))) ⁻¹'
      Exists.choose
        (_ :
          ∃ V,
            IsClopen V ∧
              ↑s =
                ↑(NatTrans.app C.π
                      (Exists.choose
                        (_ :
                          ↑s ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                  V))
[PROOFSTEP]
exact ⟨(hV s).1.1.preimage (F.map _).continuous, (hV s).1.2.preimage (F.map _).continuous⟩
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
⊢ U = ↑(NatTrans.app C.π j0) ⁻¹' ⋃ (s : ↑S) (_ : s ∈ G), W s
[PROOFSTEP]
ext x
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
⊢ x ∈ U ↔ x ∈ ↑(NatTrans.app C.π j0) ⁻¹' ⋃ (s : ↑S) (_ : s ∈ G), W s
[PROOFSTEP]
constructor
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mp
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
⊢ x ∈ U → x ∈ ↑(NatTrans.app C.π j0) ⁻¹' ⋃ (s : ↑S) (_ : s ∈ G), W s
[PROOFSTEP]
intro hx
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mp
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
hx : x ∈ U
⊢ x ∈ ↑(NatTrans.app C.π j0) ⁻¹' ⋃ (s : ↑S) (_ : s ∈ G), W s
[PROOFSTEP]
simp_rw [Set.preimage_iUnion, Set.mem_iUnion]
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mp
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
hx : x ∈ U
⊢ ∃ i i_1,
    x ∈
      ↑(NatTrans.app C.π j0) ⁻¹'
        if h : i ∈ G then
          ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j i)))) ⁻¹'
            Exists.choose
              (_ :
                ∃ V,
                  V ∈
                      (fun j => {W | IsClopen W})
                        (Exists.choose
                          (_ :
                            ↑i ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                    ↑i =
                      ↑(NatTrans.app (toTopCat.mapCone C).π
                            (Exists.choose
                              (_ :
                                ↑i ∈
                                  {U |
                                    ∃ j V,
                                      V ∈ (fun j => {W | IsClopen W}) j ∧
                                        U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                        V)
        else Set.univ
[PROOFSTEP]
obtain ⟨_, ⟨s, rfl⟩, _, ⟨hs, rfl⟩, hh⟩ := hG hx
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mp.intro.intro.intro.intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h => (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) s) hs
⊢ ∃ i i_1,
    x ∈
      ↑(NatTrans.app C.π j0) ⁻¹'
        if h : i ∈ G then
          ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j i)))) ⁻¹'
            Exists.choose
              (_ :
                ∃ V,
                  V ∈
                      (fun j => {W | IsClopen W})
                        (Exists.choose
                          (_ :
                            ↑i ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                    ↑i =
                      ↑(NatTrans.app (toTopCat.mapCone C).π
                            (Exists.choose
                              (_ :
                                ↑i ∈
                                  {U |
                                    ∃ j V,
                                      V ∈ (fun j => {W | IsClopen W}) j ∧
                                        U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                        V)
        else Set.univ
[PROOFSTEP]
refine' ⟨s, hs, _⟩
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mp.intro.intro.intro.intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h => (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) s) hs
⊢ x ∈
    ↑(NatTrans.app C.π j0) ⁻¹'
      if h : s ∈ G then
        ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j s)))) ⁻¹'
          Exists.choose
            (_ :
              ∃ V,
                V ∈
                    (fun j => {W | IsClopen W})
                      (Exists.choose
                        (_ :
                          ↑s ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                  ↑s =
                    ↑(NatTrans.app (toTopCat.mapCone C).π
                          (Exists.choose
                            (_ :
                              ↑s ∈
                                {U |
                                  ∃ j V,
                                    V ∈ (fun j => {W | IsClopen W}) j ∧
                                      U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                      V)
      else Set.univ
[PROOFSTEP]
rwa [dif_pos hs, ← Set.preimage_comp, ← Profinite.coe_comp, ← Functor.map_comp, C.w]
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
⊢ x ∈ ↑(NatTrans.app C.π j0) ⁻¹' ⋃ (s : ↑S) (_ : s ∈ G), W s → x ∈ U
[PROOFSTEP]
intro hx
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
hx : x ∈ ↑(NatTrans.app C.π j0) ⁻¹' ⋃ (s : ↑S) (_ : s ∈ G), W s
⊢ x ∈ U
[PROOFSTEP]
simp_rw [Set.preimage_iUnion, Set.mem_iUnion] at hx
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
hx :
  ∃ i i_1,
    x ∈
      ↑(NatTrans.app C.π j0) ⁻¹'
        if h : i ∈ G then
          ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j i)))) ⁻¹'
            Exists.choose
              (_ :
                ∃ V,
                  V ∈
                      (fun j => {W | IsClopen W})
                        (Exists.choose
                          (_ :
                            ↑i ∈
                              {U |
                                ∃ j V,
                                  V ∈ (fun j => {W | IsClopen W}) j ∧
                                    U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                    ↑i =
                      ↑(NatTrans.app (toTopCat.mapCone C).π
                            (Exists.choose
                              (_ :
                                ↑i ∈
                                  {U |
                                    ∃ j V,
                                      V ∈ (fun j => {W | IsClopen W}) j ∧
                                        U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                        V)
        else Set.univ
⊢ x ∈ U
[PROOFSTEP]
obtain ⟨s, hs, hx⟩ := hx
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ↑(NatTrans.app C.π j0) ⁻¹'
      if h : s ∈ G then
        ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j s)))) ⁻¹'
          Exists.choose
            (_ :
              ∃ V,
                V ∈
                    (fun j => {W | IsClopen W})
                      (Exists.choose
                        (_ :
                          ↑s ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                  ↑s =
                    ↑(NatTrans.app (toTopCat.mapCone C).π
                          (Exists.choose
                            (_ :
                              ↑s ∈
                                {U |
                                  ∃ j V,
                                    V ∈ (fun j => {W | IsClopen W}) j ∧
                                      U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                      V)
      else Set.univ
⊢ x ∈ U
[PROOFSTEP]
rw [h]
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ↑(NatTrans.app C.π j0) ⁻¹'
      if h : s ∈ G then
        ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j s)))) ⁻¹'
          Exists.choose
            (_ :
              ∃ V,
                V ∈
                    (fun j => {W | IsClopen W})
                      (Exists.choose
                        (_ :
                          ↑s ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                  ↑s =
                    ↑(NatTrans.app (toTopCat.mapCone C).π
                          (Exists.choose
                            (_ :
                              ↑s ∈
                                {U |
                                  ∃ j V,
                                    V ∈ (fun j => {W | IsClopen W}) j ∧
                                      U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                      V)
      else Set.univ
⊢ x ∈ ⋃₀ S
[PROOFSTEP]
refine' ⟨s.1, s.2, _⟩
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ↑(NatTrans.app C.π j0) ⁻¹'
      if h : s ∈ G then
        ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j s)))) ⁻¹'
          Exists.choose
            (_ :
              ∃ V,
                V ∈
                    (fun j => {W | IsClopen W})
                      (Exists.choose
                        (_ :
                          ↑s ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                  ↑s =
                    ↑(NatTrans.app (toTopCat.mapCone C).π
                          (Exists.choose
                            (_ :
                              ↑s ∈
                                {U |
                                  ∃ j V,
                                    V ∈ (fun j => {W | IsClopen W}) j ∧
                                      U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                      V)
      else Set.univ
⊢ x ∈ ↑s
[PROOFSTEP]
rw [(hV s).2]
[GOAL]
case refine_3.intro.intro.intro.intro.refine'_2.h.mpr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toCompHaus.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J :=
  fun s =>
    Exists.choose
      (_ : ↑s ∈ {U | ∃ j V, V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})
V : (s : ↑S) → Set ↑(F.obj (j s)).toCompHaus.toTop :=
  fun s =>
    Exists.choose
      (_ :
        ∃ V,
          V ∈
              (fun j => {W | IsClopen W})
                (Exists.choose
                  (_ :
                    ↑s ∈
                      {U |
                        ∃ j V,
                          V ∈ (fun j => {W | IsClopen W}) j ∧ U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
            ↑s =
              ↑(NatTrans.app (toTopCat.mapCone C).π
                    (Exists.choose
                      (_ :
                        ↑s ∈
                          {U |
                            ∃ j V,
                              V ∈ (fun j => {W | IsClopen W}) j ∧
                                U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                V)
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ↑(NatTrans.app C.π (j s)) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i)
hsU : U ⊆ ⋃ (i : ↑S), (fun s => (forget Profinite).map (NatTrans.app C.π (j s)) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ (i : ↑S) (_ : i ∈ G), (fun s => ↑(NatTrans.app C.π (j s)) ⁻¹' V s) i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs => Nonempty.some (_ : Nonempty (j0 ⟶ j s))
W : ↑S → Set ↑(F.obj j0).toCompHaus.toTop := fun s => if hs : s ∈ G then ↑(F.map (f s hs)) ⁻¹' V s else Set.univ
x : ↑C.pt.toCompHaus.toTop
s : ↑S
hs : s ∈ G
hx :
  x ∈
    ↑(NatTrans.app C.π j0) ⁻¹'
      if h : s ∈ G then
        ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j s)))) ⁻¹'
          Exists.choose
            (_ :
              ∃ V,
                V ∈
                    (fun j => {W | IsClopen W})
                      (Exists.choose
                        (_ :
                          ↑s ∈
                            {U |
                              ∃ j V,
                                V ∈ (fun j => {W | IsClopen W}) j ∧
                                  U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V})) ∧
                  ↑s =
                    ↑(NatTrans.app (toTopCat.mapCone C).π
                          (Exists.choose
                            (_ :
                              ↑s ∈
                                {U |
                                  ∃ j V,
                                    V ∈ (fun j => {W | IsClopen W}) j ∧
                                      U = ↑(NatTrans.app (toTopCat.mapCone C).π j) ⁻¹' V}))) ⁻¹'
                      V)
      else Set.univ
⊢ x ∈ ↑(NatTrans.app C.π (j s)) ⁻¹' V s
[PROOFSTEP]
rwa [dif_pos hs, ← Set.preimage_comp, ← Profinite.coe_comp, ← Functor.map_comp, C.w] at hx
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let U := f ⁻¹' {0}
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
obtain ⟨j, V, hV, h⟩ := exists_clopen_of_cofiltered C hC hU
[GOAL]
case intro.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
use j, LocallyConstant.ofClopen hV
[GOAL]
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
⊢ f = LocallyConstant.comap (↑(NatTrans.app C.π j)) (LocallyConstant.ofClopen hV)
[PROOFSTEP]
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
[GOAL]
case h.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(LocallyConstant.comap (↑(NatTrans.app C.π j)) (LocallyConstant.ofClopen hV)) ⁻¹' {0}
[PROOFSTEP]
rw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous]
[GOAL]
case h.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(LocallyConstant.ofClopen hV) ∘ ↑(NatTrans.app C.π j) ⁻¹' {0}
[PROOFSTEP]
conv_rhs => rw [Set.preimage_comp]
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
| ↑(LocallyConstant.ofClopen hV) ∘ ↑(NatTrans.app C.π j) ⁻¹' {0}
[PROOFSTEP]
rw [Set.preimage_comp]
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
| ↑(LocallyConstant.ofClopen hV) ∘ ↑(NatTrans.app C.π j) ⁻¹' {0}
[PROOFSTEP]
rw [Set.preimage_comp]
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
| ↑(LocallyConstant.ofClopen hV) ∘ ↑(NatTrans.app C.π j) ⁻¹' {0}
[PROOFSTEP]
rw [Set.preimage_comp]
[GOAL]
case h.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2)
U : Set ↑C.pt.toCompHaus.toTop := ↑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toCompHaus.toTop
hV : IsClopen V
h : U = ↑(NatTrans.app C.π j) ⁻¹' V
⊢ ↑f ⁻¹' {0} = ↑(NatTrans.app C.π j) ⁻¹' (↑(LocallyConstant.ofClopen hV) ⁻¹' {0})
[PROOFSTEP]
rw [LocallyConstant.ofClopen_fiber_zero hV, ← h]
[GOAL]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
[GOAL]
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let ff := (f.map ι).flip
[GOAL]
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
have hff := fun a : α => exists_locallyConstant_fin_two _ hC (ff a)
[GOAL]
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
hff : ∀ (a : α), ∃ j g, ff a = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
choose j g h using hff
[GOAL]
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let G : Finset J := Finset.univ.image j
[GOAL]
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists G
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
have hj : ∀ a, j a ∈ (Finset.univ.image j : Finset J) :=
  by
  intro a
  simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]
[GOAL]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
⊢ ∀ (a : α), j a ∈ Finset.image j Finset.univ
[PROOFSTEP]
intro a
[GOAL]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
a : α
⊢ j a ∈ Finset.image j Finset.univ
[PROOFSTEP]
simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let fs : ∀ a : α, j0 ⟶ j a := fun a => (hj0 (hj a)).some
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let gg : α → LocallyConstant (F.obj j0) (Fin 2) := fun a => (g a).comap (F.map (fs _))
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let ggg := LocallyConstant.unflip gg
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
refine' ⟨j0, ggg, _⟩
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg
[PROOFSTEP]
have : f.map ι = LocallyConstant.unflip (f.map ι).flip := by simp
[GOAL]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
[PROOFSTEP]
simp
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
⊢ LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg
[PROOFSTEP]
rw [this]
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg
[PROOFSTEP]
clear this
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg
[PROOFSTEP]
have : LocallyConstant.comap (C.π.app j0) ggg = LocallyConstant.unflip (LocallyConstant.comap (C.π.app j0) ggg).flip :=
  by simp
[GOAL]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg))
[PROOFSTEP]
simp
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg
[PROOFSTEP]
rw [this]
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg))
[PROOFSTEP]
clear this
[GOAL]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg))
[PROOFSTEP]
congr 1
[GOAL]
case intro.intro.e_f
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.flip (LocallyConstant.map ι f) =
    LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg)
[PROOFSTEP]
ext1 a
[GOAL]
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.flip (LocallyConstant.map ι f) a =
    LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg) a
[PROOFSTEP]
change ff a = _
[GOAL]
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ ff a = LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg) a
[PROOFSTEP]
rw [h]
[GOAL]
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a) =
    LocallyConstant.flip (LocallyConstant.comap (↑(NatTrans.app C.π j0)) ggg) a
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a) =
    LocallyConstant.flip
      (LocallyConstant.comap (↑(NatTrans.app C.π j0))
        (LocallyConstant.unflip fun a =>
          LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
      a
[PROOFSTEP]
ext1 x
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)) x =
    ↑(LocallyConstant.flip
          (LocallyConstant.comap (↑(NatTrans.app C.π j0))
            (LocallyConstant.unflip fun a =>
              LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
          a)
      x
[PROOFSTEP]
rw [LocallyConstant.coe_comap _ _ (C.π.app (j a)).continuous]
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (↑(g a) ∘ ↑(NatTrans.app C.π (j a))) x =
    ↑(LocallyConstant.flip
          (LocallyConstant.comap (↑(NatTrans.app C.π j0))
            (LocallyConstant.unflip fun a =>
              LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
          a)
      x
[PROOFSTEP]
dsimp [LocallyConstant.flip, LocallyConstant.unflip]
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) (↑(NatTrans.app C.π (j a)) x) =
    ↑(LocallyConstant.comap ↑(NatTrans.app C.π j0)
          { toFun := fun x a => ↑(LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)) x,
            isLocallyConstant :=
              (_ :
                IsLocallyConstant fun x a =>
                  ↑(LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)) x) })
      x a
[PROOFSTEP]
rw [LocallyConstant.coe_comap _ _ (C.π.app j0).continuous]
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) (↑(NatTrans.app C.π (j a)) x) =
    (↑{ toFun := fun x a => ↑(LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)) x,
            isLocallyConstant :=
              (_ :
                IsLocallyConstant fun x a =>
                  ↑(LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)) x) } ∘
        ↑(NatTrans.app C.π j0))
      x a
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) (↑(NatTrans.app C.π (j a)) x) =
    ↑(LocallyConstant.comap (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)) (↑(NatTrans.app C.π j0) x)
[PROOFSTEP]
rw [LocallyConstant.coe_comap _ _ _]
  -- Porting note: `repeat' rw [LocallyConstant.coe_comap]` didn't work
    -- so I did all three rewrites manually
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) (↑(NatTrans.app C.π (j a)) x) =
    (↑(g a) ∘ ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (↑(NatTrans.app C.π j0) x)
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) (↑(NatTrans.app C.π (j a)) x) =
    ↑(g a) (↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))) (↑(NatTrans.app C.π j0) x))
[PROOFSTEP]
congr! 1
[GOAL]
case intro.intro.e_f.h.h.h.e'_6.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
e_2✝ : ↑(F.obj (j a)).toCompHaus.toTop = (forget Profinite).obj (F.obj (j a))
⊢ ↑(NatTrans.app C.π (j a)) x = ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))) (↑(NatTrans.app C.π j0) x)
[PROOFSTEP]
change _ = (C.π.app j0 ≫ F.map (fs a)) x
[GOAL]
case intro.intro.e_f.h.h.h.e'_6.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
e_2✝ : ↑(F.obj (j a)).toCompHaus.toTop = (forget Profinite).obj (F.obj (j a))
⊢ ↑(NatTrans.app C.π (j a)) x = ↑(NatTrans.app C.π j0 ≫ F.map (fs a)) x
[PROOFSTEP]
rw [C.w]
[GOAL]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (↑(NatTrans.app C.π (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap (↑(F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ Continuous ↑(F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))
[PROOFSTEP]
exact (F.map _).continuous
[GOAL]
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
inhabit α
[GOAL]
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f
[GOAL]
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
[GOAL]
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default
[GOAL]
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
refine' ⟨j, gg.map σ, _⟩
[GOAL]
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
⊢ f = LocallyConstant.comap (↑(NatTrans.app C.π j)) (LocallyConstant.map σ gg)
[PROOFSTEP]
ext x
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = ↑(LocallyConstant.comap (↑(NatTrans.app C.π j)) (LocallyConstant.map σ gg)) x
[PROOFSTEP]
rw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous]
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = (↑(LocallyConstant.map σ gg) ∘ ↑(NatTrans.app C.π j)) x
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg (↑(NatTrans.app C.π j) x) then Exists.choose h else default
[PROOFSTEP]
have h1 : ι (f x) = gg (C.π.app j x) :=
  by
  change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
  rw [h, LocallyConstant.coe_comap _ _ (C.π.app j).continuous]
  rfl
[GOAL]
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
[PROOFSTEP]
change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
[GOAL]
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑(LocallyConstant.map (fun a b => if a = b then 0 else 1) f) x = ↑gg (↑(NatTrans.app C.π j) x)
[PROOFSTEP]
rw [h, LocallyConstant.coe_comap _ _ (C.π.app j).continuous]
[GOAL]
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ (↑gg ∘ ↑(NatTrans.app C.π j)) x = ↑gg (↑(NatTrans.app C.π j) x)
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
⊢ ↑f x = if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg (↑(NatTrans.app C.π j) x) then Exists.choose h else default
[PROOFSTEP]
have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
⊢ ↑f x = if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg (↑(NatTrans.app C.π j) x) then Exists.choose h else default
[PROOFSTEP]
rw [dif_pos h2]
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
⊢ ↑f x = Exists.choose h2
[PROOFSTEP]
apply_fun ι
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
⊢ ι (↑f x) = ι (Exists.choose h2)
[PROOFSTEP]
rw [h2.choose_spec]
[GOAL]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
⊢ ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
[PROOFSTEP]
exact h1
[GOAL]
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
⊢ Function.Injective ι
[PROOFSTEP]
intro a b hh
[GOAL]
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
a b : α
hh : ι a = ι b
⊢ a = b
[PROOFSTEP]
have hhh := congr_fun hh a
[GOAL]
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
a b : α
hh : ι a = ι b
hhh : ι a a = ι b a
⊢ a = b
[PROOFSTEP]
dsimp at hhh
[GOAL]
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
a b : α
hh : ι a = ι b
hhh : (if a = a then 0 else 1) = if b = a then 0 else 1
⊢ a = b
[PROOFSTEP]
rw [if_pos rfl] at hhh
[GOAL]
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
a b : α
hh : ι a = ι b
hhh : 0 = if b = a then 0 else 1
⊢ a = b
[PROOFSTEP]
split_ifs at hhh  with hh1
[GOAL]
case pos
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
a b : α
hh : ι a = ι b
hh1 : b = a
hhh : 0 = 0
⊢ a = b
[PROOFSTEP]
exact hh1.symm
[GOAL]
case neg
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (↑(NatTrans.app C.π j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg (↑(NatTrans.app C.π j) x)
h2 : ∃ a, ι a = ↑gg (↑(NatTrans.app C.π j) x)
a b : α
hh : ι a = ι b
hh1 : ¬b = a
hhh : 0 = 1
⊢ a = b
[PROOFSTEP]
exact False.elim (bot_ne_top hhh)
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let S := f.discreteQuotient
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let ff : S → α := f.lift
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
cases isEmpty_or_nonempty S
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
suffices ∃ j, IsEmpty (F.obj j) by
  refine' this.imp fun j hj => _
  refine' ⟨⟨hj.elim, fun A => _⟩, _⟩
  · suffices : (fun a ↦ IsEmpty.elim hj a) ⁻¹' A = ∅
    · rw [this]
      exact isOpen_empty
    exact @Set.eq_empty_of_isEmpty _ hj _
  · ext x
    exact hj.elim' (C.π.app j x)
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
refine' this.imp fun j hj => _
[GOAL]
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ ∃ g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
refine' ⟨⟨hj.elim, fun A => _⟩, _⟩
[GOAL]
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
⊢ IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)
[PROOFSTEP]
suffices : (fun a ↦ IsEmpty.elim hj a) ⁻¹' A = ∅
[GOAL]
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
this : (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
⊢ IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
this : (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
⊢ IsOpen ∅
[PROOFSTEP]
exact isOpen_empty
[GOAL]
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
⊢ (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
[PROOFSTEP]
exact @Set.eq_empty_of_isEmpty _ hj _
[GOAL]
case refine'_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ f =
    LocallyConstant.comap ↑(NatTrans.app C.π j)
      { toFun := fun a => IsEmpty.elim hj a,
        isLocallyConstant := (_ : ∀ (A : Set α), IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)) }
[PROOFSTEP]
ext x
[GOAL]
case refine'_2.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x =
    ↑(LocallyConstant.comap ↑(NatTrans.app C.π j)
          { toFun := fun a => IsEmpty.elim hj a,
            isLocallyConstant := (_ : ∀ (A : Set α), IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)) })
      x
[PROOFSTEP]
exact hj.elim' (C.π.app j x)
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
[PROOFSTEP]
simp only [← not_nonempty_iff, ← not_forall]
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ¬∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
[PROOFSTEP]
intro h
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
⊢ False
[PROOFSTEP]
haveI : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
⊢ False
[PROOFSTEP]
haveI : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j => (inferInstance : T2Space (F.obj j))
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
⊢ False
[PROOFSTEP]
haveI : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j => (inferInstance : CompactSpace (F.obj j))
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
⊢ False
[PROOFSTEP]
have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} (F ⋙ Profinite.toTopCat)
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
⊢ False
[PROOFSTEP]
suffices : Nonempty C.pt
[GOAL]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝² : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝¹ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
this : Nonempty ↑C.pt.toCompHaus.toTop
⊢ False
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
⊢ Nonempty ↑C.pt.toCompHaus.toTop
[PROOFSTEP]
exact IsEmpty.false (S.proj this.some)
[GOAL]
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
⊢ Nonempty ↑C.pt.toCompHaus.toTop
[PROOFSTEP]
let D := Profinite.toTopCat.mapCone C
[GOAL]
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
⊢ Nonempty ↑C.pt.toCompHaus.toTop
[PROOFSTEP]
have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
[GOAL]
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
hD : IsLimit D
⊢ Nonempty ↑C.pt.toCompHaus.toTop
[PROOFSTEP]
have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{u, u} _)).inv
[GOAL]
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
hD : IsLimit D
CD : (TopCat.limitCone (F ⋙ toTopCat)).pt ⟶ D.pt
⊢ Nonempty ↑C.pt.toCompHaus.toTop
[PROOFSTEP]
exact cond.map CD
[GOAL]
case inr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
let f' : LocallyConstant C.pt S := ⟨S.proj, S.proj_isLocallyConstant⟩
[GOAL]
case inr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'
[GOAL]
case inr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (↑(NatTrans.app C.π j)) g'
⊢ ∃ j g, f = LocallyConstant.comap (↑(NatTrans.app C.π j)) g
[PROOFSTEP]
refine' ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, _⟩
[GOAL]
case inr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (↑(NatTrans.app C.π j)) g'
⊢ f =
    LocallyConstant.comap ↑(NatTrans.app C.π j)
      { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) }
[PROOFSTEP]
ext1 t
[GOAL]
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (↑(NatTrans.app C.π j)) g'
t : ↑C.pt.toCompHaus.toTop
⊢ ↑f t =
    ↑(LocallyConstant.comap ↑(NatTrans.app C.π j)
          { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) })
      t
[PROOFSTEP]
apply_fun fun e => e t at hj
[GOAL]
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : ↑f' t = ↑(LocallyConstant.comap (↑(NatTrans.app C.π j)) g') t
⊢ ↑f t =
    ↑(LocallyConstant.comap ↑(NatTrans.app C.π j)
          { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) })
      t
[PROOFSTEP]
rw [LocallyConstant.coe_comap _ _ (C.π.app j).continuous] at hj ⊢
[GOAL]
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : ↑f' t = (↑g' ∘ ↑(NatTrans.app C.π j)) t
⊢ ↑f t =
    (↑{ toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) } ∘ ↑(NatTrans.app C.π j)) t
[PROOFSTEP]
dsimp at hj ⊢
[GOAL]
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t = ↑g' (↑(NatTrans.app C.π j) t)
⊢ ↑f t = ↑(LocallyConstant.lift f) (↑g' (↑(NatTrans.app C.π j) t))
[PROOFSTEP]
rw [← hj]
[GOAL]
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t = ↑g' (↑(NatTrans.app C.π j) t)
⊢ ↑f t = ↑(LocallyConstant.lift f) (DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t)
[PROOFSTEP]
rfl