awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.map ι f).flip
⊢ LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
have intro : LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (hypothesis)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
have this : LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
  LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
Tactic: have :
    LocallyConstant.comap (C.π.app j0).hom.hom ggg =
      LocallyConstant.unflip (LocallyConstant.comap (C.π.app j0).hom.hom ggg).flip := by
    simp
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
this :
  LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
have intro : LocallyConstant.unflip (LocallyConstant.map ι f).flip =
  LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
have intro : (LocallyConstant.map ι f).flip = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
⊢ (LocallyConstant.map ι f).flip = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
have intro : ∀ (a : α), (LocallyConstant.map ι f).flip a = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
⊢ ff a = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
have intro : LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) =
  (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) =
    (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
have intro : ∀ (x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
  Eq (α := Fin 2)
    ((LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) :
          (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
        x :
      Fin 2)
    (((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a :
          (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
        x :
      Fin 2)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
have inhabit : ∀ (inhabited_h : Inhabited α),
  ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
have obtain : ∀ (j : J)
  (gg :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (α → Fin 2))
  (h :
    LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
      LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg),
  ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Tactic: obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
have refine : f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg)
Tactic: refine ⟨j, gg.map σ, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg)
have h₁ : ∀ (x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
  Eq.{u_1 + 1} (α := α) ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x : α)
    ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg) :
          (a : (↑C.pt.toTop : Type (max u v))) → α)
        x :
      α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Eq.{u_1 + 1} (α := α) ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x : α)
    ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg) :
          (a : (↑C.pt.toTop : Type (max u v))) → α)
        x :
      α)
have h₁ : (f : (a : (↑C.pt.toTop : Type (max u v))) → α) x =
  σ
    ((gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
      ((TopCat.Hom.hom (C.π.app j).hom : (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v))) x :
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))))
Tactic: simp only [Functor.const_obj_obj, LocallyConstant.coe_comap, LocallyConstant.map_apply,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
have inl : IsEmpty (Quotient S.toSetoid) →
  ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Tactic: cases isEmpty_or_nonempty S
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
inl :
  IsEmpty (Quotient S.toSetoid) →
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        α),
      f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
have inr : Nonempty (Quotient S.toSetoid) →
  ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Tactic: cases isEmpty_or_nonempty S
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
have refine : ∀ (j : J)
  (hj :
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
  ∃ (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Tactic: refine this.imp fun j hj => ?_