awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
this_1 : IsFiltered.{w, u} P.FullSubcategory
G : Functor.{w, w, w, u} (FinalModel C₀) P.FullSubcategory :=
  { obj := fun (X : FinalModel C₀) ↦ ObjectProperty.FullSubcategory.mk (P := P) (Functor.obj (fromFinalModel C₀) X) ⋯,
    map := fun {X Y : FinalModel C₀} (f : X ⟶ Y) ↦ ObjectProperty.homMk (P := P) (Functor.map (fromFinalModel C₀) f),
    map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
Y : FinalModel C₀
⊢ ∃ (a : FinalModel C₀), G.obj a = ObjectProperty.FullSubcategory.mk (P := P) (Functor.obj (fromFinalModel C₀) Y) ⋯

Tactic:
⟨Y, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
this_1 : IsFiltered.{w, u} P.FullSubcategory
G : Functor.{w, w, w, u} (FinalModel C₀) P.FullSubcategory :=
  { obj := fun (X : FinalModel C₀) ↦ ObjectProperty.FullSubcategory.mk (P := P) (Functor.obj (fromFinalModel C₀) X) ⋯,
    map := fun {X Y : FinalModel C₀} (f : X ⟶ Y) ↦ ObjectProperty.homMk (P := P) (Functor.map (fromFinalModel C₀) f),
    map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
Y : FinalModel C₀
⊢ ∃ (a : FinalModel C₀), G.obj a = ObjectProperty.FullSubcategory.mk (P := P) (Functor.obj (fromFinalModel C₀) Y) ⋯

Tactic:
exact ⟨Y, rfl⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
this_1 : IsFiltered.{w, u} P.FullSubcategory
G : Functor.{w, w, w, u} (FinalModel C₀) P.FullSubcategory :=
  { obj := fun (X : FinalModel C₀) ↦ ObjectProperty.FullSubcategory.mk (P := P) (Functor.obj (fromFinalModel C₀) X) ⋯,
    map := fun {X Y : FinalModel C₀} (f : X ⟶ Y) ↦ ObjectProperty.homMk (P := P) (Functor.map (fromFinalModel C₀) f),
    map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
⊢ ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F : Functor.{w, w, u, u} D C₀),
    F.Final

Tactic:
exact ⟨P.FullSubcategory, small_of_surjective (f := G.obj)
      (by rintro ⟨_, Y, _, rfl⟩; exact ⟨Y, rfl⟩), inferInstance, inferInstance, P.ι,
      Functor.final_of_comp_full_faithful' G P.ι ⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
⊢ ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final

Tactic:
have (C₀ : Type u) [Category.{w} C₀] [IsFiltered C₀] [FinallySmall.{w} C₀] :
      ∃ (D : Type u) (_ : Small.{w} D) (_ : Category.{w} D) (_ : IsFiltered D) (F : D ⥤ C₀),
        F.Final := by
    /- For `D`, we can choose the full subcategory of `C₀` which is the strict image
    of the final functor `fromFinalModel.{w} C₀ : FinalModel.{w} C₀ ⥤ C₀`,
    where `FinalModel.{w} C₀` is a `w`-small category. -/
    let P : ObjectProperty C₀ := ObjectProperty.strictMap ⊤ (fromFinalModel.{w} C₀)
    have hP (X : C₀) : ∃ (Y : C₀) (hY : P Y), Nonempty (X ⟶ Y) := by
      let f : StructuredArrow X (fromFinalModel.{w} C₀) := Classical.arbitrary _
      exact ⟨_, ObjectProperty.strictMap_obj _ _ (X := f.right) (by tauto), ⟨f.hom⟩⟩
    have : IsFiltered P.FullSubcategory :=
      { nonempty := by
          obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)
          exact ⟨X, hX⟩
        cocone_objs := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩
          obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (leftToMax X Y ≫ f),
            ObjectProperty.homMk (rightToMax X Y ≫ f), by tauto⟩
        cocone_maps := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩ ⟨f₁ : X ⟶ Y⟩ ⟨f₂ : X ⟶ Y⟩
          obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩ }
    let G : FinalModel.{w} C₀ ⥤ P.FullSubcategory :=
      { obj X := ⟨(fromFinalModel.{w} C₀).obj X, by tauto⟩
        map f := ObjectProperty.homMk ((fromFinalModel.{w} C₀).map f) }
    have : (G ⋙ P.ι).Final := inferInstanceAs (fromFinalModel.{w} C₀).Final
    exact ⟨P.FullSubcategory, small_of_surjective (f := G.obj)
      (by rintro ⟨_, Y, _, rfl⟩; exact ⟨Y, rfl⟩), inferInstance, inferInstance, P.ι,
      Functor.final_of_comp_full_faithful' G P.ι ⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
C₀ : Type u
inst_4 : Category.{w, u} C₀
h : IsFiltered.{w, u} C₀
h_1 : FinallySmall.{w, w, u} C₀
obtain :
  ∀ (D : Type u),
    Small.{w, u} D →
      ∀ (w : Category.{w, u} D),
        IsFiltered.{w, u} D →
          ∀ (F : Functor.{w, w, u, u} D C₀),
            F.Final → ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final

Tactic:
obtain ⟨D, _, _, _, F, _⟩ := this C₀
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
C₀ : Type u
inst_4 : Category.{w, u} C₀
h : IsFiltered.{w, u} C₀
h_1 : FinallySmall.{w, w, u} C₀
D : Type u
w : Small.{w, u} D
w_1 : Category.{w, u} D
w_2 : IsFiltered.{w, u} D
F : Functor.{w, w, u, u} D C₀
h_2 : F.Final
e : Equivalence.{w, w, u, w} D (SmallModel.{w, w, u} D) := equivSmallModel D
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final

Tactic:
⟨_, _, of_equivalence e, e.inverse ⋙ F, inferInstance⟩

Premises used: CategoryTheory.Functor.comp, inferInstance, CategoryTheory.IsFiltered.of_equivalence, Exists.intro, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
C₀ : Type u
inst_4 : Category.{w, u} C₀
h : IsFiltered.{w, u} C₀
h_1 : FinallySmall.{w, w, u} C₀
D : Type u
w : Small.{w, u} D
w_1 : Category.{w, u} D
w_2 : IsFiltered.{w, u} D
F : Functor.{w, w, u, u} D C₀
h_2 : F.Final
e : Equivalence.{w, w, u, w} D (SmallModel.{w, w, u} D) := equivSmallModel D
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final

Tactic:
exact ⟨_, _, of_equivalence e, e.inverse ⋙ F, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
⊢ ∀ (C₀ : Type u) [inst : Category.{w, u} C₀],
    IsFiltered.{w, u} C₀ →
      FinallySmall.{w, w, u} C₀ → ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final

Tactic:
have (C₀ : Type u) [Category.{w} C₀] (_ : IsFiltered C₀) (_ : FinallySmall.{w} C₀) :
      ∃ (D : Type w) (_ : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final := by
    obtain ⟨D, _, _, _, F, _⟩ := this C₀
    let e := equivSmallModel.{w} D
    exact ⟨_, _, of_equivalence e, e.inverse ⋙ F, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this_1 :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀],
    IsFiltered.{w, u} C₀ →
      FinallySmall.{w, w, u} C₀ → ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
obtain :
  ∀ (D : Type w) (w : SmallCategory D),
    IsFiltered D →
      ∀ (F : Functor.{w, w, w, u} D (ShrinkHoms.{u} C)),
        F.Final → ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : Functor.{w, v, w, u} D C), F.Final
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : Functor.{w, v, w, u} D C), F.Final

Tactic:
obtain ⟨D, _, _, F, _⟩ := this (ShrinkHoms C)
    (of_equivalence e) (finallySmall_of_final_of_finallySmall e.functor)

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.finallySmall_of_final_of_finallySmall, CategoryTheory.IsFiltered.of_equivalence, CategoryTheory.ShrinkHoms
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this_1 :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀],
    IsFiltered.{w, u} C₀ →
      FinallySmall.{w, w, u} C₀ → ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
D : Type w
w : SmallCategory D
w_1 : IsFiltered D
F : Functor.{w, w, w, u} D (ShrinkHoms.{u} C)
h : F.Final
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : Functor.{w, v, w, u} D C), F.Final

Tactic:
⟨D, inferInstance, inferInstance, F ⋙ e.inverse, inferInstance⟩

Premises used: CategoryTheory.Functor.comp, inferInstance, Exists.intro, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
this_1 :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered.{w, u} C₀] [FinallySmall.{w, w, u} C₀],
    ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F :
      Functor.{w, w, u, u} D C₀), F.Final
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀],
    IsFiltered.{w, u} C₀ →
      FinallySmall.{w, w, u} C₀ → ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : D ⥤ C₀), F.Final
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
D : Type w
w : SmallCategory D
w_1 : IsFiltered D
F : Functor.{w, w, w, u} D (ShrinkHoms.{u} C)
h : F.Final
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsFiltered D) (F : Functor.{w, v, w, u} D C), F.Final

