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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ ∀ (j : ↑(F.obj c₁)),
    colimit.ι (Grothendieck.ι F c₁ ⋙ X✝) j ≫
        (fiberwiseColimit X✝).map f ≫ colim.map ((Grothendieck.ι F c₂).whiskerLeft α) =
      colimit.ι (Grothendieck.ι F c₁ ⋙ X✝) j ≫
        colim.map ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y✝).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G✝ : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ }.app x✝ =
    (𝟙 (fiberwiseColimit G)).app x✝

Tactic:
simp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G✝ : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ colimMap (𝟙 (Grothendieck.ι F x✝ ⋙ G)) = 𝟙 (colimit (Grothendieck.ι F x✝ ⋙ G))
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ }.app x✝ =
    ({ app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
          { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }).app
      x✝

Tactic:
simp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ colimMap ((Grothendieck.ι F x✝).whiskerLeft α ≫ (Grothendieck.ι F x✝).whiskerLeft β) =
    colimMap ((Grothendieck.ι F x✝).whiskerLeft α) ≫ colimMap ((Grothendieck.ι F x✝).whiskerLeft β)
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ ≫ f.fiber = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).fiber

Tactic:
simp

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

Goal state before:
pp: case e_a.w_base
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ f.base = ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber).base

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

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
j✝ : ↑(F.obj x✝¹)
⊢ colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x✝) G).hom) ≫
          colimit.pre (Grothendieck.ι F x✝ ⋙ G) (F.map f).toFunctor) ≫
        colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 c.pt

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        ((Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).hom.app ((F.map f.base).toFunctor.obj X.fiber) ≫
            (𝟭 ↑(F.obj Y.base)).map f.fiber ≫ (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).inv.app Y.fiber) ≫
          eqToHom ⋯ =
    f.fiber

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c✝ : Cocone G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
j✝ : ↑(F.obj c)
⊢ colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
        hc.desc
          { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫ s.ι.app c

Tactic:
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:
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:
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
f : X ⟶ Y
⊢ f.fiber = eqToHom ⋯ ≫ f.fiber

Tactic:
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 (eqToHom ⋯).base).toFunctor.obj X.fiber = X.fiber

Tactic:
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 (eqToHom ⋯)).toFunctor.obj X.fiber = X.fiber

Tactic:
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₁.hom, fiber := e₂.hom } ≫
        { base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ }).base =
    (𝟙 X).base

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

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

Goal state before:
pp: case e_a.e_a.e_6
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ f = ((Grothendieck.ιNatTrans f).app X.fiber).base ≫ ((Grothendieck.ι F Y.base).map g).base

Tactic:
simp

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

Goal state before:
pp: case e_a.e_a.e_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ g ≍
    eqToHom ⋯ ≫
      (F.map ((Grothendieck.ι F Y.base).map g).base).toFunctor.map ((Grothendieck.ιNatTrans f).app X.fiber).fiber ≫
        ((Grothendieck.ι F Y.base).map g).fiber

Tactic:
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:
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
⊢ eqToHom ⋯ ≫
      (eqToHom ⋯).toNatTrans.app X.fiber ≫
        (α.app Z.base).toFunctor.map (eqToHom ⋯) ≫
          (eqToHom ⋯ ≫ (α.app Y.base ≫ G.map g.base).toFunctor.map f.fiber ≫ eqToHom ⋯) ≫
            (α.app Z.base).toFunctor.map g.fiber =
    eqToHom ⋯ ≫
      ((G.map g.base).toFunctor.map ((eqToHom ⋯).toNatTrans.app X.fiber) ≫
          (α.app Y.base ≫ G.map g.base).toFunctor.map f.fiber) ≫
        (eqToHom ⋯).toNatTrans.app Y.fiber ≫ (α.app Z.base).toFunctor.map g.fiber

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

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : HasColimit (fiberwiseColimit G)
X : Grothendieck F
⊢ colimit.ι G X =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base) ≫
      (colimitFiberwiseColimitIso G).hom

Tactic:
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✝ : a✝¹ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
a✝ : ↑a✝¹
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerLeft f✝ η✝)).toNatTrans.app (of a✝) =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (prelaxfunctor.map₂ η✝) ≫
              (Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).inv).toNatTrans.app
      (of a✝)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝ : HasColimitsOfShape C H
X✝ Y✝ : Grothendieck F ⥤ H
x✝ : X✝ ⟶ Y✝
j✝¹ : C
j✝ : ↑(F.obj j✝¹)
⊢ colimit.ι (Grothendieck.ι F j✝¹ ⋙ X✝) j✝ ≫
      colimit.ι ((fiberwiseColim F H).obj X✝) j✝¹ ≫
        (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
    colimit.ι (Grothendieck.ι F j✝¹ ⋙ X✝) j✝ ≫
      colimit.ι ((fiberwiseColim F H).obj X✝) j✝¹ ≫ (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber }.base =
    (𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }).base

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

Goal state after:
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✝¹
⊢ h✝.toFunctor.map (η✝.toNatTrans.app a✝) = h✝.toFunctor.map (down (η✝.toNatTrans.app a✝))
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ AsSmall.up.map ((𝟙 (G.obj Y✝.base)).toFunctor.map ((α.app Y✝.base).toFunctor.map f.fiber.down)) ≍
    AsSmall.up.map ((α.app Y✝.base).toFunctor.map f.fiber.down)

Tactic:
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✝ d✝ : Cat
f✝ : a✝¹ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (f✝.toFunctor.associator g✝.toFunctor h✝.toFunctor).hom)).toNatTrans.app (of a✝) =
    (NatTrans.toCatHom₂ (mapComp (f✝.toFunctor ⋙ g✝.toFunctor) h✝.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f✝.toFunctor g✝.toFunctor).hom)
                (map h✝.toFunctor).toCatHom ≫
              (Bicategory.associator (map f✝.toFunctor).toCatHom (map g✝.toFunctor).toCatHom
                    (map h✝.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f✝.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g✝.toFunctor h✝.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f✝.toFunctor (g✝.toFunctor ⋙ h✝.toFunctor)).inv).toNatTrans.app
      (of a✝)

Tactic:
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
X : Grothendieck (G ⋙ typeToCat)
⊢ (𝟭 (Grothendieck (G ⋙ typeToCat))).obj X ≅ (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).obj X

Tactic:
rcases X with ⟨_, ⟨⟩⟩
        exact Iso.refl _

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
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ { base := base, fiber := { down := { down := f } } } ≫ 𝟙 { base := base✝, fiber := { as := as✝ } } =
    𝟙 { base := base✝¹, fiber := { as := as✝¹ } } ≫
      (grothendieckTypeToCatInverse G).map
        ((grothendieckTypeToCatFunctor G).map { base := base, fiber := { down := { down := f } } })

Tactic:
simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ { base := base, fiber := { down := { down := f } } } =
    (grothendieckTypeToCatInverse G).map
      ((grothendieckTypeToCatFunctor G).map { base := base, fiber := { down := { down := f } } })
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
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : ⟨fst✝¹, snd✝¹⟩.fst ⟶ ⟨fst✝, snd✝⟩.fst
e : (ConcreteCategory.hom (G.map f)) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ (grothendieckTypeToCatFunctor G).map ((grothendieckTypeToCatInverse G).map ⟨f, e⟩) ≫
      𝟙 ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj ⟨fst✝, snd✝⟩)) =
    𝟙 ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj ⟨fst✝¹, snd✝¹⟩)) ≫ ⟨f, e⟩

Tactic:
simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : ⟨fst✝¹, snd✝¹⟩.fst ⟶ ⟨fst✝, snd✝⟩.fst
e : (ConcreteCategory.hom (G.map f)) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ (grothendieckTypeToCatFunctor G).map ((grothendieckTypeToCatInverse G).map ⟨f, e⟩) = ⟨f, e⟩
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
base✝ : C
as✝ : G.obj base✝
⊢ (grothendieckTypeToCatFunctor G).map
        ((NatIso.ofComponents
                (fun X ↦
                  casesOn X fun base fiber ↦
                    Discrete.casesOn fiber fun as ↦
                      Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } }))
                ⋯).hom.app
          { base := base✝, fiber := { as := as✝ } }) ≫
      (NatIso.ofComponents
              (fun X ↦
                Sigma.casesOn (motive := fun t ↦
                  X = t →
                    ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ (𝟭 G.Elements).obj X))
                  X
                  (fun fst snd h ↦
                    ⋯ ▸ Iso.refl ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst, snd⟩))
                  ⋯)
              ⋯).hom.app
        ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }) =
    𝟙 ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })

Tactic:
simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝ : C
as✝ : G.obj base✝
⊢ (Sigma.rec (motive := fun t ↦
        (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } } = t →
          ((grothendieckTypeToCatFunctor G).obj
              ((grothendieckTypeToCatInverse G).obj
                ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })) ≅
            (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }))
        (fun fst snd h ↦
          ⋯ ▸ Iso.refl ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj ⟨fst, snd⟩)))
        ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }) ⋯).hom =
    𝟙 ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })
Module: Mathlib.CategoryTheory.WithTerminal.Basic

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

Tactic:
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 : Grothendieck (G ⋙ F)
⊢ eqToHom ⋯ ≫ { base := G.map (𝟙 X).base, fiber := (𝟙 X).fiber }.fiber =
    (𝟙 { base := G.obj X.base, fiber := X.fiber }).fiber

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

Goal state after: