awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 : RepresentablyFlat F
J : Type v₁
𝒥 : SmallCategory J
x : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))
have h : IsLimit (F.mapCone c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 : RepresentablyFlat F
J : Type v₁
𝒥 : SmallCategory J
x : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ m = PreservesFiniteLimitsOfFlat.lift F hc s
have h₁ : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
Tactic: apply PreservesFiniteLimitsOfFlat.uniq F hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 : RepresentablyFlat F
J : Type v₁
𝒥 : SmallCategory J
x : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
h₁ : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ m = PreservesFiniteLimitsOfFlat.lift F hc s
have h₂ : ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app j = s.π.app j
Tactic: apply PreservesFiniteLimitsOfFlat.uniq F hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
⊢ Eq (α :=
    (CostructuredArrow.proj F X ⋙ G₁).obj T ⟶
      Functor.obj
        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) G₂)
    (((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      Functor.map (F.lan ⋙ Functor.obj (evaluation D E) X) φ ≫
        Iso.hom
          ((fun (G : C ⥤ E) ↦
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                  (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
                ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                  (colimit.cocone
                      (Functor.obj
                        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                        G)).pt))
            G₂))
    (((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      Iso.hom
          ((fun (G : C ⥤ E) ↦
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                  (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
                ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                  (colimit.cocone
                      (Functor.obj
                        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                        G)).pt))
            G₁) ≫
        Functor.map
          (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) φ)
have 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
Tactic: have h₁ := fun (G : C ⥤ E) => IsColimit.comp_coconePointUniqueUpToIso_hom
        (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G X) (colimit.isColimit _) T
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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 (α :=
    (CostructuredArrow.proj F X ⋙ G₁).obj T ⟶
      Functor.obj
        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) G₂)
    (((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      Functor.map (F.lan ⋙ Functor.obj (evaluation D E) X) φ ≫
        Iso.hom
          ((fun (G : C ⥤ E) ↦
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                  (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
                ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                  (colimit.cocone
                      (Functor.obj
                        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                        G)).pt))
            G₂))
    (((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app T ≫
      Iso.hom
          ((fun (G : C ⥤ E) ↦
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                  (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
                ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                  (colimit.cocone
                      (Functor.obj
                        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                        G)).pt))
            G₁) ≫
        Functor.map
          (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) φ)
have h₂ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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),
    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)
h₂ :
  Eq (α := G₁.obj T.left ⟶ (Functor.obj F.lan G₂).obj (F.obj T.left))
    (φ.app T.left ≫ NatTrans.app (NatTrans.app F.lanUnit G₂) T.left)
    (NatTrans.app (NatTrans.app F.lanUnit G₁) T.left ≫ NatTrans.app (Functor.map F.lan φ) (F.obj T.left))
⊢ Eq (α := G₁.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂))
    ((NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫ (F.leftKanExtension G₁).map T.hom) ≫
      NatTrans.app (Functor.map F.lan φ) X ≫
        Iso.hom
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
            (colimit.isColimit (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 φ)))
have simp : ∀
  (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₂))
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        NatTrans.app (Functor.map F.lan φ) X ≫
          Iso.hom
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (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: simp only [Category.assoc] at h₁ ⊢
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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 ⟶ (Functor.obj F.lan G₂).obj (F.obj T.left))
    (φ.app T.left ≫ NatTrans.app (NatTrans.app F.lanUnit G₂) T.left)
    (NatTrans.app (NatTrans.app F.lanUnit G₁) T.left ≫ NatTrans.app (Functor.map F.lan φ) (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₂))
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        NatTrans.app (Functor.map F.lan φ) X ≫
          Iso.hom
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (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 φ)))
have simp : 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: simp only [Functor.lan, Functor.lanUnit] at h₂ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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₂))
    (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 φ)))
have 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)
Tactic: rw [reassoc_of% h₁, NatTrans.naturality_assoc, ← reassoc_of% h₂, h₁,
        ι_colimMap, Functor.whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ PreservesFiniteLimits (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) F.op.lan
have h : ∀ (J : Type u₁) {𝒥 : SmallCategory J} (x : FinCategory J),
  PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J F.op.lan
have h : ∀ (k : Dᵒᵖ),
  PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J (F.op.lan ⋙ Functor.obj (evaluation Dᵒᵖ E) k)
Tactic: apply preservesLimitsOfShape_of_evaluation (F.op.lan : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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ᵒᵖ
⊢ PreservesLimitsOfShape (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) J (F.op.lan ⋙ Functor.obj (evaluation Dᵒᵖ E) K)
have this : IsFiltered.{u₁, u₁} (CostructuredArrow F.op K)
Tactic: haveI : IsFiltered (CostructuredArrow F.op K) :=
    IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
⊢ PreservesFiniteLimits (C := Functor.{u₁, u₁, u₁, u₂} Cᵒᵖ E) F.op.lan
have this : RepresentablyFlat F
Tactic: haveI := flat_of_preservesFiniteLimits F
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
⊢ RepresentablyFlat F
have this : PreservesFiniteLimits (C := Cᵒᵖ ⥤ Type u₁) F.op.lan
Tactic: haveI := preservesFiniteLimits_of_flat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
have h : ∀ (J : Type u₁) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
⊢ RepresentablyFlat F
have this₁ : PreservesFiniteLimits F
Tactic: haveI : PreservesFiniteLimits F := by
      apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
      intros; apply preservesLimit_of_lan_preservesLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
have obtain : ∀ (Y : StructuredArrow X G), IsCofiltered (StructuredArrow X (F ⋙ G))
Tactic: obtain ⟨Y⟩ := IsCofiltered.nonempty (C := StructuredArrow X G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
have obtain : ∀ (A : StructuredArrow Y.right F), IsCofiltered (StructuredArrow X (F ⋙ G))
Tactic: obtain ⟨A⟩ := IsCofiltered.nonempty (C := StructuredArrow Y.right F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
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
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
have this : Nonempty (StructuredArrow X (F ⋙ G))
Tactic: have : Nonempty (StructuredArrow X (F ⋙ G)) := ⟨.mk (Y.hom ≫ G.map A.hom)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
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))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))
have suffices : IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
Tactic: suffices IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G)) by constructor