awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x : TopologicalSpace X.obj := ⊥
this :
  DiscreteTopology
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
f' : LocallyConstant
  (↑(c.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))
  (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
    Type (max u w)) :=
  {
    toFun :=
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))))
            (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
                (↑X.toTop : Type (max u w)))
              c.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑X.toTop : Type (max u w)))
            (toProfinite.obj X)),
    isLocallyConstant := ⋯ }
i : I
g :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max w u)))) :
      Type (max w u))
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
⊢ ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g
have refine : f =
  c.π.app i ≫
    toProfinite.map
      (InducedCategory.Hom.mk (F := ObjectProperty.FullSubcategory.obj)
        (↾(⇑g :
            (a : (↑((F ⋙ toProfinite).obj i).toTop : Type (max w u))) → (↑(toProfinite.obj X).toTop : Type (max u w)))))
Tactic: refine ⟨i, ⟨↾g⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
⊢ (functor.{u, w} c).Initial
have suffices : (e.inverse ⋙ functor.{u, w} c).Initial
Tactic: suffices (e.inverse ⋙ functor c).Initial from initial_of_equivalence_comp e.inverse (functor c)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
⊢ (e.inverse ⋙ functor.{u, w} c).Initial
have rw : (∀ (d : StructuredArrow c.pt toProfinite),
    ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)) ∧
  ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
    (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
    ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
      (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
Tactic: rw [initial_iff_of_isCofiltered (F := e.inverse ⋙ functor c)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
⊢ (∀ (d : StructuredArrow c.pt toProfinite),
      ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)) ∧
    ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
      (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
      ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
        (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
have left : ∀ (d : StructuredArrow c.pt toProfinite),
  ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left :
  ∀ (d : StructuredArrow c.pt toProfinite),
    ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)
⊢ (∀ (d : StructuredArrow c.pt toProfinite),
      ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)) ∧
    ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
      (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
      ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
        (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
have right : ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
  (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
  ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
    (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∃ (c_1 : ULiftHom (ULift.{w, u} I)),
    Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ { left := left, right := X, hom := f })
have left : ∀ (i : I) (g : F.obj i ⟶ X) (h : f = c.π.app i ≫ toProfinite.map g),
  ∃ (c_1 : ULiftHom (ULift.{w, u} I)),
    Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ { left := left, right := X, hom := f })
Tactic: obtain ⟨i, g, h⟩ := exists_hom c hc f
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∀ {c_1 : ULiftHom (ULift.{w, u} I)}
    (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ { left := left, right := X, hom := f }),
    ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
      (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
have right : ∀ (i : I)
  (s s' : (e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I } ⟶ { left := left, right := X, hom := f }),
  ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
    (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
Tactic: ⟨i⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
⊢ ∀ (s s' : (e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I } ⟶ { left := left, right := X, hom := f }),
    ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
      (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
have right : ∀
  (left_1 :
    ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
      Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f })
  (s : F.obj i ⟶ X) (w : f = c.π.app i ≫ toProfinite.map s)
  (s' : (e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I } ⟶ { left := left, right := X, hom := f }),
  ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
    (e.inverse ⋙ functor.{u, w} c).map t ≫
        { left := left_1, right := s, w := w :
          CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
            { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
      (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
Tactic: ⟨_, (s : F.obj i ⟶ X), (w : f = c.π.app i ≫ _)⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left_1 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
⊢ ∀ (s' : (e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I } ⟶ { left := left, right := X, hom := f }),
    ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
      (e.inverse ⋙ functor.{u, w} c).map t ≫
          { left := left_1, right := s, w := w :
            CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
              { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
        (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
have right : ∀
  (left_2 :
    ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
      Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f })
  (s' : F.obj i ⟶ X) (w' : f = c.π.app i ≫ toProfinite.map s'),
  ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
    (e.inverse ⋙ functor.{u, w} c).map t ≫
        { left := left_1, right := s, w := w :
          CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
            { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
      (e.inverse ⋙ functor.{u, w} c).map t ≫ { left := left_2, right := s', w := w' }
Tactic: ⟨_, (s' : F.obj i ⟶ X), (w' : f = c.π.app i ≫ _)⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left_1 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left_2 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
    (e.inverse ⋙ functor.{u, w} c).map t ≫
        { left := left_1, right := s, w := w :
          CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
            { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
      (e.inverse ⋙ functor.{u, w} c).map t ≫ { left := left_2, right := s', w := w' }
have right : ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
  StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map t) ≫
      StructuredArrow.Hom.right
        { left := left_1, right := s, w := w :
          CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
            { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
    StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map t) ≫
      StructuredArrow.Hom.right { left := left_2, right := s', w := w' }
Tactic: simp only [StructuredArrow.hom_eq_iff,
      StructuredArrow.comp_right]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left_1 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left_2 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ { down := i }),
    StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map t) ≫
        StructuredArrow.Hom.right
          { left := left_1, right := s, w := w :
            CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
              { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
      StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map t) ≫
        StructuredArrow.Hom.right { left := left_2, right := s', w := w' }
have right : StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map (𝟙 { down := i : ULift.{w, u} I })) ≫
    StructuredArrow.Hom.right
      { left := left_1, right := s, w := w :
        CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
          { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
  StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map (𝟙 { down := i : ULift.{w, u} I })) ≫
    StructuredArrow.Hom.right { left := left_2, right := s', w := w' }
Tactic: refine ⟨⟨i⟩, 𝟙 _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left_1 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left_2 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map (𝟙 { down := i : ULift.{w, u} I })) ≫
      StructuredArrow.Hom.right
        { left := left_1, right := s, w := w :
          CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
            { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
    StructuredArrow.Hom.right ((e.inverse ⋙ functor.{u, w} c).map (𝟙 { down := i : ULift.{w, u} I })) ≫
      StructuredArrow.Hom.right { left := left_2, right := s', w := w' }
have right : StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })) ≫
    StructuredArrow.Hom.right
      { left := left_1, right := s, w := w :
        CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
          { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
  StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })) ≫
    StructuredArrow.Hom.right { left := left_2, right := s', w := w' }
Tactic: simp only [CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (hypothesis)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left_1 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left_2 :
  ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I }).left ⟶
    Comma.left (T := Profinite) (L := fromPUnit c.pt) (R := toProfinite) { left := left, right := X, hom := f }
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })) ≫
      StructuredArrow.Hom.right
        { left := left_1, right := s, w := w :
          CommaMorphism ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })
            { left := left, right := X, hom := f : Comma (fromPUnit c.pt) toProfinite } } =
    StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor.{u, w} c).obj { down := i : ULift.{w, u} I })) ≫
      StructuredArrow.Hom.right { left := left_2, right := s', w := w' }
have w'₁ : c.π.app i ≫ toProfinite.map s = c.π.app i ≫ toProfinite.map s'
Tactic: rw [w] at w'
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (hypothesis)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
⊢ (functorOp.{u, w} c).Final
have this : (functor.{u, w} c).Initial
Tactic: have := functor_initial c hc
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (hypothesis)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
this : (functor.{u, w} c).Initial
⊢ (functorOp.{u, w} c).Final
have this₁ : IsEquivalence (C := (StructuredArrow c.pt toProfinite)ᵒᵖ) (StructuredArrow.toCostructuredArrow toProfinite c.pt)
Tactic: have : ((StructuredArrow.toCostructuredArrow toProfinite c.pt)).IsEquivalence :=
    (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (hypothesis)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst_2 : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u_2, v_1, u_2 + 1, u_1} Profiniteᵒᵖ C
S : Profinite
x x_1 : CostructuredArrow toProfinite.op (Opposite.op S)
f : x ⟶ x_1
⊢ Eq (α :=
    obj (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G) x ⟶
      obj.{u_2, v_1, u_2 + 1, u_1}
        (obj (const (CostructuredArrow toProfinite.op (Opposite.op S))) (G.obj (Opposite.op S))) x_1)
    (CategoryTheory.Functor.map (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G) f ≫
      G.map x_1.hom)
    (G.map x.hom ≫
      CategoryTheory.Functor.map
        (obj (const (CostructuredArrow toProfinite.op (Opposite.op S))) (G.obj (Opposite.op S))) f)
have this : toProfinite.op.map f.left ≫ x_1.hom = x.hom ≫ CategoryTheory.Functor.map (fromPUnit (Opposite.op S)) f.right
Tactic: have := f.w
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (hypothesis)
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst_2 : Category.{v_1, u_1} C
G : CategoryTheory.Functor.{u_2, v_1, u_2 + 1, u_1} Profiniteᵒᵖ C
S : Profinite
x x_1 : CostructuredArrow toProfinite.op (Opposite.op S)
f : x ⟶ x_1
this : toProfinite.op.map f.left ≫ x_1.hom = x.hom ≫ CategoryTheory.Functor.map (fromPUnit (Opposite.op S)) f.right
⊢ Eq (α :=
    obj (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G) x ⟶
      obj.{u_2, v_1, u_2 + 1, u_1}
        (obj (const (CostructuredArrow toProfinite.op (Opposite.op S))) (G.obj (Opposite.op S))) x_1)
    (CategoryTheory.Functor.map (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G) f ≫
      G.map x_1.hom)
    (G.map x.hom ≫
      CategoryTheory.Functor.map
        (obj (const (CostructuredArrow toProfinite.op (Opposite.op S))) (G.obj (Opposite.op S))) f)
have this₁ : (toProfinite.map f.left.unop).op ≫ x_1.hom = x.hom
Tactic: simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
        Category.comp_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
⊢ Continuous (Y := I → Bool) fun (c : I → Bool) (i : I) ↦ if J i then c i else false
have h : ∀ (i : I), Continuous (Y := Bool) fun (a : I → Bool) ↦ if J i then a i else false
Tactic: apply continuous_pi
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
i : I
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ if J i then a i else false
have h : J i → Continuous (Y := Bool) fun (a : I → Bool) ↦ a i
Tactic: split
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
i : I
h : J i → Continuous (Y := Bool) fun (a : I → Bool) ↦ a i
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ if J i then a i else false
have h₁ : ¬J i → Continuous (Y := Bool) fun (a : I → Bool) ↦ false
Tactic: split
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
⊢ Proj J x = x
have h₁ : ∀ (i : I), Proj J x i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ Proj J x i = x i
have h₁ : ¬J i → false = x i
Tactic: simp only [Proj, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ ¬J i → false = x i
have h₁ : false ≠ x i → J i
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
⊢ π C J = C
have h : ∀ (x : I → Bool), x ∈ π C J ↔ x ∈ C
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
⊢ x ∈ π C J ↔ x ∈ C
have h : x ∈ π C J → ∀ (y : I → Bool) (hy : y ∈ C) (h : Proj J y = x), x ∈ C
Tactic: refine ⟨fun ⟨y, hy, h⟩ ↦ ?_, fun h ↦ ⟨x, h, ?_⟩⟩