awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F F' : Functor.{v₁, v₂, u₁, u₂} C D
iso : F ≅ F'
X : C
Y : D
g : F'.obj X ⟶ Y
⊢ (fun (f : F.obj X ⟶ Y) ↦ iso.inv.app X ≫ f) ((fun (g : F'.obj X ⟶ Y) ↦ iso.hom.app X ≫ g) g) = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G_1 G G' : Functor.{v₂, v₁, u₂, u₁} D C
iso : G ≅ G'
X : C
Y : D
f : X ⟶ G.obj Y
⊢ (fun (g : X ⟶ G'.obj Y) ↦ g ≫ iso.inv.app Y) ((fun (f : X ⟶ G.obj Y) ↦ f ≫ iso.hom.app Y) f) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G_1 G G' : Functor.{v₂, v₁, u₂, u₁} D C
iso : G ≅ G'
X : C
Y : D
g : X ⟶ G'.obj Y
⊢ (fun (f : X ⟶ G.obj Y) ↦ f ≫ iso.hom.app Y) ((fun (g : X ⟶ G'.obj Y) ↦ g ≫ iso.inv.app Y) g) = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ H
iso : F ≅ G
X : C
simp : iso.inv.app X ≫ F.map (adj.unit.app X) ≫ F.map (H.map (iso.hom.app X)) ≫ adj.counit.app (G.obj X) = 𝟙 (G.obj X)
⊢ G.map ((adj.unit ≫ whiskerRight iso.hom H).app X) ≫ (H.whiskerLeft iso.inv ≫ adj.counit).app (G.obj X) = 𝟙 (G.obj X)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, NatTrans.comp_app, Functor.whiskerRight_app,
      Functor.map_comp, Functor.whiskerLeft_app, Category.assoc, NatTrans.naturality_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ H
iso : F ≅ G
X : C
⊢ iso.inv.app X ≫ F.map (adj.unit.app X) ≫ F.map (H.map (iso.hom.app X)) ≫ adj.counit.app (G.obj X) = 𝟙 (G.obj X)

Tactic:
simp [← Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ H
iso : F ≅ G
⊢ ∀ (Y : D),
    (adj.unit ≫ whiskerRight iso.hom H).app (H.obj Y) ≫ H.map ((H.whiskerLeft iso.inv ≫ adj.counit).app Y) = 𝟙 (H.obj Y)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ H
iso : F ≅ G
X : C
Y : D
f : G.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ H.obj Y)
    (((adj.ofNatIsoLeft iso).homEquiv X Y : (a : G.obj X ⟶ Y) → X ⟶ H.obj Y) f : X ⟶ H.obj Y)
    ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ H.obj Y) (iso.hom.app X ≫ f) : X ⟶ H.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ H
iso : F ≅ G
X : C
Y : D
f : X ⟶ H.obj Y
⊢ Eq.{v₂ + 1} (α := G.obj X ⟶ Y)
    ((((adj.ofNatIsoLeft iso).homEquiv X Y).symm : (a : X ⟶ H.obj Y) → G.obj X ⟶ Y) f : G.obj X ⟶ Y)
    (iso.inv.app X ≫ ((adj.homEquiv X Y).symm : (a : X ⟶ H.obj Y) → F.obj X ⟶ Y) f : G.obj X ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
iso : G ≅ H
X : C
⊢ F.map ((adj.unit ≫ F.whiskerLeft iso.hom).app X) ≫ (whiskerRight iso.inv F ≫ adj.counit).app (F.obj X) = 𝟙 (F.obj X)

Tactic:
simp [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
iso : G ≅ H
Y : D
simp : iso.inv.app Y ≫ iso.hom.app Y = 𝟙 (H.obj Y)
⊢ (adj.unit ≫ F.whiskerLeft iso.hom).app (H.obj Y) ≫ H.map ((whiskerRight iso.inv F ≫ adj.counit).app Y) = 𝟙 (H.obj Y)

Tactic:
simp only [id_obj, comp_obj, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app, map_comp,
      assoc, ← iso.hom.naturality_assoc, ← iso.hom.naturality, unit_naturality_assoc,
      adj.right_triangle_components_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Adjunction.right_triangle_components_assoc, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₁, u₂, u₁} D C
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
iso : G ≅ H
Y : D
⊢ iso.inv.app Y ≫ iso.hom.app Y = 𝟙 (H.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
iso : G ≅ H
X : C
Y : D
f : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ H.obj Y)
    (((adj.ofNatIsoRight iso).homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ H.obj Y) f : X ⟶ H.obj Y)
    ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f ≫ iso.hom.app Y : X ⟶ H.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
iso : G ≅ H
X : C
Y : D
f : X ⟶ H.obj Y
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y)
    ((((adj.ofNatIsoRight iso).homEquiv X Y).symm : (a : X ⟶ H.obj Y) → F.obj X ⟶ Y) f : F.obj X ⟶ Y)
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) (f ≫ iso.inv.app Y) : F.obj X ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
E : Type u₃
ℰ : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
I : Functor.{v₃, v₂, u₃, u₂} E D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
X : C
⊢ (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X))

Tactic:
simp [Adjunction.comp]

Premises used: CategoryTheory.Adjunction.comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
E : Type u₃
ℰ : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
I : Functor.{v₃, v₂, u₃, u₂} E D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
X : E
⊢ (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X

Tactic:
simp [Adjunction.comp]

Premises used: CategoryTheory.Adjunction.comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
E : Type u₃
ℰ : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
I : Functor.{v₃, v₂, u₃, u₂} E D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
⊢ (adj₁.comp adj₂).homEquiv = fun (x : C) (x_1 : E) ↦
    Equiv.trans (adj₂.homEquiv (F.obj x) x_1) (adj₁.homEquiv x (I.obj x_1))

Tactic:
mk'_homEquiv _

Premises used: Equiv.trans, CategoryTheory.Adjunction.mk'_homEquiv, CategoryTheory.Adjunction.comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
rw :
  Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))
⊢ Eq.{v₂ + 1} (α := F_obj X ⟶ F_obj Z)
    ((Equiv.symm (e X (F_obj Z)) : (a : X ⟶ G.obj (F_obj Z)) → F_obj X ⟶ F_obj Z)
        ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))) :
      F_obj X ⟶ F_obj Z)
    (CategoryStruct.comp (Y := F_obj Y)
        ((Equiv.symm (e X (F_obj Y)) : (a : X ⟶ G.obj (F_obj Y)) → F_obj X ⟶ F_obj Y)
          (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y))))
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))) :
      F_obj X ⟶ F_obj Z)

Tactic:
rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_eq
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
rhs :
  CategoryStruct.comp (Y := G.obj (F_obj Y))
    (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
    (G.map
      ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
        (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))))
| Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))

Tactic:
rhs
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
rw : f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))
| CategoryStruct.comp (Y := G.obj (F_obj Y))
    (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
    (G.map
      ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
        (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))))

Tactic:
rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]

Premises used: CategoryTheory.Category.assoc, Equiv.apply_symm_apply, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
rw : f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))
| Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))

Tactic:
rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]

Premises used: CategoryTheory.Category.assoc, Equiv.apply_symm_apply, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
conv :
  Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
⊢ Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (CategoryStruct.comp (Y := G.obj (F_obj Y))
      (f ≫ (e Y (F_obj Y) : (a : F_obj Y ⟶ F_obj Y) → Y ⟶ G.obj (F_obj Y)) (𝟙 (F_obj Y)))
      (G.map
        ((Equiv.symm (e Y (F_obj Z)) : (a : Y ⟶ G.obj (F_obj Z)) → F_obj Y ⟶ F_obj Z)
          (f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z))))))

Tactic:
conv =>
      rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]

Premises used: CategoryTheory.Category.assoc, Equiv.apply_symm_apply, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X Y Z : C
f : X ⟶ Y
f' : Y ⟶ Z
⊢ Eq (α := X ⟶ G.obj (F_obj Z))
    ((f ≫ f') ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))
    (f ≫ f' ≫ (e Z (F_obj Z) : (a : F_obj Z ⟶ F_obj Z) → Z ⟶ G.obj (F_obj Z)) (𝟙 (F_obj Z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X' X_1 : C
Y_1 : D
f_1 : X' ⟶ X_1
g_1 : X_1 ⟶ G.obj Y_1
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
rw :
  f ≫ G.map g = (e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f) ≫ G.map g
⊢ Eq.{v₂ + 1} (α := F_obj X ⟶ Y') (((e X Y').symm : (a : X ⟶ G.obj Y') → F_obj X ⟶ Y') (f ≫ G.map g) : F_obj X ⟶ Y')
    (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f ≫ g : F_obj X ⟶ Y')

Tactic:
rw [Equiv.symm_apply_eq, he]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X' X_1 : C
Y_1 : D
f_1 : X' ⟶ X_1
g_1 : X_1 ⟶ G.obj Y_1
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f) ≫ G.map g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'),
    Eq.{v₂ + 1} (α := F_obj X ⟶ Y') (((e X Y').symm : (a : X ⟶ G.obj Y') → F_obj X ⟶ Y') (f ≫ G.map g) : F_obj X ⟶ Y')
      (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f ≫ g : F_obj X ⟶ Y')

Tactic:
have {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
            (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
          rw [Equiv.symm_apply_eq, he]; simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this :
  ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'),
    Eq.{v₂ + 1} (α := F_obj X ⟶ Y') (((e X Y').symm : (a : X ⟶ G.obj Y') → F_obj X ⟶ Y') (f ≫ G.map g) : F_obj X ⟶ Y')
      (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f ≫ g : F_obj X ⟶ Y')
⊢ Eq.{v₂ + 1} (α := (leftAdjointOfEquiv e he).obj X' ⟶ Y)
    (((e X' Y).symm : (a : X' ⟶ G.obj Y) → (leftAdjointOfEquiv e he).obj X' ⟶ Y) (f ≫ g) :
      (leftAdjointOfEquiv e he).obj X' ⟶ Y)
    ((leftAdjointOfEquiv e he).map f ≫ ((e X Y).symm : (a : X ⟶ G.obj Y) → (leftAdjointOfEquiv e he).obj X ⟶ Y) g :
      (leftAdjointOfEquiv e he).obj X' ⟶ Y)

Tactic:
simp [← this, ← he]
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
rw : f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) (((e X Y).symm : (a : X ⟶ G_obj Y) → F.obj X ⟶ Y) g) = f ≫ g
⊢ Eq (α := F.obj X' ⟶ Y) (F.map f ≫ ((e X Y).symm : (a : X ⟶ G_obj Y) → F.obj X ⟶ Y) g)
    (((e X' Y).symm : (a : X' ⟶ G_obj Y) → F.obj X' ⟶ Y) (f ≫ g))

Tactic:
rw [Equiv.eq_symm_apply, he]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) (((e X Y).symm : (a : X ⟶ G_obj Y) → F.obj X ⟶ Y) g) = f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
rw :
  Eq.{v₂ + 1} (α := F.obj (G_obj Y) ⟶ Y'')
    ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g' :
      F.obj (G_obj Y) ⟶ Y'')
    (CategoryStruct.comp (Y := F.obj (G_obj Y'))
        (F.map
          ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
            ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
        ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g') :
      F.obj (G_obj Y) ⟶ Y'')
⊢ Eq.{v₁ + 1} (α := G_obj Y ⟶ G_obj Y'')
    ((e (G_obj Y) Y'' : (a : F.obj (G_obj Y) ⟶ Y'') → G_obj Y ⟶ G_obj Y'')
        ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g') :
      G_obj Y ⟶ G_obj Y'')
    (CategoryStruct.comp (Y := G_obj Y')
        ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
          ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g))
        ((e (G_obj Y') Y'' : (a : F.obj (G_obj Y') ⟶ Y'') → G_obj Y' ⟶ G_obj Y'')
          ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g')) :
      G_obj Y ⟶ G_obj Y'')

Tactic:
rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, _private.0.CategoryTheory.Adjunction.he'', Equiv.eq_symm_apply