mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ (s.pt.map f ≫ (t Y).lift { pt := s.pt.obj Y, π := whiskerRight s.π ((evaluation K C).obj Y) }) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j =
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π ((evaluation K C).obj X) } ≫ c.pt.map f) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w', v, u} C
K : Cᵒᵖ
J : Type w
x✝ : Category.{t, w} J
⊢ PreservesLimitsOfShape J (shrinkYoneda.{w', v, u} ⋙ (evaluation Cᵒᵖ (Type w')).obj K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesLimitsOfShape J F
K : J' ⥤ C
c : Cone (K ⋙ F)
hc : IsLimit c
⊢ LiftableCone K F c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w'
inst✝ : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, w', u, w' + 1} F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
j : J
⊢ { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ } ≫
      c.π.app j =
    s.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m =
    { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type u_1
inst✝ : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, u_1, u, u_1 + 1} F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → LimitCone (F.flip.obj k)
k : K
j : J
⊢ (c k).isLimit.lift { pt := (c k).cone.pt, π := (c k).cone.π ≫ F.flip.map (𝟙 k) } ≫ (c k).cone.π.app j =
    𝟙 (c k).cone.pt ≫ (c k).cone.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ Small.{v, max v w} ↑(G ⋙ forget C).sections

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
⊢ Function.Injective fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → LimitCone (F.flip.obj k)
k₁ k₂ k₃ : K
f₁ : k₁ ⟶ k₂
f₂ : k₂ ⟶ k₃
j : J
⊢ (c k₃).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map (f₁ ≫ f₂) } ≫ (c k₃).cone.π.app j =
    ((c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f₁ } ≫
        (c k₃).isLimit.lift { pt := (c k₂).cone.pt, π := (c k₂).cone.π ≫ F.flip.map f₂ }) ≫
      (c k₃).cone.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  (IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ ((Cocone.precompose (isoWhiskerRight h F).inv).obj ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).ι.app j ≫
      (Iso.refl
          ((Cocone.precompose (isoWhiskerRight h F).inv).obj
              ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).pt).hom =
    c.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
⊢ ((const J).obj
            { obj := fun k ↦ (c k).cone.pt,
              map := fun {k₁ k₂} f ↦ (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f },
              map_id := ⋯, map_comp := ⋯ }).map
        g ≫
      { app := fun k ↦ (c k).cone.π.app j₂, naturality := ⋯ } =
    { app := fun k ↦ (c k).cone.π.app j₁, naturality := ⋯ } ≫ F.map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ G.mapCocone (liftColimit ((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm t)) ≅ c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
⊢ let ff := fun a ↦ (ConcreteCategory.hom (D.ι.app a.fst)) a.snd;
  Function.Surjective ff

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
x : ToType D.pt
⊢ ∃ j y, (ConcreteCategory.hom (D.ι.app j)) y = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesColimitsOfShape J F
K : J' ⥤ C
c : Cocone (K ⋙ F)
hc : IsColimit c
⊢ LiftableCocone K F c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
⊢ LiftableCone K (F ⋙ G) c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      c.pt.map f ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) } =
    (((evaluation K C).obj X).mapCocone c).ι.app j ≫
      (t X).desc { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) } ≫ s.pt.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) },
        naturality := ⋯ } =
    s.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m =
    { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) }, naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → ColimitCocone (F.flip.obj k)
k : K
j : J
⊢ (c k).cocone.ι.app j ≫ (c k).isColimit.desc { pt := (c k).cocone.pt, ι := F.flip.map (𝟙 k) ≫ (c k).cocone.ι } =
    (c k).cocone.ι.app j ≫ 𝟙 (c k).cocone.pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → ColimitCocone (F.flip.obj k)
k₁ k₂ k₃ : K
f₁ : k₁ ⟶ k₂
f₂ : k₂ ⟶ k₃
j : J
⊢ (c k₁).cocone.ι.app j ≫
      (c k₁).isColimit.desc { pt := (c k₃).cocone.pt, ι := F.flip.map (f₁ ≫ f₂) ≫ (c k₃).cocone.ι } =
    (c k₁).cocone.ι.app j ≫
      (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f₁ ≫ (c k₂).cocone.ι } ≫
        (c k₂).isColimit.desc { pt := (c k₃).cocone.pt, ι := F.flip.map f₂ ≫ (c k₃).cocone.ι }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
h : ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
⊢ F.map g ≫ { app := fun k ↦ (c k).cocone.ι.app j₂, naturality := ⋯ } =
    { app := fun k ↦ (c k).cocone.ι.app j₁, naturality := ⋯ } ≫
      ((const J).obj
            { obj := fun k ↦ (c k).cocone.pt,
              map := fun {k₁ k₂} f ↦
                (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι },
              map_id := ⋯, map_comp := ⋯ }).map
        g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ { app := fun Y_1 ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := ⋯ } =
    { app := fun Y ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ ((const J).obj (F.flip ⋙ colim)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
x : ToType D.pt
k : J
⊢ ∃ j x_1 y, (ConcreteCategory.hom (D.ι.app j)) y = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
⊢ IsColimit (pointwiseCocone F)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable

Goal state before:
pp: G : Type u
inst✝ : AddCommGroup G
x y : G
⊢ (uliftZMultiplesHom G) (x + y) = (uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation F k).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j = (limit.π F j).app k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
x✝ : Cᵒᵖ
⊢ Small.{w, v} ((yoneda.obj X).obj x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj X).map g)) (shrinkYonedaObjObjEquiv.symm f) =
    shrinkYonedaObjObjEquiv.symm (g.unop ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation F k).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X X' : C
Y : Cᵒᵖ
f : unop Y ⟶ X
g : X ⟶ X'
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map g).app Y)) (shrinkYonedaObjObjEquiv.symm f) =
    shrinkYonedaObjObjEquiv.symm (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X X' : C
Y : Cᵒᵖ
f : (shrinkYoneda.{w, v, u}.obj X).obj Y
g : X ⟶ X'
⊢ shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map g).app Y)) f) =
    shrinkYonedaObjObjEquiv f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : (shrinkYoneda.{w, v, u}.obj X).obj Y
⊢ shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj X).map g)) f) =
    g.unop ≫ shrinkYonedaObjObjEquiv f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
x : P.obj (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ ((shrinkYoneda.{w, v, u}.obj X).map g ≫
      ↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Z)).symm f)))) x) =
    (↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x) ≫ P.map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limitObjIsoLimitCompEvaluation F i).inv ≫ (limit F).map f =
    limMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (limitObjIsoLimitCompEvaluation F j).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
τ : shrinkYoneda.{w, v, u}.obj X ⟶ P
⊢ (fun x ↦
        {
          app := fun Y ↦
            ↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x,
          naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) ((equivShrink ((yoneda.obj X).obj (op X))) (𝟙 X))) τ) =
    τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
x : P.obj (op X)
⊢ (fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) ((equivShrink ((yoneda.obj X).obj (op X))) (𝟙 X)))
      ((fun x ↦
          {
            app := fun Y ↦
              ↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x,
            naturality := ⋯ })
        x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
⊢ (limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ G.whiskerLeft (limit.π F j) =
    limit.π (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
P : Cᵒᵖ ⥤ Type w
f : shrinkYoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.op)) (shrinkYonedaEquiv f) =
    (ConcreteCategory.hom (f.app (op Y))) (shrinkYonedaObjObjEquiv.symm g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
⊢ shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f) = shrinkYonedaObjObjEquiv.symm f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
⊢ (limitCompWhiskeringLeftIsoCompLimit F G).inv ≫ limit.π (F ⋙ (whiskeringLeft D K C).obj G) j =
    G.whiskerLeft (limit.π F j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P Q : Cᵒᵖ ⥤ Type w
α : shrinkYoneda.{w, v, u}.obj X ⟶ P
β : P ⟶ Q
⊢ shrinkYonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app (op X))) (shrinkYonedaEquiv α)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation F k).inv = (colimit.ι F j).app k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
P : Cᵒᵖ ⥤ Type w
f : shrinkYoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.op)) (shrinkYonedaEquiv f) = shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map g ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (colimit.ι F j).app k ≫ (colimitObjIsoColimitCompEvaluation F k).hom = colimit.ι (F ⋙ (evaluation K C).obj k) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Cᵒᵖ ⥤ Type w
t : P.obj X
⊢ shrinkYonedaEquiv (shrinkYonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) =
    shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f.unop ≫ shrinkYonedaEquiv.symm t)

Tactic:
by

Goal state after: