awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteLimits.{v, u} C
⊢ IsCofiltered.{v, u} C

Tactic:
of_cone_nonempty.{v} C fun F => ⟨limit.cone F⟩

Premises used: CategoryTheory.Limits.limit.cone, Nonempty.intro, CategoryTheory.IsCofiltered.of_cone_nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : IsInitial.{v, u} X
⊢ IsCofiltered.{v, u} C

Tactic:
of_cone_nonempty.{v} _ fun {_} _ _ _ => ⟨⟨X, ⟨fun _ => h.to _, fun _ _ _ => h.hom_ext _ _⟩⟩⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.NatTrans.mk, CategoryTheory.Limits.IsInitial.to, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofiltered.of_cone_nonempty, CategoryTheory.Functor.const, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
⊢ IsCofiltered.{v, u} C

Tactic:
of_isInitial _ initialIsInitial

Premises used: CategoryTheory.IsCofiltered.of_isInitial, CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsCofiltered.{v, u} C ↔
    ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)

Tactic:
⟨fun _ _ _ _ F => cone_nonempty F, of_cone_nonempty C⟩

Premises used: CategoryTheory.IsCofiltered.cone_nonempty, Iff.intro, CategoryTheory.IsCofiltered.of_cone_nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f = f.unop.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ g = g.unop.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
rw :
  Eq (α := op (IsFiltered.coeq f.unop.op.unop g.unop.op.unop) ⟶ Y)
    (Quiver.Hom.op (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
    (Quiver.Hom.op (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
⊢ Eq (α := op (IsFiltered.coeq f.unop g.unop) ⟶ Y) (Quiver.Hom.op (IsFiltered.coeqHom f.unop g.unop) ≫ f)
    (Quiver.Hom.op (IsFiltered.coeqHom f.unop g.unop) ≫ g)

Tactic:
rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
e_f :
  Eq (α := unop Y ⟶ IsFiltered.coeq f.unop.op.unop g.unop.op.unop)
    (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)
    (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)
⊢ Eq (α := op (IsFiltered.coeq f.unop.op.unop g.unop.op.unop) ⟶ Y)
    (Quiver.Hom.op (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
    (Quiver.Hom.op (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := unop Y ⟶ IsFiltered.coeq f.unop.op.unop g.unop.op.unop)
    (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)
    (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)

Tactic:
IsFiltered.coeq_condition f.unop g.unop

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := unop Y ⟶ IsFiltered.coeq f.unop.op.unop g.unop.op.unop)
    (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)
    (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)

Tactic:
exact IsFiltered.coeq_condition f.unop g.unop

Premises used: Quiver.Hom.unop, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f = f.unop.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ g = g.unop.op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
rw :
  Eq (α := X ⟶ op (IsCofiltered.eq f.unop.op.unop g.unop.op.unop))
    (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop))
    (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop))
⊢ Eq (α := X ⟶ op (IsCofiltered.eq f.unop g.unop)) (f ≫ Quiver.Hom.op (IsCofiltered.eqHom f.unop g.unop))
    (g ≫ Quiver.Hom.op (IsCofiltered.eqHom f.unop g.unop))

Tactic:
rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
e_f :
  Eq (α := IsCofiltered.eq f.unop.op.unop g.unop.op.unop ⟶ unop X)
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop)
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop)
⊢ Eq (α := X ⟶ op (IsCofiltered.eq f.unop.op.unop g.unop.op.unop))
    (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop))
    (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := IsCofiltered.eq f.unop.op.unop g.unop.op.unop ⟶ unop X)
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop)
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop)

Tactic:
IsCofiltered.eq_condition f.unop g.unop

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := IsCofiltered.eq f.unop.op.unop g.unop.op.unop ⟶ unop X)
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop)
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop)

Tactic:
exact IsCofiltered.eq_condition f.unop g.unop

Premises used: Quiver.Hom.unop, CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} Cᵒᵖ
⊢ IsCofilteredOrEmpty.{v, u} C

