awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base

Tactic:
simp
-- 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
⊢ eqToHom ⋯ ≫ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber

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

Tactic:
simp [map]

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

Tactic:
simp [mapCompIso]

Premises used: CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso
-- 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₂ : f.fiber = g.fiber ≫ eqToHom ⋯
mk :
  ∀ (base : a.base ⟶ b.base) (fiber : a.fiber ⟶ obj (Cat.Hom.toFunctor (F.map base.op.toLoc)) b.fiber)
    (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base)
    (hfg₂ : { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber ≫ eqToHom ⋯),
    { 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 : a.fiber ⟶ obj (Cat.Hom.toFunctor (F.map base.op.toLoc)) b.fiber
hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = g.base
hfg₂ : { base := base, fiber := fiber : a.Hom b }.fiber = g.fiber ≫ eqToHom ⋯
mk :
  ∀ (base_1 : a.base ⟶ b.base) (fiber_1 : a.fiber ⟶ obj (Cat.Hom.toFunctor (F.map base_1.op.toLoc)) b.fiber)
    (hfg₁ : { base := base, fiber := fiber : a.Hom b }.base = { base := base_1, fiber := fiber_1 }.base)
    (hfg₂ :
      { base := base, fiber := fiber : a.Hom b }.fiber =
        { base := base_1, fiber := fiber_1 : a.Hom b }.fiber ≫ eqToHom ⋯),
    { 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
rw rw₁ : g.base = g.base
⊢ f.base = g.base

Tactic:
rw [hfg]
-- 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
⊢ f.fiber = g.fiber ≫ eqToHom ⋯

Tactic:
simp [hfg]
-- 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
⊢ f.fiber = g.fiber ≫ eqToHom ⋯

Tactic:
simp [h]
-- 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₂ : (𝟙 a ≫ f).fiber = f.fiber ≫ eqToHom ⋯
⊢ 𝟙 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
⊢ (𝟙 a ≫ f).fiber = f.fiber ≫ eqToHom ⋯

Tactic:
simp [F.mapComp_id_right_inv_app, Strict.rightUnitor_eqToIso, ← NatTrans.naturality_assoc,
        ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso, CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app, CategoryTheory.NatTrans.naturality_assoc
-- 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₂ : (f ≫ 𝟙 b).fiber = f.fiber ≫ eqToHom ⋯
⊢ 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
⊢ (f ≫ 𝟙 b).fiber = f.fiber ≫ eqToHom ⋯

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

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso
-- 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₂ : ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber ≫ eqToHom ⋯
⊢ (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
⊢ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber ≫ eqToHom ⋯

Tactic:
simp [← NatTrans.naturality_assoc, F.mapComp_assoc_right_inv_app, Strict.associator_eqToIso]

Premises used: CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app, CategoryTheory.NatTrans.naturality_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
⊢ { base := Hom.base (𝟙 a),
        fiber :=
          Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (Hom.fiber (𝟙 a)) ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc))) a.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
              ∫ᶜ G }.Hom
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G } }.base =
    Hom.base
      (𝟙 { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op 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 b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ { base := (f ≫ g).base,
        fiber :=
          Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (f ≫ g).fiber ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
              ∫ᶜ G }.Hom
          { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
            ∫ᶜ G } }.base =
    Hom.base
      ({ base := f.base,
          fiber :=
            Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber :
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                ∫ᶜ G }.Hom
            { base := b.base,
              fiber := obj (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) b.fiber : ∫ᶜ G } } ≫
        { base := g.base,
          fiber :=
            Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.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
a₁ :
  Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base }))
    (Functor.map (Cat.Hom.toFunctor (F.map f.base.op.toLoc)) g.fiber)
| Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
      (Functor.map (Cat.Hom.toFunctor (F.map f.base.op.toLoc)) g.fiber) ≫
    Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp g.base.op.toLoc f.base.op.toLoc))) c.fiber) ≫
      Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base }))
        (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp g.base.op.toLoc f.base.op.toLoc))) c.fiber)

Tactic:
simp [← Cat.Hom.toNatIso_inv, Cat.Hom.comp_toFunctor,
        ← Cat.Hom.toNatIso_hom, ← map_comp, Iso.inv_hom_id_app, comp_obj, map_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Cat.Hom.toNatIso_hom, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Cat.Hom.toNatIso_inv
-- 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
⊢ Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
      ((Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
              (Functor.map (Cat.Hom.toFunctor (F.map f.base.op.toLoc)) g.fiber) ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc)))
              (obj (Cat.Hom.toFunctor (F.map g.base.op.toLoc)) c.fiber)) ≫
          Functor.map (Cat.Hom.toFunctor (G.map f.base.op.toLoc))
            (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber)) ≫
        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (G.mapComp g.base.op.toLoc f.base.op.toLoc)))
          (obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber) =
    Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
      NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber ≫
        Functor.map (Cat.Hom.toFunctor (G.map f.base.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber) ≫
          Functor.map (Cat.Hom.toFunctor (G.map f.base.op.toLoc))
              (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber) ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (G.mapComp g.base.op.toLoc f.base.op.toLoc)))
              (obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber)

Tactic:
simp only [assoc, ← reassoc_of% Cat.Hom.comp_map,
        (α.naturality f.base.op.toLoc).hom.toNatTrans.naturality_assoc]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality, CategoryTheory.Category.assoc, Quiver.Hom.op, CategoryTheory.Cat.Hom.comp_map, Quiver.Hom.toLoc, CategoryTheory.Cat.Hom₂.toNatTrans, CategoryTheory.Iso.hom, CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.base, CategoryTheory.NatTrans.naturality_assoc
-- 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₂ : ((map (𝟙 F)).map f).fiber = f.fiber ≫ eqToHom ⋯
⊢ (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
⊢ ((map (𝟙 F)).map f).fiber = f.fiber ≫ eqToHom ⋯

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.Functor.comp, CategoryTheory.Pseudofunctor.CoGrothendieck.forget, 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.CoGrothendieck.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.CoGrothendieck.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₂ : ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber ≫ eqToHom ⋯
⊢ (map (α ≫ β)).map f = (map β).map ((map α).map f)

Tactic:
ext
-- 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
⊢ ((map (α ≫ β)).map f).base = ((map β).map ((map α).map f)).base

Tactic:
simp
-- 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
⊢ ((map (α ≫ β)).map f).fiber = ((map β).map ((map α).map f)).fiber ≫ eqToHom ⋯

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

Tactic:
simp [map]

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.map
-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x : ∫ᶜ F
⊢ (mapCompIso α β).hom.app x = eqToHom ⋯

Tactic:
simp [mapCompIso]

Premises used: CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f g : X ⟶ Y
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.Bicategory.InducedBicategory.Hom.ext
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f g : X ⟶ Y
η θ : f ⟶ g
h : η.hom = θ.hom
⊢ η = θ

Tactic:
Hom₂.ext h

Premises used: CategoryTheory.Bicategory.InducedBicategory.Hom₂.ext
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_2} C
F : B → C
x x_1 x_2 : InducedBicategory C F
x_3 x_4 : x ⟶ x_1
x_5 x_6 : x_1 ⟶ x_2
η : x_3 ⟶ x_4
θ : x_5 ⟶ x_6
h :
  (mkHom₂ (x_3.hom ◁ θ.hom) ≫ mkHom₂ (η.hom ▷ x_6.hom)).hom = (mkHom₂ (η.hom ▷ x_5.hom) ≫ mkHom₂ (x_4.hom ◁ θ.hom)).hom
⊢ mkHom₂ (x_3.hom ◁ θ.hom) ≫ mkHom₂ (η.hom ▷ x_6.hom) = mkHom₂ (η.hom ▷ x_5.hom) ≫ mkHom₂ (x_4.hom ◁ θ.hom)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_2} C
F : B → C
x x_1 x_2 : InducedBicategory C F
x_3 x_4 : x ⟶ x_1
x_5 x_6 : x_1 ⟶ x_2
η : x_3 ⟶ x_4
θ : x_5 ⟶ x_6
⊢ (mkHom₂ (x_3.hom ◁ θ.hom) ≫ mkHom₂ (η.hom ▷ x_6.hom)).hom = (mkHom₂ (η.hom ▷ x_5.hom) ≫ mkHom₂ (x_4.hom ◁ θ.hom)).hom

Tactic:
simpa using whisker_exchange _ _

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f g : X ⟶ Y
h : f = g
subst : Hom₂.hom (eqToHom ⋯) = eqToHom ⋯
⊢ Hom₂.hom (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f : X ⟶ Y
⊢ Hom₂.hom (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, Hom.category_id_hom]

Premises used: CategoryTheory.Bicategory.InducedBicategory.Hom.category_id_hom, CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f g : F X ⟶ F Y
h : f = g
h₁ : (mkHom₂ (eqToHom h)).hom = Hom₂.hom (eqToHom ⋯)
⊢ mkHom₂ (eqToHom h) = eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f g : F X ⟶ F Y
h : f = g
h₁ : (mkHom₂ (eqToHom ⋯)).hom = Hom₂.hom (eqToHom ⋯)
⊢ (mkHom₂ (eqToHom h)).hom = Hom₂.hom (eqToHom ⋯)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_4, u_3, u_2} C
F : B → C
X Y : InducedBicategory C F
f : F X ⟶ F Y
⊢ (mkHom₂ (eqToHom ⋯)).hom = Hom₂.hom (eqToHom ⋯)

Tactic:
simp only [eqToHom_refl, Hom.category_id_hom]

Premises used: CategoryTheory.Bicategory.InducedBicategory.Hom.category_id_hom, CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
dsimp :
  (adj.unit ▷ h ≫ (α_ f u h).hom) ≫ f ◁ (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)
⊢ ((LeftExtension.mk u adj.unit).whisker h).unit ≫
      f ◁ (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
dsimp only [whisker_extension, StructuredArrow.mk_right, whisker_unit,
            StructuredArrow.mk_hom_eq_self]

Premises used: CategoryTheory.StructuredArrow.mk_right, CategoryTheory.Bicategory.LeftExtension.whisker_unit, CategoryTheory.Bicategory.LeftExtension.whisker_extension, CategoryTheory.StructuredArrow.mk_hom_eq_self
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ (adj.unit ▷ h ≫ (α_ f u h).hom) ≫ f ◁ (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
rw :
  𝟙 (𝟙 a ≫ h) ⊗≫ (𝟙 a ◁ s.unit ≫ adj.unit ▷ (f ≫ s.extension)) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ (adj.unit ▷ (𝟙 a ≫ h) ≫ (f ≫ u) ◁ s.unit) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ (𝟙 a ◁ s.unit ≫ adj.unit ▷ (f ≫ s.extension)) ⊗≫ f ◁ adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) =
    𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
rw : 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit

Tactic:
rw [adj.left_triangle]

Premises used: CategoryTheory.Bicategory.Adjunction.left_triangle
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
h₁ :
  StructuredArrow.Hom.right τ₀ =
    StructuredArrow.Hom.right
      ((fun (s : LeftExtension f (𝟙 a ≫ h)) ↦
          homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)
        s)
⊢ τ₀ =
    (fun (s : LeftExtension f (𝟙 a ≫ h)) ↦
        homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)
      s

Tactic:
ext