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 : 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''
rhs :
  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')
| 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'')

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
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 :
  (((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')

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

Premises used: CategoryTheory.Category.assoc, Equiv.symm_apply_apply, CategoryTheory.Category.comp_id, _private.0.CategoryTheory.Adjunction.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 : 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 :
  (((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'')
| 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'')

Tactic:
rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]

Premises used: CategoryTheory.Category.assoc, Equiv.symm_apply_apply, CategoryTheory.Category.comp_id, _private.0.CategoryTheory.Adjunction.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 : 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''
conv :
  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'')
    (((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'')
⊢ 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'')

Tactic:
conv =>
      rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]

Premises used: CategoryTheory.Category.assoc, Equiv.symm_apply_apply, CategoryTheory.Category.comp_id, _private.0.CategoryTheory.Adjunction.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 : 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''
⊢ 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'')
    (((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'')

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)
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
rw :
  f ≫ g =
    (e X Y : (a : F.obj X ⟶ Y) → X ⟶ (rightAdjointOfEquiv e he).obj Y)
      (F.map f ≫ ((e X' Y).symm : (a : X' ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X' ⟶ Y) g)
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y)
    (((e X Y).symm : (a : X ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X ⟶ Y) (f ≫ g) : F.obj X ⟶ Y)
    (F.map f ≫ ((e X' Y).symm : (a : X' ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X' ⟶ Y) g : F.obj X ⟶ Y)

Tactic:
rw [Equiv.symm_apply_eq]

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
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' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g =
    (e X Y : (a : F.obj X ⟶ Y) → X ⟶ (rightAdjointOfEquiv e he).obj Y)
      (F.map f ≫ ((e X' Y).symm : (a : X' ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X' ⟶ Y) g)

Tactic:
simp [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 : 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)
X : C
Y Y' : D
g : F.obj X ⟶ Y
h : Y ⟶ Y'
⊢ Eq.{v₁ + 1} (α := X ⟶ (rightAdjointOfEquiv e he).obj Y')
    ((e X Y' : (a : F.obj X ⟶ Y') → X ⟶ (rightAdjointOfEquiv e he).obj Y') (g ≫ h) :
      X ⟶ (rightAdjointOfEquiv e he).obj Y')
    ((e X Y : (a : F.obj X ⟶ Y) → X ⟶ (rightAdjointOfEquiv e he).obj Y) g ≫ (rightAdjointOfEquiv e he).map h :
      X ⟶ (rightAdjointOfEquiv e he).obj Y')

Tactic:
simp [← he, reassoc_of% (he'' e)]

Premises used: _private.0.CategoryTheory.Adjunction.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 : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
Z : D
rw :
  Function.Bijective.{v₁ + 1, v₁ + 1} (α := Y ⟶ G.obj Z) (β := X ⟶ G.obj Z)
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
        (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z)
          fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g)
        (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z)) ↔
    Function.Bijective (β := X ⟶ G.obj Z) fun (g : Y ⟶ G.obj Z) ↦ f ≫ g
⊢ (Function.Bijective (β := F.obj X ⟶ Z) fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g) ↔
    Function.Bijective (β := X ⟶ G.obj Z) fun (g : Y ⟶ G.obj Z) ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff' (adj.homEquiv _ _).bijective,
    ← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective]

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', CategoryTheory.Adjunction.homEquiv, Equiv.symm
-- 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
adj : F ⊣ G
X Y : C
f : X ⟶ Y
Z : D
a :
  ∀ (x : Y ⟶ G.obj Z),
    Eq (α := (Y ⟶ G.obj Z) → (X ⟶ G.obj Z))
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
        (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z)
          fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g)
        (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z))
      (CategoryStruct.comp f)
⊢ Function.Bijective.{v₁ + 1, v₁ + 1} (α := Y ⟶ G.obj Z) (β := X ⟶ G.obj Z)
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
        (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z)
          fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g)
        (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z)) ↔
    Function.Bijective (β := X ⟶ G.obj Z) fun (g : Y ⟶ G.obj Z) ↦ f ≫ g

Tactic:
congr!
-- 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
adj : F ⊣ G
X Y : C
f : X ⟶ Y
Z : D
x : Y ⟶ G.obj Z
a :
  ∀ (g : Y ⟶ G.obj Z),
    Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
        (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z)
          fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g)
        (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z) g =
      f ≫ g
⊢ Eq (α := (Y ⟶ G.obj Z) → (X ⟶ G.obj Z))
    (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
      (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) fun (g : F.obj Y ⟶ Z) ↦
        F.map f ≫ g)
      (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z))
    (CategoryStruct.comp f)

Tactic:
ext g
-- 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
adj : F ⊣ G
X Y : C
f : X ⟶ Y
Z : D
x g : Y ⟶ G.obj Z
⊢ Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
      (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) fun (g : F.obj Y ⟶ Z) ↦
        F.map f ≫ g)
      (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z) 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
adj : F ⊣ G
X Y : D
g : X ⟶ Y
Z : C
rw :
  (Function.Bijective (β := Z ⟶ G.obj Y) fun (f : Z ⟶ G.obj X) ↦ f ≫ G.map g) ↔
    Function.Bijective.{v₁ + 1, v₁ + 1} (α := Z ⟶ G.obj X) (β := Z ⟶ G.obj Y)
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
        (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y)
          fun (f : F.obj Z ⟶ X) ↦ f ≫ g)
        (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X))
⊢ (Function.Bijective (β := Z ⟶ G.obj Y) fun (f : Z ⟶ G.obj X) ↦ f ≫ G.map g) ↔
    Function.Bijective (β := F.obj Z ⟶ Y) fun (f : F.obj Z ⟶ X) ↦ f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff' (adj.homEquiv _ _).bijective,
    ← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective]

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff, Function.Bijective.of_comp_iff', CategoryTheory.Adjunction.homEquiv, Equiv.symm
-- 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
adj : F ⊣ G
X Y : D
g : X ⟶ Y
Z : C
a :
  ∀ (x : Z ⟶ G.obj X),
    x ≫ G.map g =
      Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
        (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y)
          fun (f : F.obj Z ⟶ X) ↦ f ≫ g)
        (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) x
⊢ (Function.Bijective (β := Z ⟶ G.obj Y) fun (f : Z ⟶ G.obj X) ↦ f ≫ G.map g) ↔
    Function.Bijective.{v₁ + 1, v₁ + 1} (α := Z ⟶ G.obj X) (β := Z ⟶ G.obj Y)
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
        (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y)
          fun (f : F.obj Z ⟶ X) ↦ f ≫ g)
        (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X))

Tactic:
congr!
-- 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
adj : F ⊣ G
X Y : D
g : X ⟶ Y
Z : C
x : Z ⟶ G.obj X
⊢ x ≫ G.map g =
    Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
      (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y) fun (f : F.obj Z ⟶ X) ↦
        f ≫ g)
      (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) x

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
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : G.IsRightAdjoint
inst_3 : ∀ (X : D), IsIso (Y := (G.leftAdjoint ⋙ G).obj X) (NatTrans.app (unit (ofIsRightAdjoint G)) X)
inst_4 : ∀ (Y : C), IsIso (X := (G ⋙ G.leftAdjoint).obj Y) (NatTrans.app (counit (ofIsRightAdjoint G)) Y)
⊢ G.IsEquivalence

Tactic:
(Adjunction.ofIsRightAdjoint G).toEquivalence.isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, CategoryTheory.Adjunction.toEquivalence, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ e.inverse.IsLeftAdjoint

Tactic:
e.symm.isLeftAdjoint_functor

Premises used: CategoryTheory.Equivalence.isLeftAdjoint_functor, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ e.functor.IsRightAdjoint

Tactic:
e.symm.isRightAdjoint_inverse

Premises used: CategoryTheory.Equivalence.isRightAdjoint_inverse, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ Eq (α := Adjunction.{v₁, v₁, u₁, u₁} (C := C) (functor refl) (inverse refl)) (toAdjunction refl) Adjunction.id

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.id, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
e' : Equivalence.{v₂, v_1, u₂, u_1} D E
⊢ (e.trans e').toAdjunction = e.toAdjunction.comp e'.toAdjunction

Tactic:
rfl

Premises used: CategoryTheory.Adjunction.mk', CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, CategoryTheory.Adjunction.comp, rfl
-- 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
inst_2 : F.IsEquivalence
⊢ F.IsLeftAdjoint

Tactic:
F.asEquivalence.isLeftAdjoint_functor

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isLeftAdjoint_functor
-- 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
inst_2 : F.IsEquivalence
⊢ F.IsRightAdjoint

Tactic:
F.asEquivalence.isRightAdjoint_functor

Premises used: CategoryTheory.Equivalence.isRightAdjoint_functor, CategoryTheory.Functor.asEquivalence
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
⊢ initial.to B' = g'

Tactic:
have : initial.to _ = g' := by cat_disch
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
change : CommaMorphism.right (initial.to B') = g
⊢ (fun (f : A ⟶ G.obj B) ↦
        (CommaMorphism.right (initial.to (StructuredArrow.mk f)) :
          Comma.right.{0, v₂, v₁, 0, u₂, u₁} (A := Discrete PUnit.{1}) (T := C) (L := Functor.fromPUnit A) (R := G)
              (⊥_ StructuredArrow A G) ⟶
            (StructuredArrow.mk f).right))
      ((fun (g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B) ↦
          StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
        g) =
    g

Tactic:
change CommaMorphism.right (initial.to B') = _

Premises used: CategoryTheory.Limits.initial.to, CategoryTheory.CommaMorphism.right
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
rw : g'.right = g
⊢ CommaMorphism.right (initial.to B') = g

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
⊢ g'.right = g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
B' : StructuredArrow A G := StructuredArrow.mk f
⊢ (fun (g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B) ↦
        StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
      ((fun (f : A ⟶ G.obj B) ↦
          (CommaMorphism.right (initial.to (StructuredArrow.mk f)) :
            Comma.right.{0, v₂, v₁, 0, u₂, u₁} (A := Discrete PUnit.{1}) (T := C) (L := Functor.fromPUnit A) (R := G)
                (⊥_ StructuredArrow A G) ⟶
              (StructuredArrow.mk f).right))
        f) =
    f

Tactic:
apply (CommaMorphism.w (initial.to B')).symm.trans (Category.id_comp _)

Premises used: CategoryTheory.CommaMorphism.w, CategoryTheory.Limits.initial.to, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
x : C
x_1 : D
⊢ ∀ (Y' : D) (g : x_1 ⟶ Y')
    (h : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := x) (T := G) (⊥_ StructuredArrow x G) ⟶ x_1),
    Eq.{v₁ + 1} (α := x ⟶ G.obj Y')
      (((leftAdjointOfStructuredArrowInitialsAux G x Y' :
              Equiv.{v₂ + 1, v₁ + 1}
                (StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := x) (T := G) (⊥_ StructuredArrow x G) ⟶ Y')
                (x ⟶ G.obj Y')) :
            (a : (⊥_ StructuredArrow x G).right ⟶ Y') → x ⟶ G.obj Y')
          (h ≫ g) :
        x ⟶ G.obj Y')
      (((leftAdjointOfStructuredArrowInitialsAux G x x_1 :
                Equiv.{v₂ + 1, v₁ + 1}
                  (StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := x) (T := G) (⊥_ StructuredArrow x G) ⟶ x_1)
                  (x ⟶ G.obj x_1)) :
              (a : (⊥_ StructuredArrow x G).right ⟶ x_1) → x ⟶ G.obj x_1)
            h ≫
          G.map g :
        x ⟶ G.obj Y')

Tactic:
simp