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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
c d : Cone F
f : c ≅ d
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt ∧ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
c d : Cone F
f : c ≅ d
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt ∧ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
s : ↑F.sections
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
x : ((const C).obj X).obj x✝²
⊢ (ConcreteCategory.hom (((const C).obj X).map x✝ ≫ ↾fun x ↦ ↑s x✝¹)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ ↑s x✝²) ≫ F.map x✝)).toFun x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝ : (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).obj X✝
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
                (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
          x✝)) =
    F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
                (uliftYoneda.{v₂, v₁, u₁}.obj X).map f)).toFun
          x✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Cᵒᵖ
x✝ : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).obj X✝).obj x✝¹
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              (((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫
                    (hF.homNatIso Y✝).hom).app
                x✝¹)).toFun
          x✝)) =
    F.map
      (Equiv.ulift ((ConcreteCategory.hom (((hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).obj X✝
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
                (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
          x✝)) =
    F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
                (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f)).toFun
          x✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝¹ : C
x✝ : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).obj X✝).obj x✝¹
⊢ F.map
      (Equiv.ulift
        ((ConcreteCategory.hom
              (((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
                    (hF.homNatIso' (unop Y✝)).hom).app
                x✝¹)).toFun
          x✝)) =
    F.map
      (Equiv.ulift
        ((ConcreteCategory.hom (((hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ F.map h.i ≫ (Arrow.mk (τ.app Y)).hom = (Arrow.mk (τ.app X)).hom ≫ G.map h.i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ F.map h.r ≫ (Arrow.mk (τ.app X)).hom = (Arrow.mk (τ.app Y)).hom ≫ G.map h.r

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v
⊢ ⋯.lift ≫ z = v

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Mono f
inst✝ : StrongEpi f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst✝¹ : Mono f
inst✝ : StrongEpi f
⊢ f ≫ ⋯.lift = 𝟙 P ∧ ⋯.lift ≫ f = 𝟙 Q

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z

Tactic:
rw [adj.hasLiftingProperty_iff]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ ∀ ⦃X Y_1 : Discrete PEmpty.{1}⦄ (f : X ⟶ Y_1),
    ((Functor.const (Discrete PEmpty.{1})).obj Y).map f ≫ id (Discrete.casesOn Y_1 fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ F.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty.{1})).obj X).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ F.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X ⟶ Y
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty.{1})).obj X).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ F.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty.{1}),
    f ≫ { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }.π.app j =
      { pt := X, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }.π.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{1})).obj X).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{1})).obj X).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X✝ ⟶ X
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{1})).obj X).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X✝ ⟶ X
⊢ ∀ (j : Discrete PEmpty.{1}),
    { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }.ι.app j ≫ f =
      { pt := X, ι := { app := fun X_2 ↦ id (Discrete.casesOn X_2 fun as ↦ ⋯.elim), naturality := ⋯ } }.ι.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f g : Y ⟶ X
⊢ ∀ (j : Discrete PEmpty.{1}), f ≫ (asEmptyCone X).π.app j = g ≫ (asEmptyCone X).π.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f g : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone X).ι.app j ≫ f = (asEmptyCocone X).ι.app j ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
⊢ ∀ ⦃X Y : Discrete PEmpty.{w + 1}⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ F₁.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j = { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.π.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
⊢ ∀ ⦃X Y : Discrete PEmpty.{w + 1}⦄ (f : X ⟶ Y),
    F₁.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ π F j ≫ eqToHom ⋯ = π F j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ eqToHom ⋯ ≫ ι F j = ι F j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
j : J
⊢ (coneMorphism c).hom ≫ π F j = c.π.app j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (Cone.forget F).map ((isLimit F).uniqueUpToIso t.isLimit).hom ≫ t.cone.π.app j = π F j

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = m ≫ F.map (𝟙 X)

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (Cone.forget F).map ((isLimit F).uniqueUpToIso t.isLimit).inv ≫ π F j = t.cone.π.app j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (limit.isLimit G).lift
        ((Cone.equivalenceOfReindexing e.symm ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
          (limit.cone F)) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ ((limit.isLimit F).conePointsIsoOfEquivalence (limit.isLimit G) e w).inv ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ ∀ (j : J), limMap (𝟙 F) ≫ limit.π F j = 𝟙 (limit F) ≫ limit.π F j

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
j : J
⊢ limMap (𝟙 F) ≫ limit.π F j = 𝟙 (limit F) ≫ limit.π F j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ : J ⥤ C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
j : J
⊢ limMap (𝟙 F) ≫ limit.π F j = 𝟙 (limit F) ≫ limit.π F j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ ∀ (j : J), limMap (α ≫ β) ≫ limit.π Z✝ j = (limMap α ≫ limMap β) ≫ limit.π Z✝ j

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
j : J
⊢ limMap (α ≫ β) ≫ limit.π Z✝ j = (limMap α ≫ limMap β) ≫ limit.π Z✝ j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ (lim.map α ≫ pre G E) ≫ π (E ⋙ G) j✝ = (pre F E ≫ lim.map (E.whiskerLeft α)) ≫ π (E ⋙ G) j✝

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
colimit.ι_desc

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
j : J
⊢ ι F j ≫ colim.map α = α.app j ≫ ι G j

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePullbackShape J)).obj none =
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      none

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePullbackShape J)).obj (some val✝) =
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      (some val✝)

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      none =
    (𝟭 (WidePullbackShape J')).obj none

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      (some val✝) =
    (𝟭 (WidePullbackShape J')).obj (some val✝)

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ ι (E₁ ⋙ F) j✝ ≫ pre F E₁ = ι (E₁ ⋙ F) j✝ ≫ colim.map (whiskerRight α F) ≫ pre F E₂

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = (s.ι.app (Opposite.op j)).unop

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
j : J
⊢ m.unop ≫ t.π.app j = (s.ι.app (Opposite.op j)).unop
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ ∀ (j : J), t.ι.app j ≫ m.unop = (s.π.app (Opposite.op j)).unop

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
j : J
⊢ t.ι.app j ≫ m.unop = (s.π.app (Opposite.op j)).unop