Tactic:
IsCofilteredOrEmpty.of_equivalence (opOpEquivalence _)

Premises used: CategoryTheory.IsCofilteredOrEmpty.of_equivalence, CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} Cᵒᵖ
⊢ IsFilteredOrEmpty.{v, u} C

Tactic:
IsFilteredOrEmpty.of_equivalence (opOpEquivalence _)

Premises used: CategoryTheory.IsFilteredOrEmpty.of_equivalence, CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} Cᵒᵖ
⊢ IsCofiltered.{v, u} C

Tactic:
IsCofiltered.of_equivalence (opOpEquivalence _)

Premises used: CategoryTheory.opOpEquivalence, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} Cᵒᵖ
⊢ IsFiltered.{v, u} C

Tactic:
IsFiltered.of_equivalence (opOpEquivalence _)

Premises used: CategoryTheory.opOpEquivalence, CategoryTheory.IsFiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsCofiltered.{v, u} Cᵒᵖ ↔ IsFiltered.{v, u} C

Tactic:
⟨fun _ ↦ isFiltered_of_isCofiltered_op _, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.isFiltered_of_isCofiltered_op
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ IsFiltered.{v, u} Cᵒᵖ ↔ IsCofiltered.{v, u} C

Tactic:
⟨fun _ ↦ isCofiltered_of_isFiltered_op _, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.isCofiltered_of_isFiltered_op
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
⊢ IsFiltered (ULift.{u₂, u} C)

Tactic:
IsFiltered.of_equivalence ULift.equivalence

Premises used: CategoryTheory.ULift.equivalence, CategoryTheory.IsFiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
⊢ IsCofiltered (ULift.{u₂, u} C)

Tactic:
IsCofiltered.of_equivalence ULift.equivalence

Premises used: CategoryTheory.ULift.equivalence, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
⊢ IsFiltered (ULiftHom C)

Tactic:
IsFiltered.of_equivalence ULiftHom.equiv

Premises used: CategoryTheory.IsFiltered.of_equivalence, CategoryTheory.ULiftHom.equiv
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
⊢ IsCofiltered (ULiftHom C)

Tactic:
IsCofiltered.of_equivalence ULiftHom.equiv

Premises used: CategoryTheory.IsCofiltered.of_equivalence, CategoryTheory.ULiftHom.equiv
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
⊢ IsFiltered (AsSmall.{u_1, v, u} C)

Tactic:
IsFiltered.of_equivalence AsSmall.equiv

Premises used: CategoryTheory.AsSmall.equiv, CategoryTheory.IsFiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
⊢ IsCofiltered (AsSmall.{u_1, v, u} C)

Tactic:
IsCofiltered.of_equivalence AsSmall.equiv

Premises used: CategoryTheory.AsSmall.equiv, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
I : α → Type u₁
inst_1 : (i : α) → Category.{v₁, u₁} (I i)
inst_2 : ∀ (i : α), IsFilteredOrEmpty.{v₁, u₁} (I i)
k l : (i : α) → I i
f g : k ⟶ l
s : α
⊢ Eq.{v₁ + 1} (α := k s ⟶ (fun (s : α) ↦ coeq (f s) (g s)) s)
    ((f ≫ fun (s : α) ↦ coeqHom (f s) (g s)) s : k s ⟶ (fun (s : α) ↦ coeq (f s) (g s)) s)
    ((g ≫ fun (s : α) ↦ coeqHom (f s) (g s)) s : k s ⟶ (fun (s : α) ↦ coeq (f s) (g s)) s)

Tactic:
simp [coeq_condition (f s) (g s)]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
I : α → Type u₁
inst_1 : (i : α) → Category.{v₁, u₁} (I i)
inst_2 : ∀ (i : α), IsCofilteredOrEmpty.{v₁, u₁} (I i)
k l : (i : α) → I i
f g : k ⟶ l
s : α
⊢ Eq.{v₁ + 1} (α := (fun (s : α) ↦ eq (f s) (g s)) s ⟶ l s)
    (((fun (s : α) ↦ eqHom (f s) (g s)) ≫ f) s : (fun (s : α) ↦ eq (f s) (g s)) s ⟶ l s)
    (((fun (s : α) ↦ eqHom (f s) (g s)) ≫ g) s : (fun (s : α) ↦ eq (f s) (g s)) s ⟶ l s)

Tactic:
simp [eq_condition (f s) (g s)]

Premises used: CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
inst_4 : IsFilteredOrEmpty.{v₂, u₂} D
k l : C × D
f g : k ⟶ l
⊢ Eq (α := k ⟶ (coeq f.1 g.1, coeq f.2 g.2)) (f ≫ (coeqHom f.1 g.1, coeqHom f.2 g.2))
    (g ≫ (coeqHom f.1 g.1, coeqHom f.2 g.2))

Tactic:
simp [coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : IsCofilteredOrEmpty.{v₁, u₁} C
inst_4 : IsCofilteredOrEmpty.{v₂, u₂} D
k l : C × D
f g : k ⟶ l
⊢ Eq (α := (eq f.1 g.1, eq f.2 g.2) ⟶ l) ((eqHom f.1 g.1, eqHom f.2 g.2) ≫ f) ((eqHom f.1 g.1, eqHom f.2 g.2) ≫ g)

Tactic:
simp [eq_condition]

Premises used: CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Connected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
⊢ IsPreconnected.{v, u} C

Tactic:
zigzag_isPreconnected fun j j' => .trans
    (.single <| .inl <| .intro <| IsFiltered.leftToMax j j')
    (.single <| .inr <| .intro <| IsFiltered.rightToMax j j')

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.zigzag_isPreconnected, Nonempty.intro, Relation.ReflTransGen.single, CategoryTheory.IsFiltered.leftToMax, Or.inl, CategoryTheory.Zigzag.trans, Or.inr
-- Module: Mathlib.CategoryTheory.Filtered.Connected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
⊢ IsPreconnected.{v, u} C

Tactic:
zigzag_isPreconnected fun j j' => .trans
    (.single <| .inr <| .intro <| IsCofiltered.minToLeft j j')
    (.single <| .inl <| .intro <| IsCofiltered.minToRight j j')

Premises used: CategoryTheory.zigzag_isPreconnected, Nonempty.intro, CategoryTheory.IsCofiltered.minToRight, Relation.ReflTransGen.single, Or.inl, CategoryTheory.Zigzag.trans, Or.inr, CategoryTheory.IsCofiltered.minToLeft
-- Module: Mathlib.CategoryTheory.Filtered.Connected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
⊢ IsConnected.{v, u} C

Tactic:
{ IsFilteredOrEmpty.isPreconnected C with }

Premises used: CategoryTheory.IsFilteredOrEmpty.isPreconnected, CategoryTheory.IsConnected.mk
-- Module: Mathlib.CategoryTheory.Filtered.Connected
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
⊢ IsConnected.{v, u} C

Tactic:
{ IsCofilteredOrEmpty.isPreconnected C with }

Premises used: CategoryTheory.IsConnected.mk, CategoryTheory.IsCofilteredOrEmpty.isPreconnected
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
⊢ IsFiltered A

Tactic:
isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩

Premises used: Nonempty.intro, CategoryTheory.isFiltered_of_nonempty_limit_colimit_to_colimit_limit
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
refine :
  (J : Type u₁) →
    {x : SmallCategory J} → {x_1 : FinCategory J} → (F : J ⥤ A ⥤ Type u₁) → limit (colimit F.flip) ⟶ colimit (limit F)
⊢ IsFiltered A

Tactic:
refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩

Premises used: Nonempty.intro, CategoryTheory.isFiltered_of_nonempty_limit_colimit_to_colimit_limit
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
b : B
⊢ PreservesLimitsOfShape (C := CostructuredArrow L (R.obj b) ⥤ Type u₁) J colim

Tactic:
filtered_colim_preservesFiniteLimits

Premises used: CategoryTheory.Cat.of, CategoryTheory.CostructuredArrow, CategoryTheory.Bundled.of, CategoryTheory.Limits.filtered_colim_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
b : B
⊢ PreservesLimitsOfShape (C := CostructuredArrow L (R.obj b) ⥤ Type u₁) J colim

Tactic:
exact filtered_colim_preservesFiniteLimits

Premises used: CategoryTheory.Limits.filtered_colim_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
⊢ ∀ (b : B), PreservesLimitsOfShape (C := (↑((R ⋙ CostructuredArrow.functor L).obj b) : Type u₁) ⥤ Type u₁) J colim

Tactic:
haveI : ∀ b, PreservesLimitsOfShape J
      (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by
    simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α]
    exact filtered_colim_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape (C := (↑((R ⋙ CostructuredArrow.functor L).obj b) : Type u₁) ⥤ Type u₁) J colim
refine :
  limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Tactic:
refine lim.map ((colimitIsoColimitGrothendieck L F.flip).hom ≫
    (inv (colimit.pre (CostructuredArrow.grothendieckProj L ⋙ F.flip) R'))) ≫
    (colimitLimitIso (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip).inv ≫
    colim.map ?_ ≫
    colimit.pre _ R' ≫
    (colimitIsoColimitGrothendieck L (limit F)).inv

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Limits.colim, CategoryTheory.Limits.colimitLimitIso, CategoryTheory.CostructuredArrow.grothendieckProj, CategoryTheory.Functor.comp, CategoryTheory.Limits.lim, CategoryTheory.Functor.map, CategoryTheory.Limits.limit, CategoryTheory.Functor.colimitIsoColimitGrothendieck, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.Limits.colimit.pre, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape (C := (↑((R ⋙ CostructuredArrow.functor L).obj b) : Type u₁) ⥤ Type u₁) J colim
⊢ limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F

Tactic:
exact (limitCompWhiskeringLeftIsoCompLimit F (R' ⋙ CostructuredArrow.grothendieckProj L)).hom

Premises used: CategoryTheory.CostructuredArrow.grothendieckProj, CategoryTheory.Functor.comp, CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₂, u₂} B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun (b : B) ↦
    Equivalence.trans
      (asEquivalence
        (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
          ((sB.inverse ⋙ R ⋙ sT.functor).obj
            { down := b : ULift.{max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃, u₂} B })))
      (Equivalence.symm (asEquivalence (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b })))))
⊢ ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))

Tactic:
haveI : ∀ b, IsFiltered (CostructuredArrow _ ((sB.inverse ⋙ R ⋙ sT.functor).obj b)) :=
    fun b => IsFiltered.of_equivalence (sC b.1).symm
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₂, u₂} B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun (b : B) ↦
    Equivalence.trans
      (asEquivalence
        (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
          ((sB.inverse ⋙ R ⋙ sT.functor).obj
            { down := b : ULift.{max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃, u₂} B })))
      (Equivalence.symm (asEquivalence (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b })))))
this :
  ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
⊢ IsFiltered (AsSmall A)

Tactic:
haveI := isFiltered_of_isFiltered_costructuredArrow_small
    (sA.inverse ⋙ L ⋙ sT.functor) (sB.inverse ⋙ R ⋙ sT.functor)
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₂, u₂} B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun (b : B) ↦
    Equivalence.trans
      (asEquivalence
        (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
          ((sB.inverse ⋙ R ⋙ sT.functor).obj
            { down := b : ULift.{max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃, u₂} B })))
      (Equivalence.symm (asEquivalence (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b })))))
this_1 :
  ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
this : IsFiltered (AsSmall A)
⊢ IsFiltered.{v₁, u₁} A

Tactic:
IsFiltered.of_equivalence sA.symm

Premises used: CategoryTheory.IsFiltered.of_equivalence, CategoryTheory.Equivalence.symm