Tactic:
exact ⟨D, inferInstance, inferInstance, F ⋙ e.inverse, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
⊢ IsFiltered.{w, w} (FilteredFinalModel.{w, v, u} C)

Tactic:
(exists_of_isFiltered.{w} C).choose_spec.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.FinallySmall.exists_of_isFiltered, CategoryTheory.FinallySmall.FilteredFinalModel, Exists.choose
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
⊢ Functor.Final.{w, v, w, u} (C := FilteredFinalModel.{w, v, u} C) (fromFilteredFinalModel C)

Tactic:
(exists_of_isFiltered.{w} C).choose_spec.choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.FinallySmall.exists_of_isFiltered, CategoryTheory.FinallySmall.FilteredFinalModel, CategoryTheory.FinallySmall.fromFilteredFinalModel
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
D : Type u_1
E : Type u_2
inst_4 : Category.{v_1, u_1} D
inst_5 : Category.{v_2, u_2} E
F : Functor.{v_1, v_2, u_1, u_2} D E
inst_6 : PreservesFilteredColimitsOfSize.{w, w, v_1, v_2, u_1, u_2} F
⊢ PreservesColimitsOfShape.{v, u, v_1, v_2, u_1, u_2} C F

Tactic:
Functor.Final.preservesColimitsOfShape_of_final
    (FinallySmall.fromFilteredFinalModel.{w} C) _

Premises used: CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final, CategoryTheory.FinallySmall.fromFilteredFinalModel
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : InitiallySmall.{w, v, u} C
obtain :
  ∀ (D : Type w) (w : SmallCategory D),
    IsFiltered D →
      ∀ (F : Functor.{w, v, w, u} D Cᵒᵖ),
        F.Final → ∃ (D : Type w) (x : SmallCategory D) (_ : IsCofiltered D) (F : Functor.{w, v, w, u} D C), F.Initial
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsCofiltered D) (F : Functor.{w, v, w, u} D C), F.Initial

Tactic:
obtain ⟨D, _, _, F, _⟩ := FinallySmall.exists_of_isFiltered.{w} Cᵒᵖ
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : InitiallySmall.{w, v, u} C
D : Type w
w : SmallCategory D
w_1 : IsFiltered D
F : Functor.{w, v, w, u} D Cᵒᵖ
h : F.Final
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsCofiltered D) (F : Functor.{w, v, w, u} D C), F.Initial

Tactic:
⟨Dᵒᵖ, inferInstance, inferInstance, F.leftOp, inferInstance⟩

Premises used: Opposite, inferInstance, Exists.intro, CategoryTheory.Functor.leftOp
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : InitiallySmall.{w, v, u} C
D : Type w
w : SmallCategory D
w_1 : IsFiltered D
F : Functor.{w, v, w, u} D Cᵒᵖ
h : F.Final
⊢ ∃ (D : Type w) (x : SmallCategory D) (_ : IsCofiltered D) (F : Functor.{w, v, w, u} D C), F.Initial

Tactic:
exact ⟨Dᵒᵖ, inferInstance, inferInstance, F.leftOp, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : InitiallySmall.{w, v, u} C
⊢ IsCofiltered.{w, w} (CofilteredInitialModel.{w, v, u} C)

Tactic:
(exists_of_isCofiltered.{w} C).choose_spec.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.InitiallySmall.exists_of_isCofiltered, Exists.choose, CategoryTheory.InitiallySmall.CofilteredInitialModel
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : InitiallySmall.{w, v, u} C
⊢ Functor.Initial.{w, v, w, u} (C := CofilteredInitialModel.{w, v, u} C) (fromCofilteredInitialModel C)

Tactic:
(exists_of_isCofiltered.{w} C).choose_spec.choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.InitiallySmall.exists_of_isCofiltered, CategoryTheory.InitiallySmall.fromCofilteredInitialModel, CategoryTheory.InitiallySmall.CofilteredInitialModel
-- Module: Mathlib.CategoryTheory.Filtered.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFiltered.{v₂, u₂} D
inst_3 : RepresentablyCoflat F
⊢ IsFiltered.{v₁, u₁} C

Tactic:
isFiltered_of_isFiltered_costructuredArrow F (𝟭 _)

Premises used: CategoryTheory.Functor.id, CategoryTheory.isFiltered_of_isFiltered_costructuredArrow
-- Module: Mathlib.CategoryTheory.Filtered.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofiltered.{v₂, u₂} D
inst_3 : RepresentablyFlat F
⊢ IsFiltered.{v₁, u₁} Cᵒᵖ

Tactic:
have := isFiltered_of_representablyCoflat F.op
-- Module: Mathlib.CategoryTheory.Filtered.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofiltered.{v₂, u₂} D
inst_3 : RepresentablyFlat F
this : IsFiltered.{v₁, u₁} Cᵒᵖ
⊢ IsCofiltered.{v₁, u₁} C

Tactic:
isCofiltered_of_isFiltered_op C

Premises used: CategoryTheory.isCofiltered_of_isFiltered_op
-- Module: Mathlib.CategoryTheory.Filtered.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofiltered.{v₂, u₂} D
inst_3 : RepresentablyFlat F
this : IsFiltered.{v₁, u₁} Cᵒᵖ
⊢ IsCofiltered.{v₁, u₁} C

Tactic:
exact isCofiltered_of_isFiltered_op C

Premises used: CategoryTheory.isCofiltered_of_isFiltered_op
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
⊢ IsFilteredOrEmpty (Grothendieck F)

Tactic:
⟨?_, ?_⟩

Premises used: CategoryTheory.IsFilteredOrEmpty.mk
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
refine_1 : ∀ (X Y : Grothendieck F), ∃ (Z : Grothendieck F) (x : X ⟶ Z) (x : Y ⟶ Z), True
refine_2 : ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ (Z : Grothendieck F) (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ IsFilteredOrEmpty (Grothendieck F)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
⊢ ∃ (Z : Grothendieck F) (x : { base := c, fiber := f : Grothendieck F } ⟶ Z) (x :
    { base := d, fiber := g : Grothendieck F } ⟶ Z), True

Tactic:
⟨⟨max c d, max ((F.map (leftToMax c d)).toFunctor.obj f)
      ((F.map (rightToMax c d)).toFunctor.obj g)⟩,
      ⟨leftToMax c d, leftToMax _ _⟩, ⟨rightToMax c d, rightToMax _ _⟩, trivial⟩

Premises used: CategoryTheory.IsFiltered.rightToMax, trivial, CategoryTheory.IsFiltered.max, CategoryTheory.Functor.map, CategoryTheory.Grothendieck.mk, Exists.intro, CategoryTheory.Grothendieck.Hom.mk, CategoryTheory.IsFiltered.leftToMax, CategoryTheory.Cat.Hom.toFunctor, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
⊢ ∃ (Z : Grothendieck F) (x : { base := c, fiber := f : Grothendieck F } ⟶ Z) (x :
    { base := d, fiber := g : Grothendieck F } ⟶ Z), True

Tactic:
exact ⟨⟨max c d, max ((F.map (leftToMax c d)).toFunctor.obj f)
      ((F.map (rightToMax c d)).toFunctor.obj g)⟩,
      ⟨leftToMax c d, leftToMax _ _⟩, ⟨rightToMax c d, rightToMax _ _⟩, trivial⟩
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
u : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ ∃ (Z : Grothendieck F) (h : { base := d, fiber := g : Grothendieck F } ⟶ Z),
    Eq (α := { base := c, fiber := f : Grothendieck F } ⟶ Z)
      ({ base := u, fiber := x :
          { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
        h)
      ({ base := v, fiber := y :
          { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
        h)

Tactic:
⟨⟨coeq u v, coeq (eqToHom ?_ ≫
        (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y)⟩,
          ⟨coeqHom u v, coeqHom _ _⟩, ?_⟩

Premises used: CategoryTheory.IsFiltered.coeqHom, CategoryTheory.eqToHom, CategoryTheory.Functor.map, CategoryTheory.Grothendieck.mk, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.coeq, CategoryTheory.Grothendieck.Hom.mk, CategoryTheory.Cat.Hom.toFunctor