awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
e : j ⟶ k
⊢ Eq (α := (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).left ⟶ (F.obj k).left)
    (Over.Hom.left
      (Functor.map (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) e ≫
        (fun (j : J) ↦
            (Over.homMk (s.π.app j) ⋯ :
              Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj j))
          k))
    (Over.Hom.left
      ((fun (j : J) ↦
            (Over.homMk (s.π.app j) ⋯ :
              Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j ⟶ F.obj j))
          j ≫
        F.map e))

Tactic:
simpa using (s.w e).symm

Premises used: CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun (j : J) ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
⊢ ∃! l : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c),
    ∀ (j : J), l ≫ NatTrans.app (Cone.π (Functor.mapCone (Over.forget X) c)) j = s.π.app j

Tactic:
⟨(hc.lift s').left, fun j ↦ congr($(hc.fac s' j).left), fun f hf ↦ ?_⟩

Premises used: congrArg, CategoryTheory.Over.Hom.left, id, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun (j : J) ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
refine :
  ∀ (f : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c))
    (hf :
      (fun (l : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c)) ↦
          ∀ (j : J), l ≫ NatTrans.app (Cone.π (Functor.mapCone (Over.forget X) c)) j = s.π.app j)
        f),
    f = Over.Hom.left (hc.lift s')
⊢ ∃! l : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c),
    ∀ (j : J), l ≫ NatTrans.app (Cone.π (Functor.mapCone (Over.forget X) c)) j = s.π.app j

Tactic:
refine ⟨(hc.lift s').left, fun j ↦ congr($(hc.fac s' j).left), fun f hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun (j : J) ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
f : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c)
hf : ∀ (j : J), f ≫ Over.Hom.left (c.π.app j) = s.π.app j
⊢ f ≫ c.pt.hom = s'.pt.hom

Tactic:
simp [s', ← hf]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered.{u_2, u_3} J
F : J ⥤ Over.{v_1, u_1} X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun (j : J) ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
f : s.pt ⟶ Cone.pt (F := F ⋙ Over.forget X) (Functor.mapCone (Over.forget X) c)
hf : ∀ (j : J), f ≫ Over.Hom.left (c.π.app j) = s.π.app j
⊢ f = Over.Hom.left (hc.lift s')

Tactic:
exact congr($(hc.uniq s' (Over.homMk f (by simp [s', ← hf]))
    fun j ↦ Over.OverMorphism.ext (hf j)).left)
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (C := Under.{v_1, u_1} X) (Under.forget X)

Tactic:
⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩

Premises used: CategoryTheory.Limits.IsColimit.ofExistsUnique, CategoryTheory.Limits.PreservesFilteredColimitsOfSize.mk, Nonempty.intro, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
refine :
  ∀ (J : Type u_3) (hJ : Category.{u_2, u_3} J) (hJ' : IsFiltered.{u_2, u_3} J) {F : J ⥤ Under.{v_1, u_1} X}
    {c : Cocone F} (hc : IsColimit c) (s : Cocone (F ⋙ Under.forget X)),
    ∃! d : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt,
      ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget X) c)) j ≫ d = s.ι.app j
⊢ PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (C := Under.{v_1, u_1} X) (Under.forget X)

Tactic:
refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
obtain :
  ∀ (i : J),
    ∃! d : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt,
      ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget X) c)) j ≫ d = s.ι.app j
⊢ ∃! d : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt,
    ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget X) c)) j ≫ d = s.ι.app j

Tactic:
obtain i := Nonempty.some ((inferInstance : Nonempty J))

Premises used: inferInstance, Nonempty.some
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j : J
obtain :
  ∀ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k),
    (F.obj j).hom ≫ s.ι.app j =
      (Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j).hom
⊢ (F.obj j).hom ≫ s.ι.app j = (Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j).hom

Tactic:
obtain ⟨k, hik, hjk, -⟩ := IsFilteredOrEmpty.cocone_objs i j

Premises used: CategoryTheory.IsFilteredOrEmpty.cocone_objs
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
hik : i ⟶ k
hjk : j ⟶ k
simp :
  (F.obj j).hom ≫ (F ⋙ Under.forget X).map hjk ≫ s.ι.app k = (F.obj i).hom ≫ (F ⋙ Under.forget X).map hik ≫ s.ι.app k
⊢ (F.obj j).hom ≫ s.ι.app j = (Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j).hom

Tactic:
simp only [Functor.const_obj_obj, Under.mk_right, Under.mk_hom,
      ← s.w hjk, ← s.w hik]

Premises used: CategoryTheory.Under.mk_hom, CategoryTheory.Limits.Cocone.w, CategoryTheory.Under.mk_right, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
hik : i ⟶ k
hjk : j ⟶ k
⊢ (F.obj j).hom ≫ (F ⋙ Under.forget X).map hjk ≫ s.ι.app k = (F.obj i).hom ≫ (F ⋙ Under.forget X).map hik ≫ s.ι.app k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
e : j ⟶ k
h :
  Eq (α :=
    (F.obj j).right ⟶ (Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) k).right)
    (Under.Hom.right
      (F.map e ≫
        (fun (j : J) ↦
            (Under.homMk (s.ι.app j) ⋯ :
              F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j))
          k))
    (Under.Hom.right
      ((fun (j : J) ↦
            (Under.homMk (s.ι.app j) ⋯ :
              F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j))
          j ≫
        Functor.map (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) e))
⊢ Eq (α := F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) k)
    (F.map e ≫
      (fun (j : J) ↦
          (Under.homMk (s.ι.app j) ⋯ :
            F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j))
        k)
    ((fun (j : J) ↦
          (Under.homMk (s.ι.app j) ⋯ :
            F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j))
        j ≫
      Functor.map (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) e)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
e : j ⟶ k
⊢ Eq (α :=
    (F.obj j).right ⟶ (Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) k).right)
    (Under.Hom.right
      (F.map e ≫
        (fun (j : J) ↦
            (Under.homMk (s.ι.app j) ⋯ :
              F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j))
          k))
    (Under.Hom.right
      ((fun (j : J) ↦
            (Under.homMk (s.ι.app j) ⋯ :
              F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j))
          j ≫
        Functor.map (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) e))

Tactic:
simpa using s.w e

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i),
    ι := { app := fun (j : J) ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
⊢ ∃! d : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt,
    ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget X) c)) j ≫ d = s.ι.app j

Tactic:
⟨(hc.desc s').right, fun j ↦ congr($(hc.fac s' j).right), fun f hf ↦ ?_⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, congrArg, id, CategoryTheory.Limits.IsColimit.desc, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Under.Hom.right
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i),
    ι := { app := fun (j : J) ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
refine :
  ∀ (f : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt)
    (hf :
      (fun (d : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt) ↦
          ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget X) c)) j ≫ d = s.ι.app j)
        f),
    f = Under.Hom.right (hc.desc s')
⊢ ∃! d : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt,
    ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget X) c)) j ≫ d = s.ι.app j

Tactic:
refine ⟨(hc.desc s').right, fun j ↦ congr($(hc.fac s' j).right), fun f hf ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i),
    ι := { app := fun (j : J) ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
f : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt
hf : ∀ (j : J), Under.Hom.right (c.ι.app j) ≫ f = s.ι.app j
⊢ c.pt.hom ≫ f = s'.pt.hom

Tactic:
simp [s', ← hf]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered.{u_2, u_3} J
F : J ⥤ Under.{v_1, u_1} X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i),
    ι := { app := fun (j : J) ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
f : Cocone.pt (F := F ⋙ Under.forget X) (Functor.mapCocone (Under.forget X) c) ⟶ s.pt
hf : ∀ (j : J), Under.Hom.right (c.ι.app j) ≫ f = s.ι.app j
⊢ f = Under.Hom.right (hc.desc s')

Tactic:
exact congr($(hc.uniq s' (Under.homMk f (by simp [s', ← hf]))
    fun j ↦ Under.UnderMorphism.ext (hf j)).right)
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : PreservesFiniteLimits A
suffices : IsCofiltered A.Elements
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
suffices IsCofiltered A.Elements from
    IsFiltered.of_equivalence (CategoryOfElements.costructuredArrowYonedaEquivalence _)
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : PreservesFiniteLimits A
suffices : HasFiniteLimits A.Elements
⊢ IsCofiltered A.Elements

Tactic:
suffices HasFiniteLimits A.Elements from IsCofiltered.of_hasFiniteLimits A.Elements
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : PreservesFiniteLimits A
⊢ HasFiniteLimits A.Elements

Tactic:
⟨fun J _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : PreservesFiniteLimits A
⊢ HasFiniteLimits A.Elements

Tactic:
exact ⟨fun J _ _ => inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ Eq (α := obj (obj yoneda i.left) (limit K) ⟶ A.obj (K.obj j))
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)) (i.hom.app (limit K) ≫ A.map (limit.π K j))

Tactic:
have := i.hom.naturality (limit.π K j)
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this :
  Eq (α := (Opposite.unop (limit K) ⟶ i.left) ⟶ A.obj (K.obj j))
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)) (i.hom.app (limit K) ≫ A.map (limit.π K j))
rw :
  Eq (α := obj ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i ⟶ (K ⋙ A).obj j)
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j))
    (NatTrans.app
        (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K)))) i ≫
      CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
        ((fun (X : CostructuredArrow yoneda A) ↦
            (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
              (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
          i)
        (NatTrans.app
            (Functor.map
              (coyoneda ⋙
                obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
              (limit.π K j))
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j))
⊢ Eq (α := obj ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i ⟶ (K ⋙ A).obj j)
    (i.hom.app (limit K) ≫ A.map (limit.π K j))
    (NatTrans.app
        (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K)))) i ≫
      CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
        ((fun (X : CostructuredArrow yoneda A) ↦
            (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
              (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
          i)
        (NatTrans.app
            (Functor.map
              (coyoneda ⋙
                obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
              (limit.π K j))
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j))

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this :
  Eq (α := (Opposite.unop (limit K) ⟶ i.left) ⟶ A.obj (K.obj j))
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)) (i.hom.app (limit K) ≫ A.map (limit.π K j))
h :
  ∀ (x : Opposite.unop (limit K) ⟶ i.left),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)))
        x =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (NatTrans.app
              (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K))))
              i ≫
            CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
              ((fun (X : CostructuredArrow yoneda A) ↦
                  (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
                    (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
                i)
              (NatTrans.app
                  (Functor.map
                    (coyoneda ⋙
                      obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
                    (limit.π K j))
                  i ≫
                ((functorToInterchangeIso A K).inv.app j).app i ≫
                  ((flipFunctorToInterchange A K).hom.app i).app j ≫
                    (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j)))
        x
⊢ Eq (α := obj ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ obj (evaluation Cᵒᵖ (Type u)) (limit K)) i ⟶ (K ⋙ A).obj j)
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j))
    (NatTrans.app
        (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K)))) i ≫
      CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
        ((fun (X : CostructuredArrow yoneda A) ↦
            (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
              (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
          i)
        (NatTrans.app
            (Functor.map
              (coyoneda ⋙
                obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
              (limit.π K j))
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this :
  Eq (α := (Opposite.unop (limit K) ⟶ i.left) ⟶ A.obj (K.obj j))
    (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)) (i.hom.app (limit K) ≫ A.map (limit.π K j))
x : Opposite.unop (limit K) ⟶ i.left
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (obj yoneda i.left) (limit.π K j) ≫ i.hom.app (K.obj j)))
      x =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app
            (Iso.hom (associator (CostructuredArrow.proj yoneda A) yoneda (obj (evaluation Cᵒᵖ (Type u)) (limit K))))
            i ≫
          CategoryStruct.comp (Y := obj (CostructuredArrow.proj yoneda A ⋙ obj coyoneda (limit K)) i)
            ((fun (X : CostructuredArrow yoneda A) ↦
                (𝟙 (Opposite.unop (limit K) ⟶ X.left) :
                  (Opposite.unop (limit K) ⟶ X.left) ⟶ Opposite.unop (limit K) ⟶ X.left))
              i)
            (NatTrans.app
                (Functor.map
                  (coyoneda ⋙
                    obj (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)) (CostructuredArrow.proj yoneda A))
                  (limit.π K j))
                i ≫
              ((functorToInterchangeIso A K).inv.app j).app i ≫
                ((flipFunctorToInterchange A K).hom.app i).app j ≫
                  (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j)))
      x

Tactic:
simp [flipFunctorToInterchange, functorToInterchangeIso, functorToInterchange]

Premises used: CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchangeIso, CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst_2 : SmallCategory J
inst_3 : FinCategory J
K : J ⥤ Cᵒᵖ
inst_4 : IsFiltered.{u, u} (CostructuredArrow yoneda A)
⊢ IsIso (X := A.obj (limit K)) (Y := limit (K ⋙ A)) (limit.post K A)

Tactic:
iso_hom A K ▸ inferInstance

Premises used: CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom, Eq.rec, inferInstance