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

Goal state before:
pp: case comp_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ h✝ : Hom a✝ b✝
i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
⊢ liftHom₂ F (Hom₂.whisker_right i✝ (η✝.vcomp θ✝)) =
    liftHom₂ F ((Hom₂.whisker_right i✝ η✝).vcomp (Hom₂.whisker_right i✝ θ✝))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case whisker_right_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.id b✝) η✝) =
    liftHom₂ F ((Hom₂.right_unitor f✝).vcomp (η✝.vcomp (Hom₂.right_unitor_inv g✝)))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case whisker_right_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ f'✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
η✝ : Hom₂ f✝ f'✝
⊢ liftHom₂ F (Hom₂.whisker_right (g✝.comp h✝) η✝) =
    liftHom₂ F
      ((Hom₂.associator_inv f✝ g✝ h✝).vcomp
        ((Hom₂.whisker_right h✝ (Hom₂.whisker_right g✝ η✝)).vcomp (Hom₂.associator f'✝ g✝ h✝)))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case whisker_assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ g'✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ g'✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.whisker_right h✝ (Hom₂.whisker_left f✝ η✝)) =
    liftHom₂ F
      ((Hom₂.associator f✝ g✝ h✝).vcomp
        ((Hom₂.whisker_left f✝ (Hom₂.whisker_right h✝ η✝)).vcomp (Hom₂.associator_inv f✝ g'✝ h✝)))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case whisker_exchange
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ : Hom a✝ b✝
h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F ((Hom₂.whisker_left f✝ θ✝).vcomp (Hom₂.whisker_right i✝ η✝)) =
    liftHom₂ F ((Hom₂.whisker_right h✝ η✝).vcomp (Hom₂.whisker_left g✝ θ✝))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case associator_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F ((Hom₂.associator f✝ g✝ h✝).vcomp (Hom₂.associator_inv f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id ((f✝.comp g✝).comp h✝))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case associator_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F ((Hom₂.associator_inv f✝ g✝ h✝).vcomp (Hom₂.associator f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id (f✝.comp (g✝.comp h✝)))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case left_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F ((Hom₂.left_unitor f✝).vcomp (Hom₂.left_unitor_inv f✝)) = liftHom₂ F (Hom₂.id ((Hom.id a✝).comp f✝))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case left_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F ((Hom₂.left_unitor_inv f✝).vcomp (Hom₂.left_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case right_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F ((Hom₂.right_unitor f✝).vcomp (Hom₂.right_unitor_inv f✝)) = liftHom₂ F (Hom₂.id (f✝.comp (Hom.id b✝)))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F ((Hom₂.right_unitor_inv f✝).vcomp (Hom₂.right_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ liftHom₂ F
      ((Hom₂.whisker_right i✝ (Hom₂.associator f✝ g✝ h✝)).vcomp
        ((Hom₂.associator f✝ (g✝.comp h✝) i✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.associator g✝ h✝ i✝)))) =
    liftHom₂ F ((Hom₂.associator (f✝.comp g✝) h✝ i✝).vcomp (Hom₂.associator f✝ g✝ (h✝.comp i✝)))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F ((Hom₂.associator f✝ (Hom.id b✝) g✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.left_unitor g✝))) =
    liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.right_unitor f✝))

Tactic:
dsimp [liftHom₂]; cat_disch

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv
Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), (app a).hom ▷ G.map f ≫ θ.naturality f = η.naturality f ≫ F.map f ◁ (app b).hom
a b : B
f : a ⟶ b
⊢ (app a).inv ▷ G.map f ≫ η.naturality f = θ.naturality f ≫ F.map f ◁ (app b).inv
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ (η.naturality f).hom = (θ.naturality f).hom ≫ (app a).inv ▷ G.map f

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ (η.naturality f).hom = (θ.naturality f).hom ≫ (app a).inv ▷ G.map f
Module: Mathlib.CategoryTheory.Bicategory.Modification.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ (η.naturality f).hom = (θ.naturality f).hom ≫ (app a).inv ▷ G.map f

Tactic:
simpa using

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ (η.naturality f).hom = (θ.naturality f).hom ≫ (app a).inv ▷ G.map f
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f g : a ⟶ b
hfg : f = g
⊢ ∃ (hfg : f.base = g.base), eqToHom ⋯ ≫ f.fiber = g.fiber

Tactic:
subst hfg; simp

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✝⁶ 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:
simpa using

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✝
⊢ x✝³.hom ◁ θ.hom ≫ η.hom ▷ x✝.hom = η.hom ▷ x✝¹.hom ≫ x✝².hom ◁ θ.hom
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
    · simp
    · simp [← NatTrans.naturality_assoc, F.mapComp_assoc_right_inv_app, Strict.associator_eqToIso]

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

Tactic:
simpa using

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 τ₀
⊢ adj.unit ▷ h ≫ (α_ f u h).hom ≫ f ◁ τ = 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
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))
⊢ leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv

Tactic:
simpa using

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))
⊢ t.unit ▷ f ≫ (α_ f t.extension f).hom ≫ f ◁ ε = (λ_ f).hom ≫ (ρ_ f).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)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
⊢ h ◁ adj.unit ⊗≫ τ ▷ u = s.unit

Tactic:
simpa using

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
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
⊢ h ◁ adj.unit ≫ (α_ h f u).inv ≫ τ ▷ u = s.unit
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))
⊢ rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv

Tactic:
simpa using

Goal state after:
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))
⊢ u ◁ t.unit ≫ (α_ u t.lift u).inv ≫ ε ▷ u = (ρ_ u).hom ≫ (λ_ u).inv
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σ
⊢ t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ

Tactic:
simpa using

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)
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σ
⊢ t.extension ◁ η' ≫ (α_ t.extension h u).inv ≫ σ ▷ u = (ρ_ t.extension).hom ≫ τ
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 ◁ η' ≫ (α_ g h u).inv) ≫ ((t.unit ▷ h ≫ (α_ f t.extension h).hom) ≫ f ◁ σ) ▷ u =
    (g ◁ η' ≫ (α_ g h u).inv) ≫ s.unit ▷ u

Tactic:
calc _
        _ = (g ◁ η' ≫ t.unit ▷ (h ≫ u)) ⊗≫ f ◁ σ ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = t.unit ▷ (𝟙 c) ⊗≫ f ◁ (t.extension ◁ η' ⊗≫ σ ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = (ρ_ g).hom ≫ t.unit ≫ f ◁ H.desc sτ ≫ (α_ f s.extension u).inv := by
          rw [Hσ]
          dsimp only [τ]
          bicategory
        _ = _ := by
          rw [IsKan.fac_assoc]
          dsimp only [StructuredArrow.mk_right, StructuredArrow.mk_hom_eq_self, sτ]
          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)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
⊢ t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit

Tactic:
simpa using

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 τ₀'
⊢ t.unit ▷ h ≫ (α_ f t.extension h).hom ≫ f ◁ τ' = s'.unit
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
i : I
X Y✝¹ : C i
f : X ⟶ Y✝¹
Y✝ : C i
g : Y✝¹ ⟶ Y✝
⊢ descMap F ⟨i, X⟩ ⟨i, Y✝⟩ (SigmaHom.mk f ≫ SigmaHom.mk g) =
    descMap F ⟨i, X⟩ ⟨i, Y✝¹⟩ (SigmaHom.mk f) ≫ descMap F ⟨i, Y✝¹⟩ ⟨i, Y✝⟩ (SigmaHom.mk g)

Tactic:
apply (F i).map_comp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝ : Cat
x : ConnectedComponents ↑x✝
⊢ (ConcreteCategory.hom (↾(𝟙 x✝).toFunctor.mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (𝟙 (ConnectedComponents ↑x✝))).toFun x

Tactic:
simpa using

Goal state after:
X : Type u
C : Cat
x✝ : Cat
x : ConnectedComponents ↑x✝
⊢ (𝟭 ↑x✝).mapConnectedComponents x = x
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
x : ConnectedComponents ↑X✝
⊢ (ConcreteCategory.hom (↾(x✝¹ ≫ x✝).toFunctor.mapConnectedComponents)).toFun x =
    (ConcreteCategory.hom (↾x✝¹.toFunctor.mapConnectedComponents ≫ ↾x✝.toFunctor.mapConnectedComponents)).toFun x

Tactic:
simpa using

Goal state after:
X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
x : ConnectedComponents ↑X✝
⊢ (x✝¹.toFunctor ⋙ x✝.toFunctor).mapConnectedComponents x =
    x✝.toFunctor.mapConnectedComponents (x✝¹.toFunctor.mapConnectedComponents x)
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X Y : Pointed
f : X ⟶ Y
a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫ (Pointed.Iso.mk (Equiv.optionSubtypeNe Y.point) ⋯).hom).toFun a =
    ((Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯).hom ≫ (𝟭 Pointed).map f).toFun a

Tactic:
by
        obtain _ | ⟨a, ha⟩ := a
        · exact f.map_point.symm
        simp_all [Equiv.optionSubtypeNe, Equiv.optionSubtype,
          Option.casesOn'_eq_elim, Part.elim_toOption]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ f ≫ Δ = Δ ≫ (f ⊗ₘ f)

Tactic:
simp +instances

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ fst A A = lift (𝟙 A) (𝟙 A) ≫ fst A A

Tactic:
simpa using

Goal state after:
case h_fst
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ fst A A = 𝟙 A
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ snd A A = lift (𝟙 A) (𝟙 A) ≫ snd A A

Tactic:
simpa using

Goal state after:
case h_snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ ≫ snd A A = 𝟙 A
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip

Tactic:
simpa using

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ Functor.whiskerRight (pullbackComp f g).hom (map (f ≫ g)) ≫ (mapPullbackAdj (f ≫ g)).counit =
    (mapPullbackAdj (f ≫ g)).counit

Tactic:
by
  rw [pullbackComp, Adjunction.rightAdjointUniq_hom_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMultiplicative
h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (f ⊗ₘ g)
X x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
hg : W g
⊢ W (X ◁ g)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMultiplicative
h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (f ⊗ₘ g)
X x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
hg : W g
⊢ W (X ◁ g)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMultiplicative
h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (f ⊗ₘ g)
X₁✝ X₂✝ : C
f : X₁✝ ⟶ X₂✝
hf : W f
Y : C
⊢ W (f ▷ Y)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMultiplicative
h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (f ⊗ₘ g)
X₁✝ X₂✝ : C
f : X₁✝ ⟶ X₂✝
hf : W f
Y : C
⊢ W (f ▷ Y)