awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasFiniteColimits.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ RepresentablyCoflat F ↔ PreservesFiniteColimits F

Tactic:
⟨fun _ => preservesFiniteColimits_of_coflat F, fun _ => coflat_of_preservesFiniteColimits F⟩

Premises used: CategoryTheory.preservesFiniteColimits_of_coflat, Iff.intro, CategoryTheory.coflat_of_preservesFiniteColimits
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst_3 : ∀ (X : D), HasColimitsOfShape.{u₁, u₁, u₁, u₂} (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
⊢ ∀ (G : C ⥤ E),
    ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).ι.app T ≫
        Iso.hom
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))) =
      (colimit.cocone (CostructuredArrow.proj F X ⋙ G)).ι.app T

Tactic:
have h₁ := fun (G : C ⥤ E) => IsColimit.comp_coconePointUniqueUpToIso_hom
        (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G X) (colimit.isColimit _) T
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst_3 : ∀ (X : D), HasColimitsOfShape.{u₁, u₁, u₁, u₂} (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₁ :
  ∀ (G : C ⥤ E),
    ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).ι.app T ≫
        Iso.hom
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))) =
      (colimit.cocone (CostructuredArrow.proj F X ⋙ G)).ι.app T
⊢ Eq (α :=
    (Functor.obj (𝟭 (C ⥤ E)) G₁).obj T.left ⟶
      (Functor.obj (F.lan ⋙ Functor.obj (Functor.whiskeringLeft C D E) F) G₂).obj T.left)
    (NatTrans.app (Functor.map (𝟭 (C ⥤ E)) φ ≫ NatTrans.app F.lanUnit G₂) T.left)
    (NatTrans.app (NatTrans.app F.lanUnit G₁ ≫ Functor.map (F.lan ⋙ Functor.obj (Functor.whiskeringLeft C D E) F) φ)
      T.left)

Tactic:
have h₂ := congr_app (F.lanUnit.naturality φ) T.left
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst_3 : ∀ (X : D), HasColimitsOfShape.{u₁, u₁, u₁, u₂} (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₂ :
  Eq (α := G₁.obj T.left ⟶ (F.leftKanExtension G₂).obj (F.obj T.left))
    (φ.app T.left ≫ NatTrans.app (F.leftKanExtensionUnit G₂) T.left)
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      NatTrans.app
        ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
          (φ ≫ F.leftKanExtensionUnit G₂))
        (F.obj T.left))
h₁ :
  ∀ (G : C ⥤ E),
    Eq (α := G.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G))
      (NatTrans.app (F.leftKanExtensionUnit G) T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          Iso.hom
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))))
      (colimit.ι (CostructuredArrow.proj F X ⋙ G) T)
rw :
  Eq (α := G₁.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂))
    (φ.app T.left ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T)
    (φ.app ((CostructuredArrow.proj F X).obj T) ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T)
⊢ Eq (α := G₁.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂))
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        CategoryStruct.comp (Y := (F.leftKanExtension G₂).obj X)
          (NatTrans.app
              ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
                (φ ≫ F.leftKanExtensionUnit G₂))
              X :
            (F.leftKanExtension G₁).obj X ⟶ (F.leftKanExtension G₂).obj X)
          (Iso.hom
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
                (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))) :
            (F.leftKanExtension G₂).obj X ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂)))
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        CategoryStruct.comp (Y := colimit (CostructuredArrow.proj F X ⋙ G₁))
          (Iso.hom
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))))
          (colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)))

Tactic:
rw [reassoc_of% h₁, NatTrans.naturality_assoc, ← reassoc_of% h₂, h₁,
        ι_colimMap, Functor.whiskerLeft_app]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst_3 : ∀ (X : D), HasColimitsOfShape.{u₁, u₁, u₁, u₂} (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₂ :
  Eq (α := G₁.obj T.left ⟶ (F.leftKanExtension G₂).obj (F.obj T.left))
    (φ.app T.left ≫ NatTrans.app (F.leftKanExtensionUnit G₂) T.left)
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      NatTrans.app
        ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
          (φ ≫ F.leftKanExtensionUnit G₂))
        (F.obj T.left))
h₁ :
  ∀ (G : C ⥤ E),
    Eq (α := G.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G))
      (NatTrans.app (F.leftKanExtensionUnit G) T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          Iso.hom
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))))
      (colimit.ι (CostructuredArrow.proj F X ⋙ G) T)
⊢ Eq (α := G₁.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂))
    (φ.app T.left ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T)
    (φ.app ((CostructuredArrow.proj F X).obj T) ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
h :
  ∀ (J : Type u₁) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan
⊢ PreservesFiniteLimits (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) F.op.lan

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
J : Type u₁
h : ∀ {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan
⊢ ∀ {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan

Tactic:
_
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
J : Type u₁
𝒥 : SmallCategory J
h : ∀ (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan
⊢ ∀ (x : FinCategory J), PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan

Tactic:
_
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
J : Type u₁
𝒥 : SmallCategory J
x : FinCategory J
h :
  ∀ (k : Dᵒᵖ),
    PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J (F.op.lan ⋙ Functor.obj (evaluation Dᵒᵖ E) k)
⊢ PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan

Tactic:
apply preservesLimitsOfShape_of_evaluation (F.op.lan : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation, CategoryTheory.Functor.lan
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
J : Type u₁
𝒥 : SmallCategory J
x : FinCategory J
K : Dᵒᵖ
⊢ IsFiltered.{u₁, u₁} (CostructuredArrow F.op K)

Tactic:
haveI : IsFiltered (CostructuredArrow F.op K) :=
    IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
J : Type u₁
𝒥 : SmallCategory J
x : FinCategory J
K : Dᵒᵖ
this : IsFiltered.{u₁, u₁} (CostructuredArrow F.op K)
⊢ PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J (F.op.lan ⋙ Functor.obj (evaluation Dᵒᵖ E) K)

Tactic:
preservesLimitsOfShape_of_natIso (lanEvaluationIsoColim _ _ _).symm

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Iso.symm, CategoryTheory.lanEvaluationIsoColim
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
J : Type u₁
𝒥 : SmallCategory J
x : FinCategory J
K : Dᵒᵖ
this : IsFiltered.{u₁, u₁} (CostructuredArrow F.op K)
⊢ PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J (F.op.lan ⋙ Functor.obj (evaluation Dᵒᵖ E) K)

Tactic:
exact preservesLimitsOfShape_of_natIso (lanEvaluationIsoColim _ _ _).symm

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Iso.symm, CategoryTheory.lanEvaluationIsoColim
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
F : C ⥤ D
inst_10 : RepresentablyFlat F
⊢ RepresentablyFlat (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) F.op.lan

Tactic:
flat_of_preservesFiniteLimits _

Premises used: CategoryTheory.flat_of_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
inst_10 : HasFiniteLimits C
F : C ⥤ D
inst_11 : PreservesFiniteLimits F
⊢ RepresentablyFlat F

Tactic:
haveI := flat_of_preservesFiniteLimits F
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst_3 : (X Y : E) → FunLike.{u_1 + 1, u₁ + 1, u₁ + 1} (FE X Y) (CE X) (CE Y)
inst_4 : ConcreteCategory E FE (CC := CE)
inst_5 : HasLimits.{u₁, u₂} E
inst_6 : HasColimits.{u₁, u₂} E
inst_7 : ReflectsLimits (forget E (FC := FE) (CC := CE))
inst_8 : PreservesFilteredColimits (forget E (FC := FE) (CC := CE))
inst_9 : PreservesLimits (forget E (FC := FE) (CC := CE))
inst_10 : HasFiniteLimits C
F : C ⥤ D
inst_11 : PreservesFiniteLimits F
this : RepresentablyFlat F
⊢ PreservesFiniteLimits (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) F.op.lan

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
inst_2 : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
⊢ PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan

Tactic:
haveI := preservesFiniteLimits_of_flat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁)
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
inst_2 : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
this : PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
h : ∀ (J : Type u₁) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
⊢ PreservesFiniteLimits F

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
inst_2 : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
this : PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
J : Type u₁
𝒥 : SmallCategory J
x : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
apply preservesLimit_of_lan_preservesLimit

Premises used: CategoryTheory.preservesLimit_of_lan_preservesLimit
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
inst_2 : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
this : PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
⊢ PreservesFiniteLimits F

Tactic:
haveI : PreservesFiniteLimits F := by
      apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
      intros; apply preservesLimit_of_lan_preservesLimit
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
inst_2 : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
this_1 : PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
this : PreservesFiniteLimits F
⊢ RepresentablyFlat F

Tactic:
apply flat_of_preservesFiniteLimits

Premises used: CategoryTheory.flat_of_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
inst_2 : HasFiniteLimits C
F : C ⥤ D
⊢ PreservesFiniteLimits F ↔ PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan

Tactic:
⟨fun _ ↦ inferInstance,
    fun _ ↦ preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁} _
      (fun _ _ _ ↦ preservesLimit_of_lan_preservesLimit _ _)⟩

Premises used: CategoryTheory.preservesLimit_of_lan_preservesLimit, inferInstance, CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize, Iff.intro
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
⊢ (StructuredArrow.pre X F G).Final

Tactic:
⟨fun _ ↦ isConnected_of_equivalent (StructuredArrow.preEquivalence _ _).symm⟩

Premises used: CategoryTheory.StructuredArrow.preEquivalence, CategoryTheory.Functor.Final.mk, CategoryTheory.Equivalence.symm, CategoryTheory.isConnected_of_equivalent
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyCoflat F
⊢ (CostructuredArrow.pre F G X).Initial

Tactic:
⟨fun _ ↦ isConnected_of_equivalent (CostructuredArrow.preEquivalence _ _).symm⟩

Premises used: CategoryTheory.Functor.Initial.mk, CategoryTheory.CostructuredArrow.preEquivalence, CategoryTheory.Equivalence.symm, CategoryTheory.isConnected_of_equivalent
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
obtain : ∀ (Y : StructuredArrow X G), IsCofiltered (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
obtain ⟨Y⟩ := IsCofiltered.nonempty (C := StructuredArrow X G)

Premises used: CategoryTheory.IsCofiltered.nonempty
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
obtain : ∀ (A : StructuredArrow Y.right F), IsCofiltered (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
obtain ⟨A⟩ := IsCofiltered.nonempty (C := StructuredArrow Y.right F)

Premises used: CategoryTheory.IsCofiltered.nonempty
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
⊢ Nonempty (StructuredArrow X (F ⋙ G))

Tactic:
have : Nonempty (StructuredArrow X (F ⋙ G)) := ⟨.mk (Y.hom ≫ G.map A.hom)⟩
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this_1 : Nonempty (StructuredArrow X (F ⋙ G))
this : IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
suffices : IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
suffices IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G)) by constructor
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
⊢ IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))

Tactic:
⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩

Premises used: CategoryTheory.IsCofilteredOrEmpty.mk
-- Module: Mathlib.CategoryTheory.Functor.Flat
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
X : E
inst_3 : RepresentablyFlat F
inst_4 : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
refine_1 : ∀ (A B : StructuredArrow X (F ⋙ G)), ∃ (W : StructuredArrow X (F ⋙ G)) (x : W ⟶ A) (x : W ⟶ B), True
refine_2 :
  ∀ (A B : StructuredArrow X (F ⋙ G)) (f g : A ⟶ B), ∃ (W : StructuredArrow X (F ⋙ G)) (h : W ⟶ A), h ≫ f = h ≫ g
⊢ IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))

Tactic:
refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