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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f =
      colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫
        ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f ≫ (preservesColimitIso G Y✝).inv

Tactic:
intro j

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f =
    colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫
      ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f ≫ (preservesColimitIso G Y✝).inv
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
⊢ (descMonoidHom t) 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
⊢ ∀ (X : B × C), (uncurry.obj (curry.obj F)).obj X = F.obj X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B ⥤ C ⥤ D
x✝ : B
⊢ ∀ (X : C), ((curry.obj (uncurry.obj F)).obj x✝).obj X = (F.obj x✝).obj X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B ⥤ C ⥤ D
x✝ : B
⊢ ∀ (X Y : C) (f : X ⟶ Y), ((curry.obj (uncurry.obj F)).obj x✝).map f = eqToHom ⋯ ≫ (F.obj x✝).map f ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z z' : M₂
⊢ ((MultilinearMap.mkPiRing R ι (z + z')) fun x ↦ 1) =
    (MultilinearMap.mkPiRing R ι z + MultilinearMap.mkPiRing R ι z') fun x ↦ 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
inst✝ : Fintype ι
c : R
z : M₂
⊢ ((MultilinearMap.mkPiRing R ι (c • z)) fun x ↦ 1) = ((RingHom.id R) c • MultilinearMap.mkPiRing R ι z) fun x ↦ 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
⊢ ∀ (X : B × D), (uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip).obj X = (F₁.prod F₂ ⋙ G).obj X

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z : M₂
⊢ (fun f ↦ f fun x ↦ 1) ((fun z ↦ MultilinearMap.mkPiRing R ι z) z) = z

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
⊢ ∀ (X : B × D), (uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip)).obj X = (F₁.prod F₂ ⋙ G).obj X

Tactic:
simp

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 : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ F.map ((liftLimit t).π.app j) = (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j

Tactic:
simp

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 : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ((liftedLimitMapsToOriginal t).inv ≫ (liftedLimitMapsToOriginal t).hom).hom ≫ c.π.app j = c.π.app j

Tactic:
simp

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 : J ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ (F.mapCocone { pt := X, ι := { app := fun j ↦ F.preimage (l.ι.app j ≫ i.inv), naturality := ⋯ } }).ι.app j ≫ i.hom =
    l.ι.app j

Tactic:
simp

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✝ : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ c.π.app j ≫ F.map (h.inv.app j ≫ h.hom.app j) = 𝟙 c.pt ≫ c.π.app j

Tactic:
simp

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:
simp

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:
simp

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
⊢ (F.map (h.inv.app j ≫ h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j

Tactic:
simp

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
⊢ (F.obj j).map f ≫ { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) }.ι.app j =
    { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) }.ι.app j ≫ s.pt.map f

Tactic:
simp

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:
simp

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:
simp

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
k j : J
y : ToType (F.obj j)
⊢ ConcreteCategory.hom (F.map (IsFiltered.rightToMax k j) ≫ D.ι.app (IsFiltered.max k j)) =
    ConcreteCategory.hom (D.ι.app j)

Tactic:
simp

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
⊢ (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j = (limit.π F j).app k

Tactic:
simp

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
⊢ (limit.π F j).app k = (preservesLimitIso ((evaluation K C).obj k) F).hom ≫ limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
simp

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
j✝ : J
⊢ ((limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom) ≫ limit.π (F ⋙ (evaluation K C).obj j) j✝ =
    ((limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))) ≫
      limit.π (F ⋙ (evaluation K C).obj j) j✝

Tactic:
simp

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:
simp

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 ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv =
    (colimit.ι F j).app k

Tactic:
simp

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 =
    colimit.ι (F ⋙ (evaluation K C).obj k) j ≫ (preservesColimitIso ((evaluation K C).obj k) F).inv

Tactic:
simp

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 : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P
⊢ shrinkYonedaEquiv (shrinkYonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) (shrinkYonedaEquiv t))) =
    (ConcreteCategory.hom (P.map f.unop.op)) (shrinkYonedaEquiv (shrinkYonedaEquiv.symm (shrinkYonedaEquiv t)))

Tactic:
simp

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
i j : K
f : i ⟶ j
j✝ : J
⊢ colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫
      colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Tactic:
simp

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✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
⊢ ∀ (j : J),
    ((flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom).app k ≫
        (limit.π G j).app k =
      ((limitIsoFlipCompLim F).symm.hom ≫ lim.map η).app k ≫ (limit.π G j).app k

Tactic:
intro j

Goal state after:
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✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
j : J
⊢ ((flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom).app k ≫
      (limit.π G j).app k =
    ((limitIsoFlipCompLim F).symm.hom ≫ lim.map η).app k ≫ (limit.π G j).app k
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✝ : HasLimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
⊢ ∀ (j : J),
    (((whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitFlipIsoCompLim G).symm.hom).app k ≫
        (limit.π ((flipFunctor K J C).obj G) j).app k =
      ((limitFlipIsoCompLim F).symm.hom ≫ (flipFunctor K J C ⋙ lim).map η).app k ≫
        (limit.π ((flipFunctor K J C).obj G) j).app k

Tactic:
intro j

Goal state after:
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✝ : HasLimitsOfShape J C
F G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
j : J
⊢ (((whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitFlipIsoCompLim G).symm.hom).app k ≫
      (limit.π ((flipFunctor K J C).obj G) j).app k =
    ((limitFlipIsoCompLim F).symm.hom ≫ (flipFunctor K J C ⋙ lim).map η).app k ≫
      (limit.π ((flipFunctor K J C).obj G) j).app k
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 G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
⊢ ∀ (j : J),
    (colimit.ι F j).app k ≫ (colim.map η ≫ (colimitIsoFlipCompColim G).hom).app k =
      (colimit.ι F j).app k ≫
        ((colimitIsoFlipCompColim F).hom ≫ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj colim).map η).app k

Tactic:
intro j

Goal state after:
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 G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
j : J
⊢ (colimit.ι F j).app k ≫ (colim.map η ≫ (colimitIsoFlipCompColim G).hom).app k =
    (colimit.ι F j).app k ≫
      ((colimitIsoFlipCompColim F).hom ≫ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj colim).map η).app k
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 G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
⊢ ∀ (j : J),
    (colimit.ι ((flipFunctor K J C).obj F) j).app k ≫
        ((flipFunctor K J C ⋙ colim).map η ≫ (colimitFlipIsoCompColim G).hom).app k =
      (colimit.ι ((flipFunctor K J C).obj F) j).app k ≫
        ((colimitFlipIsoCompColim F).hom ≫ ((whiskeringRight K (J ⥤ C) C).obj colim).map η).app k

Tactic:
intro j

Goal state after:
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 G : K ⥤ J ⥤ C
η : F ⟶ G
k : K
j : J
⊢ (colimit.ι ((flipFunctor K J C).obj F) j).app k ≫
      ((flipFunctor K J C ⋙ colim).map η ≫ (colimitFlipIsoCompColim G).hom).app k =
    (colimit.ι ((flipFunctor K J C).obj F) j).app k ≫
      ((colimitFlipIsoCompColim F).hom ≫ ((whiskeringRight K (J ⥤ C) C).obj colim).map η).app k
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 (unop X)
⊢ (fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X))))
      ((fun x ↦
          { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
            naturality := ⋯ })
        x) =
    x

Tactic:
simp

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 : shrinkCoyoneda.{w, v, u}.obj (op X) ⟶ P
⊢ shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) (shrinkCoyonedaEquiv t))) =
    (ConcreteCategory.hom (P.map f.op.unop)) (shrinkCoyonedaEquiv (shrinkCoyonedaEquiv.symm (shrinkCoyonedaEquiv t)))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) (1 j) = 1 j'

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) 1 = 1

Tactic:
simp

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
⊢ ↑1 j = 1
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget MonCat)).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) (x✝¹ * x✝) =
    (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) x✝¹ *
      (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) x✝

Tactic:
simp

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget MonCat)).pt
⊢ ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹ * (equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j =
    ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝¹) j * ↑((equivShrink ↑(F ⋙ forget MonCat).sections).symm x✝) j
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) 1, ⋯⟩ =
    1

Tactic:
simp

Goal state after:
case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) 1 = 1

Tactic:
simp

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) (x✝¹ + x✝) =
    (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝¹ +
      (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝

Tactic:
simp

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹ +
          (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝)
      j =
    ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹) j +
      ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j