awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Extend
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_1 : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
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_1, right := X, hom := f })
⊢ ∃ (c_1 : ULiftHom (ULift.{w, u} I)),
    Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ { left := left_1, right := X, hom := f })

Tactic:
obtain ⟨i, g, h⟩ := exists_hom c hc f

Premises used: Profinite.exists_hom
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
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:
⟨⟨i⟩, ⟨StructuredArrow.homMk g h.symm⟩⟩

Premises used: CategoryTheory.StructuredArrow.homMk, Nonempty.intro, Exists.intro, ULift.up, Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
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:
exact ⟨⟨i⟩, ⟨StructuredArrow.homMk g h.symm⟩⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
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'
⊢ ∀ {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'

Tactic:
⟨i⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
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'
⊢ ∀ (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:
⟨_, (s : F.obj i ⟶ X), (w : f = c.π.app i ≫ _)⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
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' }
⊢ ∀ (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 ≫ _)⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
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'
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' }
⊢ ∃ (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:
simp only [StructuredArrow.hom_eq_iff,
      StructuredArrow.comp_right]

Premises used: CategoryTheory.StructuredArrow.hom_eq_iff, CategoryTheory.StructuredArrow.comp_right
-- Module: Mathlib.Topology.Category.Profinite.Extend
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' }

Tactic:
⟨⟨i⟩, 𝟙 _, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, Exists.intro, ULift.up
-- Module: Mathlib.Topology.Category.Profinite.Extend
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'
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' }
⊢ ∃ (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:
refine ⟨⟨i⟩, 𝟙 _, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
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'
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' }
⊢ 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:
simp only [CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.Topology.Category.Profinite.Extend
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.π.app i ≫ toProfinite.map s = c.π.app i ≫ toProfinite.map s'

Tactic:
rw [w] at w'
-- Module: Mathlib.Topology.Category.Profinite.Extend
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'_1 : f = c.π.app i ≫ toProfinite.map s'
w' : c.π.app i ≫ toProfinite.map s = 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'_1 }

Tactic:
toProfinite.map_injective <| Epi.left_cancellation _ _ w'

Premises used: CategoryTheory.Epi.left_cancellation, FintypeCat.toProfinite, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Topology.Category.Profinite.Extend
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'_1 : f = c.π.app i ≫ toProfinite.map s'
w' : c.π.app i ≫ toProfinite.map s = 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'_1 }

Tactic:
exact toProfinite.map_injective <| Epi.left_cancellation _ _ w'

Premises used: CategoryTheory.Epi.left_cancellation, FintypeCat.toProfinite, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Topology.Category.Profinite.Extend
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)
⊢ (functor.{u, w} c).Initial

Tactic:
have := functor_initial c hc
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
⊢ IsEquivalence (C := (StructuredArrow c.pt toProfinite)ᵒᵖ) (StructuredArrow.toCostructuredArrow toProfinite c.pt)

Tactic:
have : ((StructuredArrow.toCostructuredArrow toProfinite c.pt)).IsEquivalence :=
    (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
-- Module: Mathlib.Topology.Category.Profinite.Extend
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_1 : (functor.{u, w} c).Initial
this : IsEquivalence (C := (StructuredArrow c.pt toProfinite)ᵒᵖ) (StructuredArrow.toCostructuredArrow toProfinite c.pt)
⊢ (functorOp.{u, w} c).Final

Tactic:
Functor.final_comp (functor c).op _

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_comp, Profinite.Extend.functorOp, Profinite.Extend.functor
-- Module: Mathlib.Topology.Category.Profinite.Extend
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_1 : (functor.{u, w} c).Initial
this : IsEquivalence (C := (StructuredArrow c.pt toProfinite)ᵒᵖ) (StructuredArrow.toCostructuredArrow toProfinite c.pt)
⊢ (functorOp.{u, w} c).Final

Tactic:
exact Functor.final_comp (functor c).op _

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_comp, Profinite.Extend.functor
-- Module: Mathlib.Topology.Category.Profinite.Extend
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 : StructuredArrow S toProfinite
f : x ⟶ x_1
⊢ CategoryTheory.Functor.map (obj (const (StructuredArrow S toProfinite)) (G.obj S)) f ≫ G.map x_1.hom =
    G.map x.hom ≫ (StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G).map f

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Category.Profinite.Extend
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 : Profinite ⥤ C
⊢ G.mapCone c = Cone.whisker (functor.{u, w} c) (cone G c.pt)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.StructuredArrow.mk, CategoryTheory.Limits.Cone.whisker, CategoryTheory.Functor.mapCone, rfl, Profinite.Extend.functor
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
⊢ toProfinite.op.map f.left ≫ x_1.hom = x.hom ≫ CategoryTheory.Functor.map (fromPUnit (Opposite.op S)) f.right

Tactic:
have := f.w
-- Module: Mathlib.Topology.Category.Profinite.Extend
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
⊢ (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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CostructuredArrow.right_eq_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map
-- Module: Mathlib.Topology.Category.Profinite.Extend
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.map f.left.unop).op ≫ x_1.hom = x.hom
⊢ 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)

Tactic:
simp [← map_comp, this]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Category.Profinite.Extend
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 : Profiniteᵒᵖ ⥤ C
⊢ G.mapCocone c.op = Cocone.whisker (functorOp.{u, w} c) (cocone G c.pt)

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.CostructuredArrow.mk, Profinite.Extend.functorOp, rfl