mathlib-initiative/mathlib-tactics huggingface dataset:
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

Goal state after:
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 ≫
      (α_ (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
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 ◁ Γ.as.app b ▷ ι.app b ≫ ((θ ≫ ι).naturality f).hom =
    ((η ≫ ι).naturality f).hom ≫ Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
dsimp

Goal state after:
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 ◁ Γ.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
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

Goal state after:
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 ≫
      (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f
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 ◁ Γ.as.app b ▷ ι.app b ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
dsimp

Goal state after:
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 ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        θ.naturality f ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
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 : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
← whisker_exchange

Goal state after:
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 ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (η.app a ◁ ι.naturality f ≫ Γ.as.app a ▷ (ι.app a ≫ H.map f)) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 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

Tactic:
dsimp

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

Goal state before:
pp: 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

Tactic:
dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
        (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
          η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g

Tactic:
← whisker_exchange

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
        ((F.map f ≫ η.app b) ◁ θ.naturality g ≫ η.naturality f ▷ (θ.app b ≫ H.map g)) ⊗≫
          η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
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 ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (map α ⋙ map β).map f

Tactic:
dsimp

Goal state after:
𝒮 : 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 (α ≫ β)).obj Y✝) = 𝟙 ((map (α ≫ β)).obj X✝) ≫ (map β).map ((map α).map f)
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

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

Tactic:
dsimp

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

Goal state before:
pp: 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

Tactic:
dsimp

Goal state after:
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 ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (map α ⋙ map β).map f

Tactic:
dsimp

Goal state after:
𝒮 : 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 (α ≫ β)).obj Y✝) = 𝟙 ((map (α ≫ β)).obj X✝) ≫ (map β).map ((map α).map f)
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)
⊢ 𝟙 (𝟙 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:
← whisker_exchange

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)
⊢ 𝟙 (𝟙 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)
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
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension

Tactic:
← whisker_exchange

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
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ 𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ ((u ≫ f) ◁ τ ≫ adj.counit ▷ s.extension) ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := H'.desc (LeftExtension.mk (𝟙 b) ((λ_ f).hom ≫ (ρ_ f).inv))
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (f ≫ t.extension)) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)
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
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
rw [whisker_exchange]; bicategory

Goal state after:
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
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift =
    StructuredArrow.Hom.right (homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯)

Tactic:
by
          rw [hτ]; dsimp only [StructuredArrow.homMk_right]

Goal state after:
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.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp f (𝟙 b₁)).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom

Tactic:
dsimp

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.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
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.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp (𝟙 b₀) f).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom

Tactic:
dsimp

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.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
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
  rw [mapComp']
  dsimp
  rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
rw [whisker_exchange]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s : LeftExtension f (g ≫ h)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
Hσ : t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ
⊢ (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u) =
    t.unit ▷ 𝟙 c ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 ((f ≫ s.extension) ≫ u)

Tactic:
rw [whisker_exchange]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }

Tactic:
let f : ∀ x, Zigzag x j₂ → (ConnectedComponents.mk j₂).Component :=
    fun x h => ⟨x, Quotient.sound' h⟩

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ (t.unit ▷ 𝟙 c ≫ (f ≫ t.extension) ◁ η') ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)

Tactic:
← whisker_exchange

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ τ' ▷ u =
    𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u)
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ (fun f ↦ ⟨fun a ↦ (f a).Dom, f.asSubtype⟩) ((fun f x ↦ { Dom := f.fst x, get := fun h ↦ f.snd ⟨x, h⟩ }) ⟨p, f⟩) =
    ⟨p, f⟩

Tactic:
dsimp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ ⟨fun a ↦ p a, asSubtype fun x ↦ { Dom := p x, get := fun h ↦ f ⟨x, h⟩ }⟩ = ⟨p, f⟩
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedFst).obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦
            { hom := { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToTwoPFst.map f ≫
      { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦
              {
                hom :=
                  { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
ext (_ | _) : 4 <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦
            { hom := { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToTwoPSnd.map f ≫
      { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦
              {
                hom :=
                  { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
ext (_ | _) : 4 <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
⊢ (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)).Final

Tactic:
apply final_of_natIso (F := F'')

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := ⋯
sB : B ≌ AsSmall B := ⋯
sT : T ≌ AsSmall T := ⋯
L' : AsSmall A ⥤ AsSmall T := ⋯
R' : AsSmall B ⥤ AsSmall T := ⋯
b : AsSmall B
x : AsSmall T := ⋯
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x := ⋯
⊢ F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)