mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ α.naturality (𝟙 a) = F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ (α.naturality (𝟙 a)).hom =
    (F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ α.naturality g = F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).hom = (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ α.naturality (f ≫ g) =
    F.mapComp f g ▷ᵢ α.app c ≪≫
      α_ (F.map f) (F.map g) (α.app c) ≪≫
        F.map f ◁ᵢ α.naturality g ≪≫
          (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
            α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).hom =
    (F.mapComp f g ▷ᵢ α.app c ≪≫
        α_ (F.map f) (F.map g) (α.app c) ≪≫
          F.map f ◁ᵢ α.naturality g ≪≫
            (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
              α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
a✝ : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app a✝ = (whiskerRight η h ≫ whiskerLeft g θ).as.app a✝
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫ ((η ≫ ι).naturality f).hom =
    ((η ≫ θ).naturality f).hom ≫ (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
dsimp
      rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵖ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵖ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
b✝ : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app b✝ = (whiskerRight η h ≫ whiskerLeft g θ).as.app b✝
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵒᵖᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
Γ : h ⟶ i
⊢ whiskerLeft f Γ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g Γ

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵒᵖᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
Γ : h ⟶ i
a✝ : B
⊢ (whiskerLeft f Γ ≫ whiskerRight η i).as.app a✝ = (whiskerRight η h ≫ whiskerLeft g Γ).as.app a✝
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
dsimp
      rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ 𝟙 a ≫ f = f

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ (𝟙 a ≫ f).base = f.base

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ f ≫ 𝟙 b = f

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ (f ≫ 𝟙 b).base = f.base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ eqToHom ⋯ ≫ (f ≫ 𝟙 b).fiber = f.fiber
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵒᵖᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
ext

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : B ⥤ᵒᵖᴸ C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
b✝ : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app b✝ = (whiskerRight η h ≫ whiskerLeft g θ).as.app b✝
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : 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 = f ≫ g ≫ h

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : 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

case hfg₂
𝒮 : 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
Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
x✝⁶ x✝⁵ x✝⁴ : InducedBicategory C F
x✝³ x✝² : x✝⁶ ⟶ x✝⁵
x✝¹ x✝ : x✝⁵ ⟶ x✝⁴
η : x✝³ ⟶ x✝²
θ : x✝¹ ⟶ x✝
⊢ mkHom₂ (x✝³.hom ◁ θ.hom) ≫ mkHom₂ (η.hom ▷ x✝.hom) = mkHom₂ (η.hom ▷ x✝¹.hom) ≫ mkHom₂ (x✝².hom ◁ θ.hom)

Tactic:
ext

Goal state after:
B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
x✝⁶ x✝⁵ x✝⁴ : InducedBicategory C F
x✝³ x✝² : x✝⁶ ⟶ x✝⁵
x✝¹ x✝ : x✝⁵ ⟶ x✝⁴
η : x✝³ ⟶ x✝²
θ : x✝¹ ⟶ x✝
⊢ (mkHom₂ (x✝³.hom ◁ θ.hom) ≫ mkHom₂ (η.hom ▷ x✝.hom)).hom = (mkHom₂ (η.hom ▷ x✝¹.hom) ≫ mkHom₂ (x✝².hom ◁ θ.hom)).hom
Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f g : X ⟶ Y
h : f = g
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
by
  subst h; simp only [eqToHom_refl, Hom.category_id_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.InducedBicategory

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f g : F X ⟶ F Y
h : f = g
⊢ mkHom₂ (eqToHom h) = eqToHom ⋯

Tactic:
ext

Goal state after:
B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f g : F X ⟶ F Y
h : f = g
⊢ (mkHom₂ (eqToHom h)).hom = (eqToHom ⋯).hom
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ { base := (𝟙 a).base,
      fiber :=
        (α.naturality (𝟙 a).base.toLoc).inv.toNatTrans.app a.fiber ≫
          (α.app { as := a.base }).toFunctor.map (𝟙 a).fiber } =
    𝟙 { base := a.base, fiber := (α.app { as := a.base }).toFunctor.obj a.fiber }

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.naturality (𝟙 a).base.toLoc).inv.toNatTrans.app a.fiber ≫
            (α.app { as := a.base }).toFunctor.map (𝟙 a).fiber }.base =
    (𝟙 { base := a.base, fiber := (α.app { as := a.base }).toFunctor.obj a.fiber }).base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ eqToHom ⋯ ≫
      { base := (𝟙 a).base,
          fiber :=
            (α.naturality (𝟙 a).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := a.base }).toFunctor.map (𝟙 a).fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := a.base }).toFunctor.obj a.fiber }).fiber
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : 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 ≫
          (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber } =
    { base := f.base,
        fiber :=
          (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
      { base := g.base,
        fiber :=
          (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫ (α.app { as := c.base }).toFunctor.map g.fiber }

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : 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 ≫
            (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.base =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
⊢ eqToHom ⋯ ≫
      { base := (f ≫ g).base,
          fiber :=
            (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := c.base }).toFunctor.map (f ≫ g).fiber }.fiber =
    ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫ (α.app { as := b.base }).toFunctor.map f.fiber } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              (α.app { as := c.base }).toFunctor.map g.fiber }).fiber
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ (map (𝟙 F)).map f = f

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
x y : ∫ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ F
f : X✝ ⟶ Y✝
⊢ (map (α ≫ β)).map f = (map β).map ((map α).map f)

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : 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

case hfg₂
𝒮 : 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
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ 𝟙 a ≫ f = f

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ (𝟙 a ≫ f).base = f.base

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ f ≫ 𝟙 b = f

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ (f ≫ 𝟙 b).base = f.base

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

Goal state before:
pp: 𝒮 : 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 = f ≫ g ≫ h

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : 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

case hfg₂
𝒮 : 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 ⋯
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : 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 :=
        (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
          (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber } =
    { base := f.base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map f.fiber ≫
            (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
      { base := g.base,
        fiber :=
          (α.app { as := op b.base }).toFunctor.map g.fiber ≫
            (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : 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 :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.base =
    ({ base := f.base,
          fiber :=
            (α.app { as := op a.base }).toFunctor.map f.fiber ≫
              (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
        { base := g.base,
          fiber :=
            (α.app { as := op b.base }).toFunctor.map g.fiber ≫
              (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).base

case hfg₂
𝒮 : 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 :=
          (α.app { as := op a.base }).toFunctor.map (f ≫ g).fiber ≫
            (α.naturality (f ≫ g).base.op.toLoc).hom.toNatTrans.app c.fiber }.fiber =
    ({ base := f.base,
            fiber :=
              (α.app { as := op a.base }).toFunctor.map f.fiber ≫
                (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber } ≫
          { base := g.base,
            fiber :=
              (α.app { as := op b.base }).toFunctor.map g.fiber ≫
                (α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber }).fiber ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s✝ t✝ : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
τ : t.ofCompId ⟶ s
⊢ τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s✝ t✝ : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
τ : t.ofCompId ⟶ s
⊢ StructuredArrow.Hom.right τ = StructuredArrow.Hom.right (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))))
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
τ : t.ofIdComp ⟶ s
⊢ τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
τ : t.ofIdComp ⟶ s
⊢ StructuredArrow.Hom.right τ = StructuredArrow.Hom.right (t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c))))
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
s : RightLift f g
τ : s ⟶ t.ofIdComp
⊢ τ = t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
s : RightLift f g
τ : s ⟶ t.ofIdComp
⊢ τ.left = (t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))).left
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ (map (𝟙 F)).map f = f

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).base = f.base

case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x y : ∫ᶜ F
f : x ⟶ y
⊢ ((map (𝟙 F)).map f).fiber = f.fiber ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
X✝ Y✝ : ∫ᶜ F
f : X✝ ⟶ Y✝
⊢ (map (α ≫ β)).map f = (map β).map ((map α).map f)

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : 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

case hfg₂
𝒮 : 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 ⋯
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso } =
    { iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso } ≫ { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }

Tactic:
ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : { of := m X✝.of }.of
⊢ (ConcreteCategory.hom { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso }.iso.hom).toFun x✝ =
    (ConcreteCategory.hom
          ({ iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso } ≫
                { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }).iso.hom).toFun
      x✝
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory 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
⊢ τ₀ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory 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
⊢ StructuredArrow.Hom.right τ₀ =
    StructuredArrow.Hom.right (homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)
Module: Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a✝ b✝ c✝ : Pith B
f✝ g✝ : a✝ ⟶ b✝
h✝ i✝ : b✝ ⟶ c✝
η : f✝ ⟶ g✝
θ : h✝ ⟶ i✝
⊢ { iso := f✝.of ◁ᵢ θ.iso } ≫ { iso := η.iso ▷ᵢ i✝.of } = { iso := η.iso ▷ᵢ h✝.of } ≫ { iso := g✝.of ◁ᵢ θ.iso }

Tactic:
ext

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a✝ b✝ c✝ : Pith B
f✝ g✝ : a✝ ⟶ b✝
h✝ i✝ : b✝ ⟶ c✝
η : f✝ ⟶ g✝
θ : h✝ ⟶ i✝
⊢ ({ iso := f✝.of ◁ᵢ θ.iso } ≫ { iso := η.iso ▷ᵢ i✝.of }).iso.hom =
    ({ iso := η.iso ▷ᵢ h✝.of } ≫ { iso := g✝.of ◁ᵢ θ.iso }).iso.hom
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
⊢ τ₀ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
⊢ StructuredArrow.Hom.right τ₀ =
    StructuredArrow.Hom.right (homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' f (𝟙 b₁) f ⋯ = (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm

Tactic:
ext

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' (𝟙 b₀) f f ⋯ = (λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f

Tactic:
ext

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' (𝟙 b₀) f f ⋯).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
by
  rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f hf).hom, Iso.hom_inv_id_assoc,
    F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf]
  simp

Goal state after: