awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x)) F.rightOp
have inst : PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesLimitsOfShape_rightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x)) F.unop
have inst : PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesLimitsOfShape_unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.op
have inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesColimitsOfShape_op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.leftOp
have inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesColimitsOfShape_leftOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.rightOp
have inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesColimitsOfShape_rightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : PreservesFiniteProducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x)) F.unop
have inst : PreservesLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesColimitsOfShape_unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteCoproducts F
n : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin n)) F.op
have inst : ReflectsColimitsOfShape (Discrete (Fin n))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsLimitsOfShape_op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x)) F.leftOp
have inst : ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsLimitsOfShape_leftOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x)) F.rightOp
have inst : ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsLimitsOfShape_rightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteCoproducts F
x : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x)) F.unop
have inst : ReflectsColimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsLimitsOfShape_unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.op
have inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsColimitsOfShape_op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.leftOp
have inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsColimitsOfShape_leftOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.rightOp
have inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsColimitsOfShape_rightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (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 : ReflectsFiniteProducts F
x : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x)) F.unop
have inst : ReflectsLimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures reflectsColimitsOfShape_unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (C := Over.{v_1, u_1} X) (Over.forget X)
have refine : ∀ (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)),
  ∃! 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 ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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)
⊢ ∃! 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
have obtain : ∀ (i : J),
  ∃! 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: obtain i := Nonempty.some ((inferInstance : Nonempty J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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 : J
⊢ s.π.app j ≫ (F.obj j).hom = (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).hom
have obtain : ∀ (k : J) (hik : k ⟶ i) (hjk : k ⟶ j),
  s.π.app j ≫ (F.obj j).hom = (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).hom
Tactic: obtain ⟨k, hik, hjk, -⟩ := IsCofilteredOrEmpty.cone_objs i j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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
hik : k ⟶ i
hjk : k ⟶ j
⊢ s.π.app j ≫ (F.obj j).hom = (Functor.obj (Functor.obj (Functor.const J) (Over.mk (s.π.app i ≫ (F.obj i).hom))) j).hom
have simp : (s.π.app k ≫ (F ⋙ Over.forget X).map hjk) ≫ (F.obj j).hom = (s.π.app k ≫ (F ⋙ Over.forget X).map hik) ≫ (F.obj i).hom
Tactic: simp only [Functor.const_obj_obj, Over.mk_left, Over.mk_hom,
      ← s.w hjk, ← s.w hik]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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 ⟶ F.obj k)
    (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)
    ((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)
have h : 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) sorry :
            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) sorry :
            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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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
have 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')
Tactic: refine ⟨(hc.lift s').left, fun j ↦ congr($(hc.fac s' j).left), fun f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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)
have 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
Tactic: refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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)
⊢ ∃! 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
have 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
Tactic: obtain i := Nonempty.some ((inferInstance : Nonempty J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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
⊢ (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
have 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
Tactic: obtain ⟨k, hik, hjk, -⟩ := IsFilteredOrEmpty.cocone_objs i j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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 ≫ s.ι.app j = (Functor.obj (Functor.obj (Functor.const J) (Under.mk ((F.obj i).hom ≫ s.ι.app i))) j).hom
have 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
Tactic: simp only [Functor.const_obj_obj, Under.mk_right, Under.mk_hom,
      ← s.w hjk, ← s.w hik]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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 ⟶ 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)
have 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) sorry :
            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) sorry :
            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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Over (goal)
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
have 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')
Tactic: refine ⟨(hc.desc s').right, fun j ↦ congr($(hc.fac s' j).right), fun f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Presheaf (goal)
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
⊢ IsFiltered (CostructuredArrow yoneda A)
have suffices : IsCofiltered A.Elements
Tactic: suffices IsCofiltered A.Elements from
    IsFiltered.of_equivalence (CategoryOfElements.costructuredArrowYonedaEquivalence _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Presheaf (goal)
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
⊢ IsCofiltered A.Elements
have suffices : HasFiniteLimits A.Elements
Tactic: suffices HasFiniteLimits A.Elements from IsCofiltered.of_hasFiniteLimits A.Elements
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Presheaf (hypothesis)
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 ((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))
have this : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Presheaf (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← this]