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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
by
    intro a b f g h η θ
    induction η using Quot.rec
    · induction θ using Quot.rec <;> rfl
    · rfl

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
    (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv

Tactic:
;

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
    (Iso.refl (liftHom F (f✝ ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g✝ ≫ h))).inv
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ 𝟙 (liftHom F g✝ ≫ liftHom F h)

Tactic:
;

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ 𝟙 (liftHom F g✝ ≫ liftHom F h)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ (F.mapComp f g ▷ η.app c ≫
          (α_ (F.map f) (F.map g) (η.app c)).hom ≫
            F.map f ◁ η.naturality g ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ≫
                η.naturality f ▷ G.map g ≫ (α_ (η.app a) (G.map f) (G.map g)).hom) ▷
        h ≫
      (α_ (η.app a) (G.map f ≫ G.map g) h).hom =
    F.mapComp f g ▷ η.app c ▷ h ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
        (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
          F.map f ◁ η.naturality g ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                η.naturality f ▷ G.map g ▷ h ≫
                  (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom

Tactic:
;

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ (F.mapComp f g ▷ η.app c ≫
          (α_ (F.map f) (F.map g) (η.app c)).hom ≫
            F.map f ◁ η.naturality g ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ≫
                η.naturality f ▷ G.map g ≫ (α_ (η.app a) (G.map f) (G.map g)).hom) ▷
        h ≫
      (α_ (η.app a) (G.map f ≫ G.map g) h).hom =
    F.mapComp f g ▷ η.app c ▷ h ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
        (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
          F.map f ◁ η.naturality g ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                η.naturality f ▷ G.map g ▷ h ≫
                  (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ (F.mapId a ▷ η.app a ≫ (λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv) ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
;

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ (F.mapId a ▷ η.app a ≫ (λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv) ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

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 ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  η.naturality f ▷ (G.map g ≫ θ.app c) ≫
                    (η.app a ≫ G.map f) ◁ θ.naturality g ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv

Tactic:
;

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 ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  η.naturality f ▷ (G.map g ≫ θ.app c) ≫
                    (η.app a ≫ G.map f) ◁ θ.naturality g ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv
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
a✝ : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app a✝ = (whiskerRight η h ≫ whiskerLeft g θ).as.app a✝

Tactic:
;

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

Tactic:
;

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
a✝ : B
⊢ (whiskerLeft f Γ ≫ whiskerRight η i).as.app a✝ = (whiskerRight η h ≫ whiskerLeft g Γ).as.app a✝

Tactic:
;

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

Goal state before:
pp: case mk
𝒮 : 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✝ }.base = g.base
hfg₂ : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
;

Goal state after:
case mk
𝒮 : 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✝ }.base = g.base
hfg₂ : eqToHom ⋯ ≫ { base := base✝, fiber := fiber✝ }.fiber = g.fiber
⊢ { base := base✝, fiber := fiber✝ } = g
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

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

Goal state after:
𝒮 : 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
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
b✝ : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app b✝ = (whiskerRight η h ≫ whiskerLeft g θ).as.app b✝

Tactic:
;

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.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)).hom = (mkHom₂ (η.hom ▷ x✝¹.hom) ≫ mkHom₂ (x✝².hom ◁ θ.hom)).hom

Tactic:
;

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

Tactic:
;

Goal state after:
B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f : X ⟶ Y
⊢ (eqToHom ⋯).hom = eqToHom ⋯
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)).hom = (eqToHom ⋯).hom

Tactic:
;

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.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 : F X ⟶ F Y
⊢ (mkHom₂ (eqToHom ⋯)).hom = (eqToHom ⋯).hom

Tactic:
;

Goal state after:
B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f : F X ⟶ F Y
⊢ (mkHom₂ (eqToHom ⋯)).hom = (eqToHom ⋯).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 : 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 only [comp_app, comp_naturality]
      calc
        _ = 𝟙 _ ⊗≫ (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
              θ.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ ι.app b ⊗≫ (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫
              θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [← whisker_exchange]
          bicategory

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

Goal state before:
pp: case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
g : a ⟶ b
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : { base := base✝, fiber := fiber✝ }.base = g.base
hfg₂ : { base := base✝, fiber := fiber✝ }.fiber = g.fiber ≫ eqToHom ⋯
⊢ { base := base✝, fiber := fiber✝ } = g

Tactic:
;

Goal state after:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
g : a ⟶ b
base✝ : a.base ⟶ b.base
fiber✝ : a.fiber ⟶ (F.map base✝.op.toLoc).toFunctor.obj b.fiber
hfg₁ : { base := base✝, fiber := fiber✝ }.base = g.base
hfg₂ : { base := base✝, fiber := fiber✝ }.fiber = g.fiber ≫ eqToHom ⋯
⊢ { base := base✝, fiber := fiber✝ } = g
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
x : { of := m α.of }.of
⊢ (ConcreteCategory.hom { iso := (EquivFunctor.mapEquiv m (𝟙 α).iso.toEquiv).toIso }.iso.hom).toFun x =
    (ConcreteCategory.hom (𝟙 { of := m α.of }).iso.hom).toFun x

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
x : { of := m α.of }.of
⊢ (ConcreteCategory.hom { iso := (EquivFunctor.mapEquiv m (𝟙 α).iso.toEquiv).toIso }.iso.hom).toFun x =
    (ConcreteCategory.hom (𝟙 { of := m α.of }).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)
⊢ 𝟙 (𝟙 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:
;

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)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit

Tactic:
;

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) ⊗≫ s.unit ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit
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).hom ≫ (λ_ u).inv) ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension

Tactic:
;

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).hom ≫ (λ_ u).inv) ▷ h ⊗≫ τ ⊗≫ 𝟙 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 ⊗≫ adj.counit ▷ u) ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 s.extension

Tactic:
;

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 ⊗≫ adj.counit ▷ u) ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ adj.unit ▷ h ⊗≫ (adj.counit ▷ (u ≫ h) ≫ 𝟙 b ◁ τ) ⊗≫ 𝟙 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 ⊗≫ ((u ≫ f) ◁ τ ≫ adj.counit ▷ s.extension) ⊗≫ 𝟙 s.extension =
    𝟙 (u ≫ h) ⊗≫ u ◁ (adj.unit ▷ h ⊗≫ f ◁ τ) ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension

Tactic:
;

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
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 ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension =
    StructuredArrow.Hom.right (homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯)

Tactic:
;

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 ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension =
    StructuredArrow.Hom.right (homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ 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 ⊗≫ f ◁ (t.extension ◁ t.unit ⊗≫ ε ▷ t.extension) ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension)

Tactic:
;

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) ⊗≫ t.unit ⊗≫ f ◁ (t.extension ◁ t.unit ⊗≫ ε ▷ t.extension) ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (f ≫ t.extension) ◁ t.unit) ⊗≫ 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
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)

Tactic:
;

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
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 ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)

Tactic:
;

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) ⊗≫ t.unit ⊗≫ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ t.extension ⊗≫ 𝟙 (f ≫ 𝟙 b ≫ t.extension) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)
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)
⊢ 𝟙 (h ≫ 𝟙 a) ⊗≫ (s.unit ▷ 𝟙 a ≫ (s.lift ≫ u) ◁ adj.unit) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u) =
    s.unit ⊗≫ s.lift ◁ (u ◁ adj.unit ⊗≫ adj.counit ▷ u) ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
;

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)
⊢ 𝟙 (h ≫ 𝟙 a) ⊗≫ (s.unit ▷ 𝟙 a ≫ (s.lift ≫ u) ◁ adj.unit) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u) =
    s.unit ⊗≫ s.lift ◁ (u ◁ adj.unit ⊗≫ adj.counit ▷ u) ⊗≫ 𝟙 (s.lift ≫ u)