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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X.Hom Y
g : Y.Hom Z
⊢ (F.map (f.base ≫ g.base)).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj ((F.map f.base).toFunctor.obj X.fiber)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X).base).toFunctor.obj X.fiber = X.fiber

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ (F.map (f ≫ g).base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj ((F.map f.base).toFunctor.obj X.fiber)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ eqToHom hF = { base := eqToHom ⋯, fiber := eqToHom ⋯ }

Tactic:
subst hF
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ ({ base := e₁.hom, fiber := e₂.hom } ≫
        { base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ }).base =
    (𝟙 X).base

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ eqToHom ⋯ ≫
      ({ base := e₁.hom, fiber := e₂.hom } ≫
          { base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ }).fiber =
    (𝟙 X).fiber

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ } ≫
        { base := e₁.hom, fiber := e₂.hom }).base =
    (𝟙 Y).base

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
α : F ⟶ G
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ { base := (f ≫ g).base,
        fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Z.base).toFunctor.map (f ≫ g).fiber }.base =
    ({ base := f.base, fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Y.base).toFunctor.map f.fiber } ≫
        { base := g.base, fiber := (eqToHom ⋯).toNatTrans.app Y.fiber ≫ (α.app Z.base).toFunctor.map g.fiber }).base

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
X Y : Grothendieck F
f : X ⟶ Y
⊢ ((map α).map f).base =
    { base := f.base, fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Y.base).toFunctor.map f.fiber }.base

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Cat
α : F ⟶ G
X Y : Grothendieck F
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ ((map α).map f).fiber =
    { base := f.base, fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Y.base).toFunctor.map f.fiber }.fiber

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ c✝ : Cat
f✝ g✝ : a✝¹ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
a✝ : ↑a✝¹
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerRight η✝ h✝)).toNatTrans.app (of a✝) =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η✝) (prelaxfunctor.map h✝) ≫
              (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv).toNatTrans.app
      (of a✝)

Tactic:
simp
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ⥤ C
X : Grothendieck (G ⋙ F)
⊢ eqToHom ⋯ ≫ { base := G.map (𝟙 X).base, fiber := (𝟙 X).fiber }.fiber =
    (𝟙 { base := G.obj X.base, fiber := X.fiber }).fiber

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ⥤ C
X✝ Y✝ Z✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := G.map (f ≫ g).base, fiber := (f ≫ g).fiber }.fiber =
    ({ base := G.map f.base, fiber := f.fiber } ≫ { base := G.map g.base, fiber := g.fiber }).fiber

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = (G.map (homToLift F X) ≫ c.ι.app (lift F X)) ≫ 𝟙 c.pt

Tactic:
simp only [Category.comp_id]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map (homToLift F X) ≫ c.ι.app (lift F X)
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
⊢ (F.map (𝟙 { base := c, fiber := X✝ }.base)).toFunctor.obj { base := c, fiber := X✝ }.fiber = X✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
d : ↑(F.obj c)
⊢ eqToHom ⋯ ≫ 𝟙 d = eqToHom ⋯

Tactic:
simp only [Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f ≫ g }.base =
    ({ base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f } ≫
        { base := 𝟙 { base := c, fiber := Y✝ }.base, fiber := eqToHom ⋯ ≫ g }).base

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case e_a
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ f = eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f ≫ eqToHom ⋯

Tactic:
apply Functor.congr_hom congr($(F.map_id _).toFunctor).symm

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ ({ base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) }).base =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }).base

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ eqToHom ⋯ ≫
      ({ base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) }).fiber =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }).fiber

Tactic:
simp [eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c : Comma (𝟭 (C ⥤ D)) (Functor.const C)
x y : C
f : x ⟶ y
⊢ c.left.map f ≫ c.hom.app y = c.hom.app x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f✝ : x ⟶ y
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
⊢ ((ofCommaObject c).map f ≫
      match of a✝ with
      | of x => φ.left.app x
      | star => φ.right) =
    (match of a✝¹ with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
x✝ : star ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.left.app x
      | star => φ.right) =
    (match star with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x✝

Tactic:
by simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasColimit F
c : Cocone F
inst✝ : IsIso (colimMap c.ι)
⊢ ∀ (j : J),
    (colimit.cocone F).ι.app j ≫
        (asIso (colimMap c.ι) ≪≫
            (colimit.isColimit ((Functor.const J).obj c.pt)).coconePointUniqueUpToIso
              (isColimitConstCocone J c.pt)).hom =
      c.ι.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
t : WithTerminal C
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      t =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      t

Tactic:
cases t

Goal state after:
case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
a✝ : C
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      (of a✝) =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      (of a✝)

case star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      star =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      star
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
hc' : IsColimit (H.mapCocone (extendCocone.obj c)) := isColimitOfPreserves H ((isColimitExtendCoconeEquiv F c).symm hc)
⊢ ∀ (j : D),
    (H.mapCocone (extendCocone.obj c)).ι.app j ≫ (Iso.refl (H.mapCocone (extendCocone.obj c)).pt).hom =
      (extendCocone.obj (H.mapCocone c)).ι.app j

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (extendCocone.obj (H.mapCocone c)) := (isColimitExtendCoconeEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : D),
    (extendCocone.obj (H.mapCocone c)).ι.app j ≫ (Iso.refl (extendCocone.obj (H.mapCocone c)).pt).hom =
      (H.mapCocone (extendCocone.obj c)).ι.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
X✝ Y✝ : WithTerminal (Discrete J)
f : X✝ ⟶ Y✝
⊢ widePullbackShapeEquivObj (widePullbackShapeEquivObj.symm X✝) = X✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
X✝ Y✝ : WithTerminal (Discrete J)
f : X✝ ⟶ Y✝
⊢ Y✝ = widePullbackShapeEquivObj (widePullbackShapeEquivObj.symm Y✝)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCocone (Cocone.whisker F c)).ι.app j ≫ (Iso.refl (H.mapCocone (Cocone.whisker F c)).pt).hom =
      (Cocone.whisker F (H.mapCocone c)).ι.app j

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : C),
    (Cocone.whisker F (H.mapCocone c)).ι.app j ≫ (Iso.refl (Cocone.whisker F (H.mapCocone c)).pt).hom =
      (H.mapCocone (Cocone.whisker F c)).ι.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₁ = m₂

Tactic:
by
  have : m₂ = EffectiveEpiFamily.desc X π (fun a => π a ≫ m₂)
      (fun a₁ a₂ g₁ g₂ h => by simp only [← assoc, h]) := by
    apply EffectiveEpiFamily.uniq; intro; rfl
  rw [this]
  exact EffectiveEpiFamily.uniq _ _ _ _ _ h

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
W✝ : C
x✝¹ : X ⟶ W✝
x✝ : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ x✝¹ = g₂ ≫ x✝¹
⊢ f ≫ inv f ≫ x✝¹ = x✝¹

Tactic:
by simp

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}

Tactic:
refine Types.isTerminalEquivIsoPUnit _ ?_

Goal state after:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ IsTerminal (colimit (F ⋙ coyoneda.obj (op d)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsColimit (ofπ f ⋯)
⊢ (Iso.refl (Fork.ofι f.op ⋯).pt).hom ≫ (Fork.ofι f.op ⋯).ι = (Fork.ofι f.op ⋯).ι ≫ (Iso.refl (Opposite.op X)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (pullbackIsoUnopPushout f f).symm.hom ≫ pullback.fst f f =
    (pushout.inl f.op f.op).unop ≫ (Iso.refl (Opposite.unop (Opposite.op X))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (pullbackIsoUnopPushout f f).symm.hom ≫ pullback.snd f f =
    (pushout.inr f.op f.op).unop ≫ (Iso.refl (Opposite.unop (Opposite.op X))).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (Functor.const C) (𝟭 (C ⥤ D))
φ : c ⟶ c'
x y : WithInitial C
f✝ : x ⟶ y
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
⊢ ((ofCommaObject c).map f ≫
      match of a✝ with
      | of x => φ.right.app x
      | star => φ.left) =
    (match of a✝¹ with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (ofCommaObject c').map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op X))).inv ≫ (ofπ f.op.unop ⋯).π ≫ (Iso.refl (ofπ f.op.unop ⋯).pt).hom =
    (ofπ f ⋯).π

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (Functor.const C) (𝟭 (C ⥤ D))
φ : c ⟶ c'
x y : WithInitial C
f : x ⟶ y
x✝ : star ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.right.app x
      | star => φ.left) =
    (match star with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (ofCommaObject c').map x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsColimit (ofπ f ⋯)
⊢ (Iso.refl (Fork.ofι f.unop ⋯).pt).hom ≫ (Fork.ofι f.unop ⋯).ι =
    (Fork.ofι f.unop ⋯).ι ≫ (Iso.refl (Opposite.unop X)).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
hc' : IsLimit (H.mapCone (extendCone.obj c)) := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)
⊢ ∀ (j : D),
    (H.mapCone (extendCone.obj c)).π.app j =
      (Iso.refl (H.mapCone (extendCone.obj c)).pt).hom ≫ (extendCone.obj (H.mapCone c)).π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
t : WithInitial C
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      t =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      t

Tactic:
cases t

Goal state after:
case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
a✝ : C
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      (of a✝) =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      (of a✝)

case star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      star =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      star
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.unop ⋯)
⊢ (pullbackIsoOpPushout f f).symm.hom ≫ pullback.fst f f =
    (pushout.inl f.unop f.unop).op ≫ (Iso.refl (Opposite.op (Opposite.unop X))).hom

Tactic:
by simp

Goal state after: