mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : (toOver yoneda A).obj X ⟶ T
⊢ (overEquivPresheafCostructuredArrow A).inverse.map
      ((ConcreteCategory.hom (((toOverCompCoyoneda A).hom.app (op X)).app T)) f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
      f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Tactic:
by

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringRight C D E).obj F).mapCone c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T
⊢ (overEquivPresheafCostructuredArrow A).functor.map
      ((ConcreteCategory.hom (((toOverCompCoyoneda A).inv.app (op X)).app T)) f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
⊢ F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂

Tactic:
by

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J E
F : D ⥤ E
inst✝ : ReflectsLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit (((whiskeringRight C D E).obj F).mapCone c)
⊢ IsLimit c

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ (limitCompWhiskeringRightIsoLimitComp F G).inv ≫ limit.π (G ⋙ (whiskeringRight C D E).obj F) j =
    whiskerRight (limit.π G j) F

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ (limitCompWhiskeringRightIsoLimitComp F G).hom ≫ whiskerRight (limit.π G j) F =
    limit.π (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
⊢ ∃ n, j ≤ sequentialFunctor_obj J n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
j : J
⊢ ∃ n, sequentialFunctor_obj J n ≤ j

Tactic:
by

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cocone K
hc : IsColimit c
⊢ IsColimit (((whiskeringRight C D E).obj F).mapCocone c)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ colimit.ι (G ⋙ (whiskeringRight C D E).obj F) j ≫ (colimitCompWhiskeringRightIsoColimitComp F G).hom =
    whiskerRight (colimit.ι G j) F

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ whiskerRight (colimit.ι G j) F ≫ (colimitCompWhiskeringRightIsoColimitComp F G).inv =
    colimit.ι (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
by

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

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
d : D
X : K ⥤ D ⥤ C
⊢ colimit (X ⋙ (evaluation D C).obj d) ≅
    colimit (((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip ⋙ (evaluation (K ⥤ D ⥤ C) C).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
⊢ StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u) =
    StructuredArrow.hom y

Tactic:
by

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

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
d : D
F G : K ⥤ D ⥤ C
η : F ⟶ G
j : K
⊢ (colimit.ι F j).app d ≫
      (colim ⋙ (evaluation D C).obj d).map η ≫
        (colimitObjIsoColimitCompEvaluation G d ≪≫
            HasColimit.isoOfNatIso (Iso.refl (G ⋙ (evaluation D C).obj d)) ≪≫
              (colimitObjIsoColimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  G).symm).hom =
    (colimit.ι F j).app d ≫
      (colimitObjIsoColimitCompEvaluation F d ≪≫
            HasColimit.isoOfNatIso (Iso.refl (F ⋙ (evaluation D C).obj d)) ≪≫
              (colimitObjIsoColimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  F).symm).hom ≫
        (colimit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip).map η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
⊢ IsConnected (CostructuredArrow (sequentialFunctor J) d)

Tactic:
by

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

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasLimitsOfShape K C
inst✝ : PreservesColimitsOfShape J lim
d : D
X : K ⥤ D ⥤ C
⊢ limit (X ⋙ (evaluation D C).obj d) ≅
    limit (((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip ⋙ (evaluation (K ⥤ D ⥤ C) C).obj X)

Tactic:
by

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

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasLimitsOfShape K C
inst✝ : PreservesColimitsOfShape J lim
d : D
F G : K ⥤ D ⥤ C
η : F ⟶ G
j : K
⊢ ((lim ⋙ (evaluation D C).obj d).map η ≫
        (limitObjIsoLimitCompEvaluation G d ≪≫
            HasLimit.isoOfNatIso (Iso.refl (G ⋙ (evaluation D C).obj d)) ≪≫
              (limitObjIsoLimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  G).symm).hom) ≫
      (limit.π ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip j).app G =
    ((limitObjIsoLimitCompEvaluation F d ≪≫
            HasLimit.isoOfNatIso (Iso.refl (F ⋙ (evaluation D C).obj d)) ≪≫
              (limitObjIsoLimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  F).symm).hom ≫
        (limit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip).map η) ≫
      (limit.π ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip j).app G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
⊢ Unique ((precomp₂ L' α).obj b ⟶ y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
⊢ StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u) = StructuredArrow.hom y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
⊢ Unique (b ⟶ y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
⊢ StructuredArrow.IsUniversal b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
x : StructuredArrow.IsUniversal b
⊢ (fun h ↦ isUniversalOfPrecomp₂ α hα h) ((fun h ↦ isUniversalPrecomp₂ α hα h) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
x : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
⊢ (fun h ↦ isUniversalPrecomp₂ α hα h) ((fun h ↦ isUniversalOfPrecomp₂ α hα h) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
⊢ StructuredArrow.hom ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) ≫
      ((whiskeringLeft C D' H).obj (L ⋙ L')).map
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
            ⋯).hom =
    StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_2} J
inst✝⁹ : Category.{v_2, u_1} D
inst✝⁸ : HasColimitsOfShape J C
inst✝⁷ : HasColimitsOfShape J D
inst✝⁶ : HasExactColimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : ReflectsFiniteLimits F
inst✝³ : HasFiniteLimits C
inst✝² : PreservesColimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cone G
hc : IsLimit c
⊢ Nonempty (IsLimit (colim.mapCone c))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
⊢ α ≫
      L.whiskerLeft
        (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
          (const D).map (hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι })) =
    α ≫ L.whiskerLeft s.ι

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
⊢ A.map f ≫ (uliftYonedaEquiv g).down = (uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map f ≫ g)).down

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (lim.mapCocone c))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
⊢ ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } = s.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
⊢ HasExactColimitsOfShape J D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
⊢ HasExactLimitsOfShape J D

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map g.unop ≫ (CostructuredArrow.mk (uliftYonedaEquiv.symm x)).hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ({ hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        f).unop =
    (cokernel.π (kernel.ι f.unop)).op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
⊢ (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) =
    (↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
      ((restrictedULiftYoneda A).obj E).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
⊢ PreservesLimit H colim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Subobject X ≃o (Subobject (op X))ᵒᵈ

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A).map f ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down =
    (uliftYonedaEquiv (y.hom ≫ g)).down ≫
      ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
⊢ PreservesColimit H lim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Transfer

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive D
F : C ⥤ D
hF : F.FullyFaithful
P Q R : C
f f' : P ⟶ Q
g : Q ⟶ R
⊢ F.map ((f + f') ≫ g) = F.map (f ≫ g + f' ≫ g)

Tactic:
by

Goal state after: