awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∃ (a : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (colimitLimitToLimitColimit F) :
          (a : (fun (X : Type v) ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))) →
            (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim)))
        a =
      x
have w : (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ (fun (X : Type v) ↦ X) (colimit (obj curry (swap K J ⋙ F) ⋙ lim))
have apply : (obj curry (swap K J ⋙ F) ⋙ lim).obj k''
Tactic: apply colimit.ι (curry.obj (swap K J ⋙ F) ⋙ Limits.lim) k'' _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ limit ((obj curry (swap K J ⋙ F)).obj k'')
have h : ∀ (j j' : J) (f : j ⟶ j'),
  Eq (α := (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry (swap K J ⋙ F)).obj k'').map f) :
          (a : (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j)) →
            (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
              (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j, k'')))
            (y j) :
          (fun (X : Type v) ↦ X) (F.obj (j, k''))) :
      (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j') :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
Tactic: apply Limit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (((obj curry (swap K J ⋙ F)).obj k'').map f) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j)) →
              (fun (X : Type v) ↦ X) (((curry.obj (swap K J ⋙ F)).obj k'').obj j'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
                (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j, k'')))
              (y j) :
            (fun (X : Type v) ↦ X) (F.obj (j, k''))) :
        (fun (X : Type v) ↦ X) (((obj curry (swap K J ⋙ F)).obj k'').obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', k'')))
⊢ limit ((obj curry (swap K J ⋙ F)).obj k'')
have x₁ : (j : J) → ((obj curry (swap K J ⋙ F)).obj k'').obj j
Tactic: apply Limit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ Eq (α := F.obj (j', k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ 𝟙 k'')) : (a : F.obj (j, k'')) → F.obj (j', k''))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
              (a : F.obj (j, k j)) → F.obj (j, k''))
            (y j) :
          F.obj (j, k'')) :
      F.obj (j', k''))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
          (a : F.obj (j', k j')) → F.obj (j', k''))
        (y j') :
      F.obj (j', k''))
have h : Eq (α := F.obj (j', k''))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
        (a : F.obj (j, k j)) → F.obj (j', k''))
      (y j) :
    F.obj (j', k''))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
        (a : F.obj (j', k j')) → F.obj (j', k''))
      (y j') :
    F.obj (j', k''))
Tactic: simp only [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j) :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f ≫ i f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j) :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
have rw : Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', k'')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f ≫ i f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
      (y j) :
    (fun (X : Type v) ↦ X) (F.obj (j', k'')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f ≫ i f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
      (y j) :
    (fun (X : Type v) ↦ X) (F.obj (j', k'')))
Tactic: rw [s (𝟙 j) f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
x : limit (obj curry F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι ((obj curry F).obj j) (k j)) :
            (a : (fun (X : Type v) ↦ X) (((curry.obj F).obj j).obj (k j))) →
              (fun (X : Type v) ↦ X) (colimit ((curry.obj F).obj j)))
          (y j) :
        (fun (X : Type v) ↦ X) (colimit ((obj curry F).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (obj curry F ⋙ colim) j) :
            (a : (fun (X : Type v) ↦ X) (limit (curry.obj F ⋙ colim))) →
              (fun (X : Type v) ↦ X) ((curry.obj F ⋙ colim).obj j))
          x :
        (fun (X : Type v) ↦ X) ((obj curry F ⋙ colim).obj j))
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j') :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ×ₘ g j ≫ hf f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (j, k j))) → (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
          (y j) :
        (fun (X : Type v) ↦ X) (F.obj (j', kf f)))
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf f ≫ i f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j') :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
        (y j') :
      (fun (X : Type v) ↦ X) (F.obj (j', k'')))
have rw : Eq (α := (fun (X : Type v) ↦ X) (F.obj (j', k'')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ hf (𝟙 j') ≫ i (𝟙 j'))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
      (y j') :
    (fun (X : Type v) ↦ X) (F.obj (j', k'')))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (j', k j'))) → (fun (X : Type v) ↦ X) (F.obj (j', k'')))
      (y j') :
    (fun (X : Type v) ↦ X) (F.obj (j', k'')))
Tactic: rw [s f (𝟙 j'), ← s (𝟙 j') (𝟙 j')]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
⊢ IsIso (X := Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F))) (Y := (limit.cone (F ⋙ colim)).pt)
    (ConeMorphism.hom (colimitLimitToLimitColimitCone F) :
      Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F)) ⟶ (limit.cone (F ⋙ colim)).pt)
have suffices : IsIso (X := colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim)) (Y :=
  obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
  (CategoryStruct.comp (Y := limit (obj curry (obj uncurry F) ⋙ colim)) (colimitLimitToLimitColimit (obj uncurry F))
      (map lim (whiskerRight (Iso.inv (Iso.app (Equivalence.unitIso currying) F)) colim)) :
    colimit (obj curry (swap K J ⋙ obj uncurry F) ⋙ lim) ⟶
      obj lim (obj (𝟭 (J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v))) F ⋙ colim))
Tactic: suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (hypothesis)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F_1 : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
⊢ IsIso (C := Cone (F ⋙ colim)) (X := mapCone colim (limit.cone F)) (Y := limit.cone (F ⋙ colim))
    (colimitLimitToLimitColimitCone F : mapCone colim (limit.cone F) ⟶ limit.cone (F ⋙ colim))
have this : IsIso (X := Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F))) (Y := (limit.cone (F ⋙ colim)).pt)
  (ConeMorphism.hom (colimitLimitToLimitColimitCone F) :
    Cone.pt (F := F ⋙ colim) (mapCone colim (limit.cone F)) ⟶ (limit.cone (F ⋙ colim)).pt)
Tactic: have : IsIso (colimitLimitToLimitColimitCone F).hom := by
    suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J : Type u₁
K : Type u₂
inst : SmallCategory J
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J
F : J × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
⊢ PreservesFiniteLimits (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) colim
have h : ∀ (J : Type v₂) {𝒥 : SmallCategory J} (x : FinCategory J),
  PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v₂}
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
⊢ PreservesLimitsOfShape (C := Functor.{v₂, v, u₂, v + 1} K (Type v)) J colim
have h : {F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)} →
  {c : Cone F} → (hc : IsLimit c) → limit.cone (F ⋙ colim) ≅ mapCone colim c
Tactic: refine ⟨fun {F} => ⟨fun {c} hc => ⟨IsLimit.ofIsoLimit (limit.isLimit _) ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
⊢ limit.cone (F ⋙ colim) ≅ mapCone colim c
have h : mapCone colim c ≅ limit.cone (F ⋙ colim)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (goal)
Goal:
J_1 : Type u₁
K : Type u₂
inst : SmallCategory J_1
inst_1 : Category.{v₂, u₂} K
inst_2 : Small.{v, u₂} K
inst_3 : FinCategory J_1
F_1 : J_1 × K ⥤ Type v
inst_4 : IsFiltered.{v₂, u₂} K
J : Type v₂
𝒥 : SmallCategory J
x : FinCategory J
F : J ⥤ Functor.{v₂, v, u₂, v + 1} K (Type v)
c : Cone F
hc : IsLimit c
⊢ mapCone colim c ≅ limit.cone (F ⋙ colim)
have trans : Iso (C := Cone (F ⋙ colim)) (mapCone colim c) (mapCone colim (limit.cone F))
Tactic: trans colim.mapCone (limit.cone F)