awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
rw :
  (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (η.naturality f).hom ▷ θ.app b ≫
        (η.app a ≫ G.map f) ◁ Γ.as.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        (η.naturality f).hom ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
            η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫
      (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        (η.naturality f).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        (η.naturality f).hom ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
            η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]

Premises used: CategoryTheory.Bicategory.whisker_exchange_assoc, CategoryTheory.Bicategory.associator_inv_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (η.naturality f).hom ▷ θ.app b ≫
        (η.app a ≫ G.map f) ◁ Γ.as.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        (η.naturality f).hom ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
            η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
dsimp :
  F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        (η.naturality f).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫ ((θ ≫ ι).naturality f).hom =
    ((η ≫ ι).naturality f).hom ≫ Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
simp_rw :
  F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      (η.naturality f).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        (η.naturality f).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
simp_rw [Category.assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.associator_inv_naturality_left, CategoryTheory.Bicategory.whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        (θ.naturality f).hom ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫
            θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
      (η.naturality f).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ (ι.naturality f).hom ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
w : ∀ (b_1 : B), (whiskerLeft f θ ≫ whiskerRight η i).as.app b_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app b_1
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
b_1 : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app b_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app b_1

Tactic:
whisker_exchange _ _

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
b_1 : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app b_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app b_1

Tactic:
exact whisker_exchange _ _

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg₁ : f.base = g.base
hfg₂ : eqToHom ⋯ ≫ f.fiber = g.fiber
mk :
  ∀ (base : a.base ⟶ b.base) (fiber : (F.map base.toLoc).toFunctor.obj a.fiber ⟶ b.fiber)
    (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base)
    (hfg₂ : eqToHom ⋯ ≫ { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber),
    { base := base, fiber := fiber : a.Hom b } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
g : a ⟶ b
base : a.base ⟶ b.base
fiber : (F.map base.toLoc).toFunctor.obj a.fiber ⟶ b.fiber
hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base
hfg₂ : eqToHom ⋯ ≫ { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber
mk :
  ∀ (base_1 : a.base ⟶ b.base) (fiber_1 : (F.map base_1.toLoc).toFunctor.obj a.fiber ⟶ b.fiber)
    (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = { base := base_1, fiber := fiber_1 }.base)
    (hfg₂ :
      eqToHom ⋯ ≫ { base := base, fiber := fiber : a.Hom b }.fiber =
        { base := base_1, fiber := fiber_1 : a.Hom b }.fiber),
    { base := base, fiber := fiber : a.Hom b } = { base := base_1, fiber := fiber_1 }
⊢ { base := base, fiber := fiber : a.Hom b } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg : f = g
subst : ∃ (hfg : f.base = f.base), eqToHom ⋯ ≫ f.fiber = f.fiber
⊢ ∃ (hfg : f.base = g.base), eqToHom ⋯ ≫ f.fiber = g.fiber

Tactic:
subst hfg
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ ∃ (hfg : f.base = f.base), eqToHom ⋯ ≫ f.fiber = f.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
h : f = g
subst : f.fiber = eqToHom ⋯ ≫ f.fiber
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ f.fiber = eqToHom ⋯ ≫ f.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
hfg₁ : (𝟙 a ≫ f).base = f.base
hfg₂ : eqToHom ⋯ ≫ (𝟙 a ≫ f).fiber = f.fiber
⊢ 𝟙 a ≫ f = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ (𝟙 a ≫ f).base = f.base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ eqToHom ⋯ ≫ (𝟙 a ≫ f).fiber = f.fiber

Tactic:
simp [F.mapComp_id_left_hom_app, Strict.leftUnitor_eqToIso, ← Functor.map_comp_assoc,
        ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app, CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
hfg₁ : (f ≫ 𝟙 b).base = f.base
hfg₂ : eqToHom ⋯ ≫ (f ≫ 𝟙 b).fiber = f.fiber
⊢ f ≫ 𝟙 b = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ (f ≫ 𝟙 b).base = f.base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ eqToHom ⋯ ≫ (f ≫ 𝟙 b).fiber = f.fiber

Tactic:
simp [F.mapComp_id_right_hom_app, Strict.rightUnitor_eqToIso, ← reassoc_of% Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso, CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
W X Y Z : ∫ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
hfg₁ : ((f ≫ g) ≫ h).base = (f ≫ g ≫ h).base
hfg₂ : eqToHom ⋯ ≫ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
W X Y Z : ∫ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ ((f ≫ g) ≫ h).base = (f ≫ g ≫ h).base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
W X Y Z : ∫ F
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ eqToHom ⋯ ≫ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber

Tactic:
simp [mapComp_assoc_right_hom_app_assoc, Strict.associator_eqToIso]

Premises used: CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc, CategoryTheory.Bicategory.Strict.associator_eqToIso
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
hfg₁ :
  { base := Hom.base (𝟙 a),
        fiber :=
          (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G } }.base =
    Hom.base
      (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber })
hfg₂ :
  CategoryStruct.comp (Y :=
      (G.map
              { base := Hom.base (𝟙 a),
                    fiber :=
                      (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                          ∫ G }.Hom
                      { base := a.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                        ∫ G } }.base.toLoc).toFunctor.obj
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }.fiber)
      (eqToHom ⋯)
      { base := Hom.base (𝟙 a),
          fiber :=
            (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) }.fiber =
    Hom.fiber
      (𝟙
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber : ∫ G })
⊢ { base := Hom.base (𝟙 a),
      fiber :=
        (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
          ∫ G } } =
    𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ { base := Hom.base (𝟙 a),
        fiber :=
          (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G } }.base =
    Hom.base
      (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ CategoryStruct.comp (Y :=
      (G.map
              { base := Hom.base (𝟙 a),
                    fiber :=
                      (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                          ∫ G }.Hom
                      { base := a.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                        ∫ G } }.base.toLoc).toFunctor.obj
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }.fiber)
      (eqToHom ⋯)
      { base := Hom.base (𝟙 a),
          fiber :=
            (α.naturality (Hom.base (𝟙 a)).toLoc).inv.toNatTrans.app a.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) (Hom.fiber (𝟙 a)) }.fiber =
    Hom.fiber
      (𝟙
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber : ∫ G })

Tactic:
simp [StrongTrans.naturality_id_inv_app, ← map_comp, ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
            ∫ G } }.base =
    Hom.base
      ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                ∫ G }.Hom
            { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
              ∫ G } } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ Eq (α :=
    (G.map (f.base.toLoc ≫ g.base.toLoc)).toFunctor.obj
        (obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber) ⟶
      obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber)
    (𝟙
        ((G.map (f.base.toLoc ≫ g.base.toLoc)).toFunctor.obj
          (obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber)) ≫
      (α.naturality (f.base.toLoc ≫ g.base.toLoc)).inv.toNatTrans.app a.fiber ≫
        Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 }))
            ((F.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app a.fiber) ≫
          ((F.map g.base.toLoc).toFunctor ⋙ Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })).map
              f.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber)
    ((G.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app
        (obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber) ≫
      (G.map g.base.toLoc).toFunctor.map ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber) ≫
        (α.naturality g.base.toLoc).inv.toNatTrans.app ((F.map f.base.toLoc).toFunctor.obj a.fiber) ≫
          ((F.map g.base.toLoc).toFunctor ⋙ Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })).map
              f.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber)

Tactic:
simp [naturality_comp_inv_app, ← Functor.map_comp, ← reassoc_of% Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
hfg₁ : ((map (𝟙 F)).map f).base = f.base
hfg₂ : eqToHom ⋯ ≫ ((map (𝟙 F)).map f).fiber = f.fiber
⊢ (map (𝟙 F)).map f = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ eqToHom ⋯ ≫ ((map (𝟙 F)).map f).fiber = f.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
⊢ map α ⋙ forget G = forget F

Tactic:
rfl

Premises used: CategoryTheory.Pseudofunctor.Grothendieck.forget, CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x : ∫ F
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : (map (𝟙 F)).obj x = obj (𝟭 (∫ F)) x
⊢ (map (𝟙 F)).obj x = obj (𝟭 (∫ F)) x

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x : ∫ F
⊢ (map (𝟙 F)).obj x = obj (𝟭 (∫ F)) x

Tactic:
simp [map]

Premises used: CategoryTheory.Pseudofunctor.Grothendieck.map
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x : ∫ F
⊢ (mapIdIso F).hom.app x = eqToHom ⋯

Tactic:
simp [mapIdIso]

Premises used: CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x : ∫ F
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ : (map (α ≫ β)).obj x = (map α ⋙ map β).obj x
⊢ (map (α ≫ β)).obj x = (map α ⋙ map β).obj x

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
dsimp : (map (α ≫ β)).map f ≫ 𝟙 ((map (α ≫ β)).obj Y) = 𝟙 ((map (α ≫ β)).obj X) ≫ (map β).map ((map α).map f)
⊢ (map (α ≫ β)).map f ≫ Iso.hom ((fun (x : ∫ F) ↦ (eqToIso ⋯ : (map (α ≫ β)).obj x ≅ (map α ⋙ map β).obj x)) Y) =
    Iso.hom ((fun (x : ∫ F) ↦ (eqToIso ⋯ : (map (α ≫ β)).obj x ≅ (map α ⋙ map β).obj x)) X) ≫ (map α ⋙ map β).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
simp : (map (α ≫ β)).map f = (map β).map ((map α).map f)
⊢ (map (α ≫ β)).map f ≫ 𝟙 ((map (α ≫ β)).obj Y) = 𝟙 ((map (α ≫ β)).obj X) ≫ (map β).map ((map α).map f)

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X Y : ∫ F
f : X ⟶ Y
hfg₁ : ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base
hfg₂ : eqToHom ⋯ ≫ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber
⊢ (map (α ≫ β)).map f = (map β).map ((map α).map f)

Tactic:
ext