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
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : F.map f ≫ g = h ≫ k
rw :
  Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k : X' ⟶ G.obj Y')
rw₁ :
  Eq.{v₁ + 1} (α := X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (F.map f ≫ g) : X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
rw₂ rw₃ :
  Eq.{v₁ + 1} (α := X' ⟶ G.obj Y') ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
    ((adj.homEquiv X' Y' : (a : F.obj X' ⟶ Y') → X' ⟶ G.obj Y') (h ≫ k) : X' ⟶ G.obj Y')
⊢ Eq (α := X' ⟶ G.obj Y') (f ≫ (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y') g)
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k)

Tactic:
rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_right, CategoryTheory.Adjunction.homEquiv_naturality_left
-- 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' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
rw :
  Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k : F.obj X' ⟶ Y')
rw₁ :
  Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (f ≫ g) : F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
rw₂ rw₃ :
  Eq.{v₂ + 1} (α := F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
    (((adj.homEquiv X' Y').symm : (a : X' ⟶ G.obj Y') → F.obj X' ⟶ Y') (h ≫ G.map k) : F.obj X' ⟶ Y')
⊢ Eq (α := F.obj X' ⟶ Y') (F.map f ≫ ((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') g)
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k)

Tactic:
rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_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' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w :
  Eq (α := X' ⟶ G.obj Y') (f ≫ (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y') g)
    ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) h ≫ G.map k)
⊢ F.map f ≫ g = h ≫ k

Tactic:
simpa only [Equiv.symm_apply_apply]
      using homEquiv_naturality_right_square adj _ _ _ _ w

Premises used: Equiv.symm_apply_apply, CategoryTheory.Adjunction.homEquiv_naturality_right_square
-- 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' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w :
  Eq (α := F.obj X' ⟶ Y') (F.map f ≫ ((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') g)
    (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y) h ≫ k)
⊢ f ≫ g = h ≫ G.map k

Tactic:
simpa only [Equiv.apply_symm_apply]
      using homEquiv_naturality_left_square adj _ _ _ _ w

Premises used: CategoryTheory.Adjunction.homEquiv_naturality_left_square, Equiv.apply_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 : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
w : ∀ (x : C), (whiskerRight adj.unit F ≫ F.whiskerLeft adj.counit).app x = NatTrans.app (𝟙 (𝟭 C ⋙ F)) x
⊢ whiskerRight adj.unit F ≫ F.whiskerLeft adj.counit = 𝟙 (𝟭 C ⋙ F)

Tactic:
ext
-- 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 : C
⊢ (whiskerRight adj.unit F ≫ F.whiskerLeft adj.counit).app x = NatTrans.app (𝟙 (𝟭 C ⋙ F)) 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
w : ∀ (x : D), (G.whiskerLeft adj.unit ≫ whiskerRight adj.counit G).app x = NatTrans.app (𝟙 (G ⋙ 𝟭 C)) x
⊢ G.whiskerLeft adj.unit ≫ whiskerRight adj.counit G = 𝟙 (G ⋙ 𝟭 C)

Tactic:
ext
-- 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 : D
⊢ (G.whiskerLeft adj.unit ≫ whiskerRight adj.counit G).app x = NatTrans.app (𝟙 (G ⋙ 𝟭 C)) 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
⊢ F.map (G.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f

Tactic:
adj.counit.naturality f

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.naturality
-- 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
⊢ adj.unit.app X ≫ G.map (F.map f) = f ≫ adj.unit.app Y

Tactic:
(adj.unit.naturality f).symm

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.NatTrans.naturality, Eq.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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : adj.unit.app A ≫ G.map f = g
⊢ f = F.map g ≫ adj.counit.app B

Tactic:
simp [← h]
-- 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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : f = F.map g ≫ adj.counit.app B
⊢ adj.unit.app A ≫ G.map f = g

Tactic:
simp [h]
-- 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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = adj.unit.app A ≫ G.map f
⊢ F.map g ≫ adj.counit.app B = f

Tactic:
simp [h]
-- 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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : F.map g ≫ adj.counit.app B = f
⊢ g = adj.unit.app A ≫ G.map f

Tactic:
simp [← h]
-- 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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
⊢ (adj.homEquiv A B : (a : F.obj A ⟶ B) → A ⟶ G.obj B) f = g ↔
    f = ((adj.homEquiv A B).symm : (a : A ⟶ G.obj B) → F.obj A ⟶ B) g

Tactic:
unit_comp_map_eq_iff adj f g

Premises used: CategoryTheory.Adjunction.unit_comp_map_eq_iff
-- 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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
⊢ g = (adj.homEquiv A B : (a : F.obj A ⟶ B) → A ⟶ G.obj B) f ↔
    ((adj.homEquiv A B).symm : (a : A ⟶ G.obj B) → F.obj A ⟶ B) g = f

Tactic:
eq_unit_comp_map_iff adj f g

Premises used: CategoryTheory.Adjunction.eq_unit_comp_map_iff
-- 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' X_1 : C
Y Y' : D
X : C
⊢ ∀ {Y Y' : D} (g : Y ⟶ Y') (f : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := (G ⋙ obj coyoneda (Opposite.op X)).obj Y')
      ((adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → (G ⋙ coyoneda.obj (Opposite.op X)).obj Y') (f ≫ g) :
        (G ⋙ obj coyoneda (Opposite.op X)).obj Y')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ obj coyoneda (Opposite.op X)).map g) :
            (a : (fun (X : Type v₁) ↦ X) ((G ⋙ coyoneda.obj (Opposite.op X)).obj Y)) →
              (fun (X : Type v₁) ↦ X) ((G ⋙ coyoneda.obj (Opposite.op X)).obj Y'))
          ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → (G ⋙ coyoneda.obj (Opposite.op X)).obj Y) f :
            (G ⋙ obj coyoneda (Opposite.op X)).obj Y) :
        (fun (X : Type v₁) ↦ X) ((G ⋙ obj coyoneda (Opposite.op X)).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 : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y_1 Y' Y : D
⊢ ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ G.obj Y),
    Eq.{v₂ + 1} (α := (F.op ⋙ obj yoneda Y).obj (Opposite.op X))
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → (F.op ⋙ yoneda.obj Y).obj (Opposite.op X)) (f ≫ g) :
        (F.op ⋙ obj yoneda Y).obj (Opposite.op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ obj yoneda Y).map f.op) :
            (a : (fun (X : Type v₂) ↦ X) ((F.op ⋙ yoneda.obj Y).obj (Opposite.op X'))) →
              (fun (X : Type v₂) ↦ X) ((F.op ⋙ yoneda.obj Y).obj (Opposite.op X)))
          (((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → (F.op ⋙ yoneda.obj Y).obj (Opposite.op X')) g :
            (F.op ⋙ obj yoneda Y).obj (Opposite.op X')) :
        (fun (X : Type v₂) ↦ X) ((F.op ⋙ obj yoneda Y).obj (Opposite.op 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
rw :
  F.map f ≫ g =
    ((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y)
      (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g)
⊢ Eq.{v₁ + 1} (α := X' ⟶ G.obj Y) ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) (F.map f ≫ g) : X' ⟶ G.obj Y)
    (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X' ⟶ G.obj Y)

Tactic:
rw [← Equiv.eq_symm_apply]

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 : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g =
    ((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y)
      (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) 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 : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
rw :
  f ≫ G.map g =
    (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y')
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g)
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y')
    (((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') (f ≫ G.map g) : F.obj X ⟶ Y')
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ 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
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g =
    (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y')
      (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) 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 : CoreHomEquivUnitCounit F G
X : C
rw : adj.unit.app X = adj.unit.app X ≫ G.map (𝟙 (F.obj X))
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit, Equiv.symm_apply_eq, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit
-- 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 : CoreHomEquivUnitCounit F G
X : C
⊢ adj.unit.app X = adj.unit.app X ≫ G.map (𝟙 (F.obj 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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : CoreHomEquivUnitCounit F G
Y : D
rw : adj.counit.app Y = F.map (𝟙 (G.obj Y)) ≫ adj.counit.app Y
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)

Tactic:
rw [← adj.homEquiv_unit, ← (adj.homEquiv _ _).eq_symm_apply, adj.homEquiv_counit]

Premises used: CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv, Equiv.eq_symm_apply, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit
-- 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 : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.counit.app Y = F.map (𝟙 (G.obj Y)) ≫ adj.counit.app 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
adj : CoreHomEquivUnitCounit F G
h :
  ∀ (x : C) (x_1 : D) (x_2 : F.obj x ⟶ x_1),
    Eq.{v₁ + 1} (α := x ⟶ G.obj x_1)
      (((mk' adj).homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
      ((adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
⊢ (mk' adj).homEquiv = adj.homEquiv

Tactic:
ext
-- 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 : CoreHomEquivUnitCounit F G
x : C
x_1 : D
x_2 : F.obj x ⟶ x_1
h : (mk' adj).unit.app x ≫ G.map x_2 = (adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2
h₁ : (mk' adj).unit.app x ≫ G.map x_2 = adj.unit.app x ≫ G.map x_2
h₂ h₃ : adj.unit.app x ≫ G.map x_2 = adj.unit.app x ≫ G.map x_2
⊢ Eq.{v₁ + 1} (α := x ⟶ G.obj x_1)
    (((mk' adj).homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)
    ((adj.homEquiv x x_1 : (a : F.obj x ⟶ x_1) → x ⟶ G.obj x_1) x_2 : x ⟶ G.obj x_1)

Tactic:
rw [homEquiv_unit, adj.homEquiv_unit, mk'_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit, CategoryTheory.Adjunction.mk'_unit
-- 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 : CoreHomEquiv F G
X Y : C
f : X ⟶ Y
⊢ Eq (α := obj.{v₁, v₁, u₁, u₁} (𝟭 C) X ⟶ (F ⋙ G).obj Y)
    (map (𝟭 C) f ≫
      ((adj.homEquiv Y (F.obj Y) : Equiv.{v₂ + 1, v₁ + 1} (F.obj Y ⟶ F.obj Y) (Y ⟶ G.obj (F.obj Y))) :
          (a : F.obj Y ⟶ F.obj Y) → Y ⟶ G.obj (F.obj Y))
        (𝟙 (F.obj Y)))
    (((adj.homEquiv X (F.obj X) : Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ F.obj X) (X ⟶ G.obj (F.obj X))) :
          (a : F.obj X ⟶ F.obj X) → X ⟶ G.obj (F.obj X))
        (𝟙 (F.obj X)) ≫
      (F ⋙ G).map f)

Tactic:
simp [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right]

Premises used: CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right, CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left
-- 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 : CoreHomEquiv F G
X Y : D
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ Equiv.invFun (adj.homEquiv (G.obj Y) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)) (𝟙 (G.obj Y)) =
    Equiv.invFun (adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)) (𝟙 (G.obj X)) ≫ map (𝟭 D) f

Tactic:
simp [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm]

Premises used: CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_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 : CoreHomEquiv F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Y) ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) f : X ⟶ G.obj Y)
    (NatTrans.app
          {
            app := fun (X : C) ↦
              ((adj.homEquiv X (F.obj X) : Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ F.obj X) (X ⟶ G.obj (F.obj X))) :
                  (a : F.obj X ⟶ F.obj X) → X ⟶ G.obj (F.obj X))
                (𝟙 (F.obj X)),
            naturality := ⋯ }
          X ≫
        G.map f :
      obj.{v₁, v₁, u₁, u₁} (𝟭 C) X ⟶ G.obj Y)

Tactic:
simp [← adj.homEquiv_naturality_right]

Premises used: CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right
-- 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 : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ ((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f =
    F.map f ≫
      { app := fun (Y : D) ↦ Equiv.invFun (adj.homEquiv (G.obj Y) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)) (𝟙 (G.obj Y)),
            naturality := ⋯ : NatTrans (G ⋙ F) (𝟭 D) }.app
        Y

Tactic:
simp [← adj.homEquiv_naturality_left_symm]

Premises used: CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_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 : CoreHomEquiv F G
h :
  ∀ (X : C) (Y : D) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y) (((mkOfHomEquiv adj).homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X ⟶ G.obj Y)
      ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X ⟶ G.obj Y)
⊢ (mkOfHomEquiv adj).homEquiv = adj.homEquiv

Tactic:
ext X Y 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 : CoreHomEquiv F G
X : C
Y : D
g : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Y) (((mkOfHomEquiv adj).homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X ⟶ G.obj Y)
    ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X ⟶ G.obj Y)

Tactic:
simp [mkOfHomEquiv, ← adj.homEquiv_naturality_right (𝟙 _) g]

Premises used: CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right, CategoryTheory.CategoryStruct.id, CategoryTheory.Adjunction.mkOfHomEquiv
-- 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 : CoreUnitCounit F G
X : C
⊢ whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit = NatTrans.id (𝟭 C ⋙ F)

Tactic:
have := adj.left_triangle
-- 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 : CoreUnitCounit F G
X : C
this : whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit = NatTrans.id (𝟭 C ⋙ F)
⊢ ∀ (x : C),
    (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x = (NatTrans.id (𝟭 C ⋙ F)).app x

Tactic:
rw [NatTrans.ext_iff, funext_iff] at this

Premises used: funext_iff, CategoryTheory.NatTrans.ext_iff
-- 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 : CoreUnitCounit F G
X : C
this :
  ∀ (x : C),
    (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x = (NatTrans.id (𝟭 C ⋙ F)).app x
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
simpa [-CoreUnitCounit.left_triangle] using this X

Premises used: CategoryTheory.Adjunction.CoreUnitCounit.left_triangle
-- 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 : CoreUnitCounit F G
Y : D
⊢ G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G = NatTrans.id (G ⋙ 𝟭 C)

Tactic:
have := adj.right_triangle
-- 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 : CoreUnitCounit F G
Y : D
this : G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G = NatTrans.id (G ⋙ 𝟭 C)
⊢ ∀ (x : D),
    (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x = (NatTrans.id (G ⋙ 𝟭 C)).app x

Tactic:
rw [NatTrans.ext_iff, funext_iff] at this

Premises used: funext_iff, CategoryTheory.NatTrans.ext_iff
-- 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 : CoreUnitCounit F G
Y : D
this :
  ∀ (x : D),
    (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x = (NatTrans.id (G ⋙ 𝟭 C)).app x
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)

Tactic:
simpa [-CoreUnitCounit.right_triangle] using this Y

Premises used: CategoryTheory.Adjunction.CoreUnitCounit.right_triangle
-- 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
f : F.obj X ⟶ Y
⊢ (fun (g : F'.obj X ⟶ Y) ↦ iso.hom.app X ≫ g) ((fun (f : F.obj X ⟶ Y) ↦ iso.inv.app X ≫ f) f) = f

Tactic:
simp