awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cocone F
x : (X : C) → IsLimit (F := F.op ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c.op)
x_1 : C
⊢ (fun (h : IsColimit c) (x : C) ↦
        (isLimitOfPreserves (Functor.obj yoneda x) h.op :
          IsLimit (F := F.op ⋙ Functor.obj yoneda x) (Functor.mapCone (Functor.obj yoneda x) c.op)))
      ((fun (h : (X : C) → IsLimit (F := F.op ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c.op)) ↦
          (yonedaJointlyReflectsLimits F.op c.op h).unop)
        x)
      x_1 =
    x x_1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
X : Cᵒᵖ
s : (↑(F ⋙ Functor.obj coyoneda X).sections : Type (max v w))
x x_1 : J
f : x ⟶ x_1
⊢ Functor.map (Functor.obj (Functor.const J) (unop X)) f ≫ (↑s : (j : J) → (F ⋙ coyoneda.obj X).obj j) x_1 =
    (↑s : (j : J) → (F ⋙ coyoneda.obj X).obj j) x ≫ F.map f

Tactic:
simp [(s.property f).symm]

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
rw :
  ∀ s ∈ (F ⋙ Functor.obj coyoneda X).sections,
    ∃! x : Cone.pt (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c),
      ∀ (j : J),
        (hom (FC := TypeCat.Fun) (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda X) c)) j) :
              (a : (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj X).mapCone c).pt).obj j)) →
                (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj X).obj j))
            x =
          s j
⊢ Nonempty (IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c))

Tactic:
rw [Types.isLimit_iff]

Premises used: CategoryTheory.Limits.Types.isLimit_iff
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
s : (j : J) → (F ⋙ Functor.obj coyoneda X).obj j
hs : s ∈ (F ⋙ Functor.obj coyoneda X).sections
⊢ ∃! x : Cone.pt (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c),
    ∀ (j : J),
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda X) c)) j) :
            (a : (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj X).mapCone c).pt).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj X).obj j))
          x =
        s j

Tactic:
⟨hc.lift (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩), hc.fac _,
      hc.uniq (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩)⟩

Premises used: CategoryTheory.Limits.IsLimit.uniq, Subtype.mk, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Limits.IsLimit.lift, CategoryTheory.Limits.coneOfSectionCompCoyoneda, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
s : (j : J) → (F ⋙ Functor.obj coyoneda X).obj j
hs : s ∈ (F ⋙ Functor.obj coyoneda X).sections
⊢ ∃! x : Cone.pt (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c),
    ∀ (j : J),
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda X) c)) j) :
            (a : (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj X).mapCone c).pt).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj X).obj j))
          x =
        s j

Tactic:
exact ⟨hc.lift (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩), hc.fac _,
      hc.uniq (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩)⟩
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
j : J
⊢ (hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
          (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
            (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
        (𝟙 (unop (op s.pt))) ≫
      c.π.app j =
    s.π.app j

Tactic:
simpa using congr_hom ((hc (op s.pt)).fac
    ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 s.pt)

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Cone.pt, Opposite.op, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.mapCone, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
a :
  Eq (α := (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (op s.pt)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
        m :
      (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (op s.pt)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
        ((hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
            (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
              (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
          (𝟙 (unop (op s.pt)))) :
      (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
⊢ m =
    (hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
        (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
          (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
      (𝟙 (unop (op s.pt)))

Tactic:
apply (Types.isLimitEquivSections (hc (op s.pt))).injective

Premises used: CategoryTheory.Limits.Types.isLimitEquivSections, CategoryTheory.Limits.Cone.pt, Opposite.op, Equiv.injective
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
a :
  ∀ (j : J),
    Eq.{v + 1} (α := (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
      ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
                (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) →
                  (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
              m) :
          (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
        j)
      ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
                (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) →
                  (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
              ((hom (FC := TypeCat.Fun)
                    (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
                  (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
                    (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
                (𝟙 (unop (op s.pt))))) :
          (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
        j)
⊢ Eq (α := (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (op s.pt)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
        m :
      (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (op s.pt)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
        ((hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
            (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
              (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
          (𝟙 (unop (op s.pt)))) :
      (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
a :
  m ≫ c.π.app j =
    (@hom _ types TypeCat.Fun _ _ _ _ _
            (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
          (a : s.pt ⟶ s.pt) → s.pt ⟶ c.pt)
        (𝟙 s.pt) ≫
      c.π.app j
⊢ Eq.{v + 1} (α := (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
    ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
              (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
            m) :
        (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      j)
    ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
              (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
            ((hom (FC := TypeCat.Fun)
                  (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
                (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
                  (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
              (𝟙 (unop (op s.pt))))) :
        (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      j)

Tactic:
dsimp [Types.isLimitEquivSections, Types.sectionOfCone]

Premises used: CategoryTheory.Limits.Types.isLimitEquivSections, CategoryTheory.Limits.Types.sectionOfCone
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ Eq (α := (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
    ((hom (FC := TypeCat.Fun)
            (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s) ≫
              NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda (op s.pt)) c)) j) :
          (a : ((coyoneda.obj (op s.pt)).mapCone s).pt) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
        (𝟙 s.pt) :
      (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
    (((@hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) j) :
            TypeCat.Fun
              (Cone.pt (F := F ⋙ Functor.obj coyoneda (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s))
              ((F ⋙ Functor.obj coyoneda (op s.pt)).obj j)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone s).pt) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
        (𝟙 s.pt) :
      (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)

Tactic:
have eq := congr_hom ((hc (op s.pt)).fac ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 s.pt)
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
x : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
h :
  ∀ (x_1 : Cᵒᵖ),
    (fun (h : IsLimit c) (x : Cᵒᵖ) ↦
          (isLimitOfPreserves (Functor.obj coyoneda x) h :
            IsLimit (F := F ⋙ Functor.obj coyoneda x) (Functor.mapCone (Functor.obj coyoneda x) c)))
        ((fun (h : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)) ↦
            coyonedaJointlyReflectsLimits F c h)
          x)
        x_1 =
      x x_1
⊢ (fun (h : IsLimit c) (x : Cᵒᵖ) ↦
        (isLimitOfPreserves (Functor.obj coyoneda x) h :
          IsLimit (F := F ⋙ Functor.obj coyoneda x) (Functor.mapCone (Functor.obj coyoneda x) c)))
      ((fun (h : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)) ↦
          coyonedaJointlyReflectsLimits F c h)
        x) =
    x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
x : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
x_1 : Cᵒᵖ
⊢ (fun (h : IsLimit c) (x : Cᵒᵖ) ↦
        (isLimitOfPreserves (Functor.obj coyoneda x) h :
          IsLimit (F := F ⋙ Functor.obj coyoneda x) (Functor.mapCone (Functor.obj coyoneda x) c)))
      ((fun (h : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)) ↦
          coyonedaJointlyReflectsLimits F c h)
        x)
      x_1 =
    x x_1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
x : ∀ (k : Cᵒᵖ), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ Functor.obj (evaluation Cᵒᵖ (Type v)) k)
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} (C := C) yoneda

Tactic:
apply preservesLimits_of_evaluation

Premises used: CategoryTheory.Limits.preservesLimits_of_evaluation
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : Cᵒᵖ
x : PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (Functor.obj coyoneda K)
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ Functor.obj (evaluation Cᵒᵖ (Type v)) K)

Tactic:
change PreservesLimitsOfSize (coyoneda.obj K)

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.PreservesLimitsOfSize, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (Functor.obj coyoneda K)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
x : ∀ (k : C), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ Functor.obj (evaluation C (Type v)) k)
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} (C := Cᵒᵖ) coyoneda

Tactic:
apply preservesLimits_of_evaluation

Premises used: CategoryTheory.Limits.preservesLimits_of_evaluation
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : C
x : PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (Functor.obj yoneda K)
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ Functor.obj (evaluation C (Type v)) K)

Tactic:
change PreservesLimitsOfSize (yoneda.obj K)

Premises used: CategoryTheory.yoneda, CategoryTheory.Limits.PreservesLimitsOfSize, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (Functor.obj yoneda K)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
⊢ ReflectsLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} (C := C) yoneda

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
⊢ ReflectsLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} (C := Cᵒᵖ) coyoneda

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
x :
  ∀ (k : Cᵒᵖ),
    PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
      (uliftYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type (max w' v))) k)
⊢ PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)} (C := C) uliftYoneda.{w', v, u}

Tactic:
apply preservesLimits_of_evaluation

Premises used: CategoryTheory.Limits.preservesLimits_of_evaluation
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : Cᵒᵖ
x : PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (Functor.obj coyoneda K ⋙ uliftFunctor.{w', v})
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type (max w' v))) K)

Tactic:
change PreservesLimitsOfSize.{t, w} (coyoneda.obj K ⋙ uliftFunctor.{w'})
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (Functor.obj coyoneda K ⋙ uliftFunctor.{w', v})

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
x :
  ∀ (k : C),
    PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
      (uliftCoyoneda.{w', v, u} ⋙ Functor.obj (evaluation C (Type (max w' v))) k)
⊢ PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)} (C := Cᵒᵖ) uliftCoyoneda.{w', v, u}

Tactic:
apply preservesLimits_of_evaluation

Premises used: CategoryTheory.Limits.preservesLimits_of_evaluation
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : C
x : PreservesLimitsOfSize.{t, w, v, max w' v, u, max (w' + 1) (v + 1)} (Functor.obj yoneda K ⋙ uliftFunctor.{w', v})
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftCoyoneda.{w', v, u} ⋙ Functor.obj (evaluation C (Type (max w' v))) K)

Tactic:
change PreservesLimitsOfSize.{t, w} (yoneda.obj _ ⋙ uliftFunctor.{w'})
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, max w' v, u, max (w' + 1) (v + 1)} (Functor.obj yoneda K ⋙ uliftFunctor.{w', v})

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
K : Cᵒᵖ
J : Type w
x : Category.{t, w} J
⊢ PreservesLimitsOfShape J ((shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K) ⋙ uliftFunctor.{v, w'})

Tactic:
have := preservesLimitsOfShape_of_natIso (J := J) (Functor.associator _ _ _ ≪≫
      shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor.{w'} K).symm
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
K : Cᵒᵖ
J : Type w
x : Category.{t, w} J
this :
  PreservesLimitsOfShape J ((shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K) ⋙ uliftFunctor.{v, w'})
⊢ PreservesLimitsOfShape.{t, w, v, w', u, w' + 1} J (shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K)

Tactic:
preservesLimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{v}

Premises used: CategoryTheory.uliftFunctor, CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
K : Cᵒᵖ
J : Type w
x : Category.{t, w} J
this :
  PreservesLimitsOfShape J ((shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K) ⋙ uliftFunctor.{v, w'})
⊢ PreservesLimitsOfShape.{t, w, v, w', u, w' + 1} J (shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K)

Tactic:
exact preservesLimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{v}
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
inst_1 : F.IsRepresentable
suffices : PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (F ⋙ uliftFunctor.{v, w'})
⊢ PreservesLimitsOfSize.{t, w, v, w', u, w' + 1} F

Tactic:
suffices PreservesLimitsOfSize (F ⋙ uliftFunctor.{v}) from
    preservesLimits_of_reflects_of_preserves _ (uliftFunctor.{v})
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
inst_1 : F.IsRepresentable
rw :
  PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (obj uliftYoneda.{w', v, u} (F ⋙ uliftFunctor.{v, w'}).reprX)
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (F ⋙ uliftFunctor.{v, w'})

Tactic:
rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso.symm]
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
inst_1 : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (obj uliftYoneda.{w', v, u} (F ⋙ uliftFunctor.{v, w'}).reprX)

Tactic:
inferInstanceAs <| PreservesLimitsOfSize (yoneda.obj _ ⋙ uliftFunctor)

Premises used: _private.0.CategoryTheory.Functor.instPreservesLimitsOfSizeOpposite._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
inst_1 : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (obj uliftYoneda.{w', v, u} (F ⋙ uliftFunctor.{v, w'}).reprX)

Tactic:
exact inferInstanceAs <| PreservesLimitsOfSize (yoneda.obj _ ⋙ uliftFunctor)
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_1 : F.IsCorepresentable
suffices : PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)} (F ⋙ uliftFunctor.{v, u_1})
⊢ PreservesLimitsOfSize.{t, w, v, u_1, u, u_1 + 1} F

Tactic:
suffices PreservesLimitsOfSize (F ⋙ uliftFunctor.{v}) from
    preservesLimits_of_reflects_of_preserves _ (uliftFunctor.{v})
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_1 : F.IsCorepresentable
rw :
  PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
    (obj uliftCoyoneda.{u_1, v, u} (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)} (F ⋙ uliftFunctor.{v, u_1})

Tactic:
rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftCoyonedaCoreprXIso.symm]
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_1 : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
    (obj uliftCoyoneda.{u_1, v, u} (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))

Tactic:
inferInstanceAs <| PreservesLimitsOfSize (coyoneda.obj _ ⋙ uliftFunctor)

Premises used: _private.0.CategoryTheory.Functor.instPreservesLimitsOfSize._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Yoneda
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_1 : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
    (obj uliftCoyoneda.{u_1, v, u} (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))

Tactic:
exact inferInstanceAs <| PreservesLimitsOfSize (coyoneda.obj _ ⋙ uliftFunctor)
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X _Y _Z : C
r : ℕ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
(Preadditive.rightComp X g).map_nsmul r f

Premises used: AddMonoidHom.map_nsmul, CategoryTheory.Preadditive.rightComp