Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
unit✝¹ : 𝟭 C ⟶ F ⋙ G
counit✝¹ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝¹ : ∀ (X : C), F.map (unit✝¹.app X) ≫ counit✝¹.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝¹ : ∀ (Y : D), unit✝¹.app (G.obj Y) ≫ G.map (counit✝¹.app Y) = 𝟙 (G.obj Y)
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.unit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit
h' :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.counit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit
⊢ { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
      right_triangle_components := right_triangle_components✝¹ } =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
unit✝¹ : 𝟭 C ⟶ F ⋙ G
counit✝¹ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝¹ : ∀ (X : C), F.map (unit✝¹.app X) ≫ counit✝¹.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝¹ : ∀ (Y : D), unit✝¹.app (G.obj Y) ≫ G.map (counit✝¹.app Y) = 𝟙 (G.obj Y)
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.unit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit
h' :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.counit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit
⊢ { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
      right_triangle_components := right_triangle_components✝¹ } =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ }