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

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
f : X✝.Hom Y✝
⊢ comp X✝.id f = f

Tactic:
by

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✝
⊢ (fiberwiseColimit G).map f ≫ colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ ((const C).obj c.pt).map f

Tactic:
by

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
f : X.Hom Y
⊢ comp f Y.id = f

Tactic:
by

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
⊢ (coconeFiberwiseColimitOfCocone c✝).ι.app c ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    s.ι.app c

Tactic:
by

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)
m : (coconeFiberwiseColimitOfCocone c).pt ⟶ s.pt
hm : ∀ (j : C), (coconeFiberwiseColimitOfCocone c).ι.app j ≫ m = s.ι.app j
X : Grothendieck F
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }

Tactic:
by

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
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
by

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

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

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
f g : X ⟶ Y
h : f = g
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj X.fiber

Tactic:
by

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

Tactic:
by

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
h : X = Y
⊢ (eqToHom h).base = eqToHom ⋯

Tactic:
by

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
h : X = Y
⊢ (F.map (eqToHom h).base).toFunctor.obj X.fiber = Y.fiber

Tactic:
by

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
h : X = Y
⊢ (eqToHom h).fiber = eqToHom ⋯

Tactic:
by

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
hF : X = Y
⊢ X.base = Y.base

Tactic:
by

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
hF : X = Y
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = Y.fiber

Tactic:
by

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

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
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber

Tactic:
by

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

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

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    (map (𝟭 C)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (𝟭 C)).obj (of a))
          | star => Iso.refl ((map (𝟭 C)).obj star)).hom ≫
        (𝟭 (WithTerminal C)).map f

Tactic:
by

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

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
E : Type u_2
inst✝¹ : Category.{v_1, u_1} D
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    (map (F ⋙ G)).map f ≫
        (match Y with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom =
      (match X with
          | of a => Iso.refl ((map (F ⋙ G)).obj (of a))
          | star => Iso.refl ((map (F ⋙ G)).obj star)).hom ≫
        (map F ⋙ map G).map f

Tactic:
by

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

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

Tactic:
by

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

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 (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.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber ≫ c.ι.app Y.base =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ c.ι.app X.base) ≫
      ((const (Grothendieck F)).obj c.pt).map { base := f, fiber := g }

Tactic:
by

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
F G : C ⥤ D
η : F ⟶ G
⊢ ∀ ⦃X Y : WithTerminal C⦄ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f

Tactic:
by

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 := 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 }

Tactic:
by

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b), NatTrans.toCatHom₂ (map₂ (𝟙 f).toNatTrans) = 𝟙 (map f.toFunctor).toCatHom

Tactic:
by

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

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 (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
hm : ∀ (j : Grothendieck F), (coconeOfCoconeFiberwiseColimit c).ι.app j ≫ m = s.ι.app j
X : C
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc
        { pt := s.pt,
          ι :=
            { app := fun X ↦ colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s),
              naturality := ⋯ } }

Tactic:
by

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 := f.base, fiber := (eqToHom ⋯).toNatTrans.app X.fiber ≫ (α.app Y.base).toFunctor.map f.fiber }

Tactic:
by

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 : C
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫ (colimitFiberwiseColimitIso G).hom =
    colimit.ι G { base := X, fiber := d }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans) =
      NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ map (𝟙 F) = 𝟭 (Grothendieck F)

Tactic:
by

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 ≫ (colimitFiberwiseColimitIso G).inv =
    colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ map (α ≫ β) = map α ⋙ map β

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c : Cat} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    prelaxfunctor.map₂ (Bicategory.whiskerLeft f η) =
      (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

Tactic:
by

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✝
⊢ (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
    (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝

Tactic:
by

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 ⥤ Cat
H : C ⥤ Cat
x✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
⊢ { base := (𝟙 x✝).base, fiber := AsSmall.down.map (𝟙 x✝).fiber } =
    𝟙 { base := x✝.base, fiber := AsSmall.down.obj x✝.fiber }

Tactic:
by

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 ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber } =
    { base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫ { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c : Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    prelaxfunctor.map₂ (Bicategory.whiskerRight η h) =
      (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

Tactic:
by

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
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ (map (whiskerRight α Cat.asSmallFunctor)).map f ≫ (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom =
    (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f

Tactic:
by

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
E : Cat
F : ↑E ⥤ Cat
⊢ Over.homMk (map (𝟙 F)).toCatHom ⋯ = 𝟙 (Over.mk (forget F).toCatHom)

Tactic:
by

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
E : Cat
X✝ Y✝ Z✝ : ↑E ⥤ Cat
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ Over.homMk (map (α ≫ β)).toCatHom ⋯ = Over.homMk (map α).toCatHom ⋯ ≫ Over.homMk (map β).toCatHom ⋯

Tactic:
by

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

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 Y : Grothendieck (G ⋙ typeToCat)} (f : X ⟶ Y),
    (𝟭 (Grothendieck (G ⋙ typeToCat))).map f ≫
        (casesOn Y fun base fiber ↦
            Discrete.casesOn fiber fun as ↦
              Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom =
      (casesOn X fun base fiber ↦
            Discrete.casesOn fiber fun as ↦
              Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom ≫
        (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map f

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    prelaxfunctor.map₂ (Bicategory.associator f g h).hom =
      (Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h.toFunctor)).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h) ≫
          (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
by

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 Y : G.Elements} (f : X ⟶ Y),
    (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).map f ≫
        (Sigma.casesOn (motive := fun t ↦
            Y = t → ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj Y ≅ (𝟭 G.Elements).obj Y)) Y
            (fun fst snd h ↦
              ⋯ ▸ Iso.refl ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst, snd⟩))
            ⋯).hom =
      (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 ≫
        (𝟭 G.Elements).map f

Tactic:
by

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
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫ R.map ((adj.homEquiv c f.right).symm f.hom) = f.hom

Tactic:
by

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
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
c : C
u : StructuredArrow c R := StructuredArrow.mk (adj.unit.app c)
f g : StructuredArrow c R
⊢ u.hom ≫ R.map ((adj.homEquiv c g.right).symm g.hom) = g.hom

Tactic:
by

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)),
    (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
            X) ≫
        (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 X) =
      𝟙 ((grothendieckTypeToCatFunctor G).obj X)

Tactic:
by

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

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
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
d : D
u : CostructuredArrow L d := CostructuredArrow.mk (adj.counit.app d)
f g : CostructuredArrow L d
⊢ L.map ((adj.homEquiv f.left d) f.hom) ≫ u.hom = f.hom

Tactic:
by

Goal state after: