awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Opposites
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.IsRightAdjoint
⊢ F.rightOp.IsLeftAdjoint

Tactic:
⟨F.leftAdjoint.leftOp, ⟨.rightOp <| .ofIsRightAdjoint _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Adjunction.rightOp, CategoryTheory.Functor.leftAdjoint, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Functor.leftOp, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (op X₁)
h :
  ∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
    Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj X₃)
      (((adj X₁).homEquiv X₂ X₃ : (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃) ((F.map f).app X₂ ≫ g) :
        X₂ ⟶ (G.obj (op X₁)).obj X₃)
      (((adj Y₁).homEquiv X₂ X₃ : (a : (F.obj Y₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op Y₁)).obj X₃) g ≫ (G.map f.op).app X₃ :
        X₂ ⟶ (G.obj (op X₁)).obj X₃)
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
w :
  ∀ (X₂ : C₂),
    ((adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁))).app X₂ =
      ((adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)).app X₂
⊢ (adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁)) = (adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)

Tactic:
ext X₂
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (op X₁)
h :
  ∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
    Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj X₃)
      (((adj X₁).homEquiv X₂ X₃ : (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃) ((F.map f).app X₂ ≫ g) :
        X₂ ⟶ (G.obj (op X₁)).obj X₃)
      (((adj Y₁).homEquiv X₂ X₃ : (a : (F.obj Y₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op Y₁)).obj X₃) g ≫ (G.map f.op).app X₃ :
        X₂ ⟶ (G.obj (op X₁)).obj X₃)
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
⊢ ((adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁))).app X₂ =
    ((adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)).app X₂

Tactic:
simpa [Adjunction.homEquiv_unit] using h f (X₂ := X₂) (𝟙 _)

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ adj₂.homEquiv = (adj₂.adj X₁).homEquiv X₂ X₃

Tactic:
rfl

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
X₂ : C₂
X₃ : C₃
f₁ : X₁ ⟶ Y₁
g : (F.obj Y₁).obj X₂ ⟶ X₃
⊢ ((adj₂.adj X₁).unit ≫ whiskerRight (F.map f₁) (G.obj (op X₁))).app X₂ =
    ((adj₂.adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f₁.op)).app X₂

Tactic:
have := NatTrans.congr_app (adj₂.unit_whiskerRight_map f₁) X₂
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
X₂ : C₂
X₃ : C₃
f₁ : X₁ ⟶ Y₁
g : (F.obj Y₁).obj X₂ ⟶ X₃
this :
  (adj₂.adj X₁).unit.app X₂ ≫ (G.obj (op X₁)).map ((F.map f₁).app X₂) =
    (adj₂.adj Y₁).unit.app X₂ ≫ (G.map f₁.op).app ((F.obj Y₁).obj X₂)
⊢ Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.map f₁).app X₂ ≫ g) :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op Y₁)).obj X₃)) :
            (a : (F.obj Y₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op Y₁)).obj X₃)
          g ≫
        (G.map f₁.op).app X₃ :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
simp only [homEquiv_eq, Adjunction.homEquiv_unit, Functor.comp_obj, Functor.map_comp,
    Category.assoc, NatTrans.naturality, reassoc_of% this]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.ParametrizedAdjunction.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ : C₁
X₂ Y₂ : C₂
X₃ : C₃
f₂ : X₂ ⟶ Y₂
g : (F.obj X₁).obj Y₂ ⟶ X₃
⊢ Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.obj X₁).map f₂ ≫ g) :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (f₂ ≫
        ((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj Y₂ ⟶ X₃) (Y₂ ⟶ (G.obj (op X₁)).obj X₃)) :
            (a : (F.obj X₁).obj Y₂ ⟶ X₃) → Y₂ ⟶ (G.obj (op X₁)).obj X₃)
          g :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
(adj₂.adj X₁).homEquiv_naturality_left _ _

Premises used: CategoryTheory.ParametrizedAdjunction.adj, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
g : (F.obj X₁).obj X₂ ⟶ X₃
⊢ Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj Y₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ Y₃) (X₂ ⟶ (G.obj (op X₁)).obj Y₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ Y₃) → X₂ ⟶ (G.obj (op X₁)).obj Y₃)
        (g ≫ f₃) :
      X₂ ⟶ (G.obj (op X₁)).obj Y₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
            (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
          g ≫
        (G.obj (op X₁)).map f₃ :
      X₂ ⟶ (G.obj (op X₁)).obj Y₃)

Tactic:
(adj₂.adj X₁).homEquiv_naturality_right _ _

Premises used: CategoryTheory.ParametrizedAdjunction.adj, CategoryTheory.Adjunction.homEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
X₂ : C₂
X₃ : C₃
f₁ : X₁ ⟶ Y₁
g : X₂ ⟶ (G.obj (op Y₁)).obj X₃
⊢ Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
        (((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op X₁)).obj X₃) ((F.obj X₁).obj X₂ ⟶ X₃)) :
            (a : X₂ ⟶ (G.obj (op X₁)).obj X₃) → (F.obj X₁).obj X₂ ⟶ X₃)
          (g ≫ (G.map f₁.op).app X₃)) :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.map f₁).app X₂ ≫
          ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op Y₁)).obj X₃) ((F.obj Y₁).obj X₂ ⟶ X₃)) :
              (a : X₂ ⟶ (G.obj (op Y₁)).obj X₃) → (F.obj Y₁).obj X₂ ⟶ X₃)
            g) :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
simp [homEquiv_naturality_one]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ : C₁
X₂ Y₂ : C₂
X₃ : C₃
f₂ : X₂ ⟶ Y₂
g : Y₂ ⟶ (G.obj (op X₁)).obj X₃
⊢ Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
        (((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op X₁)).obj X₃) ((F.obj X₁).obj X₂ ⟶ X₃)) :
            (a : X₂ ⟶ (G.obj (op X₁)).obj X₃) → (F.obj X₁).obj X₂ ⟶ X₃)
          (f₂ ≫ g)) :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ X₃) (X₂ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ X₃) → X₂ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.obj X₁).map f₂ ≫
          ((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (Y₂ ⟶ (G.obj (op X₁)).obj X₃) ((F.obj X₁).obj Y₂ ⟶ X₃)) :
              (a : Y₂ ⟶ (G.obj (op X₁)).obj X₃) → (F.obj X₁).obj Y₂ ⟶ X₃)
            g) :
      X₂ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
simp [homEquiv_naturality_two]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
g : X₂ ⟶ (G.obj (op X₁)).obj X₃
⊢ Eq.{v₂ + 1} (α := X₂ ⟶ (G.obj (op X₁)).obj Y₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ Y₃) (X₂ ⟶ (G.obj (op X₁)).obj Y₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ Y₃) → X₂ ⟶ (G.obj (op X₁)).obj Y₃)
        (((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op X₁)).obj Y₃) ((F.obj X₁).obj X₂ ⟶ Y₃)) :
            (a : X₂ ⟶ (G.obj (op X₁)).obj Y₃) → (F.obj X₁).obj X₂ ⟶ Y₃)
          (g ≫ (G.obj (op X₁)).map f₃)) :
      X₂ ⟶ (G.obj (op X₁)).obj Y₃)
    (((adj₂.homEquiv : Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj X₂ ⟶ Y₃) (X₂ ⟶ (G.obj (op X₁)).obj Y₃)) :
          (a : (F.obj X₁).obj X₂ ⟶ Y₃) → X₂ ⟶ (G.obj (op X₁)).obj Y₃)
        (((Equiv.symm adj₂.homEquiv : Equiv.{v₂ + 1, v₃ + 1} (X₂ ⟶ (G.obj (op X₁)).obj X₃) ((F.obj X₁).obj X₂ ⟶ X₃)) :
              (a : X₂ ⟶ (G.obj (op X₁)).obj X₃) → (F.obj X₁).obj X₂ ⟶ X₃)
            g ≫
          f₃) :
      X₂ ⟶ (G.obj (op X₁)).obj Y₃)

Tactic:
simp [homEquiv_naturality_three]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
w :
  ∀ (X₃ : C₃),
    ((G.obj (op Y₁)).whiskerLeft (F.map f) ≫ (adj₂.adj Y₁).counit).app X₃ =
      (whiskerRight (G.map f.op) (F.obj X₁) ≫ (adj₂.adj X₁).counit).app X₃
⊢ (G.obj (op Y₁)).whiskerLeft (F.map f) ≫ (adj₂.adj Y₁).counit =
    whiskerRight (G.map f.op) (F.obj X₁) ≫ (adj₂.adj X₁).counit

Tactic:
ext X₃
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
w :
  (F.map f).app ((G.obj (op Y₁)).obj X₃) ≫ (adj₂.adj Y₁).counit.app X₃ =
    (F.obj X₁).map ((G.map f.op).app X₃) ≫ (adj₂.adj X₁).counit.app X₃
⊢ ((G.obj (op Y₁)).whiskerLeft (F.map f) ≫ (adj₂.adj Y₁).counit).app X₃ =
    (whiskerRight (G.map f.op) (F.obj X₁) ≫ (adj₂.adj X₁).counit).app X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
w :
  Eq.{v₂ + 1} (α := (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃)
              ((G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃) → (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.map f).app ((G.obj (op Y₁)).obj X₃) ≫ (adj₂.adj Y₁).counit.app X₃) :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃)
              ((G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃) → (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.obj X₁).map ((G.map f.op).app X₃) ≫ (adj₂.adj X₁).counit.app X₃) :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
⊢ (F.map f).app ((G.obj (op Y₁)).obj X₃) ≫ (adj₂.adj Y₁).counit.app X₃ =
    (F.obj X₁).map ((G.map f.op).app X₃) ≫ (adj₂.adj X₁).counit.app X₃

Tactic:
apply adj₂.homEquiv.injective

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
w :
  Eq.{v₂ + 1} (α := (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃)
                ((G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op Y₁)).obj X₃)) :
            (a : (F.obj Y₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃) → (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op Y₁)).obj X₃)
          ((adj₂.adj Y₁).counit.app X₃) ≫
        (G.map f.op).app X₃ :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    ((G.map f.op).app X₃ ≫
        ((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj ((G.obj (op X₁)).obj X₃) ⟶ X₃)
                ((G.obj (op X₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)) :
            (a : (F.obj X₁).obj ((G.obj (op X₁)).obj X₃) ⟶ X₃) → (G.obj (op X₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
          ((adj₂.adj X₁).counit.app X₃) :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
⊢ Eq.{v₂ + 1} (α := (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃)
              ((G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃) → (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.map f).app ((G.obj (op Y₁)).obj X₃) ≫ (adj₂.adj Y₁).counit.app X₃) :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
            Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃)
              ((G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)) :
          (a : (F.obj X₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃) → (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
        ((F.obj X₁).map ((G.map f.op).app X₃) ≫ (adj₂.adj X₁).counit.app X₃) :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
rw [homEquiv_naturality_one, homEquiv_naturality_two]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one
-- Module: Mathlib.CategoryTheory.Adjunction.Parametrized
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
F : C₁ ⥤ Functor.{v₂, v₃, u₂, u₃} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v₃, v₂, u₃, u₂} C₃ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
⊢ Eq.{v₂ + 1} (α := (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    (((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj Y₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃)
                ((G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op Y₁)).obj X₃)) :
            (a : (F.obj Y₁).obj ((G.obj (op Y₁)).obj X₃) ⟶ X₃) → (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op Y₁)).obj X₃)
          ((adj₂.adj Y₁).counit.app X₃) ≫
        (G.map f.op).app X₃ :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
    ((G.map f.op).app X₃ ≫
        ((adj₂.homEquiv :
              Equiv.{v₃ + 1, v₂ + 1} ((F.obj X₁).obj ((G.obj (op X₁)).obj X₃) ⟶ X₃)
                ((G.obj (op X₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)) :
            (a : (F.obj X₁).obj ((G.obj (op X₁)).obj X₃) ⟶ X₃) → (G.obj (op X₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)
          ((adj₂.adj X₁).counit.app X₃) :
      (G.obj (op Y₁)).obj X₃ ⟶ (G.obj (op X₁)).obj X₃)

Tactic:
simp [homEquiv_eq, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.ParametrizedAdjunction.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
s : Cone (P ⋙ G.flip.obj X₃)
x x_1 : Jᵒᵖ
f : x ⟶ x_1
⊢ Eq (α :=
    (P.leftOp ⋙ F.flip.obj s.pt).obj x ⟶ Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) x_1)
    ((P.leftOp ⋙ F.flip.obj s.pt).map f ≫
      ((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1}
              (s.pt ⟶
                (G.obj (op (P.leftOp.obj x_1))).obj
                  (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) x_1))
              ((F.obj (P.leftOp.obj x_1)).obj s.pt ⟶
                Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) x_1)) :
          (a : s.pt ⟶ (G.obj (op (P.leftOp.obj x_1))).obj (((Functor.const Jᵒᵖ).obj X₃).obj x_1)) →
            (F.obj (P.leftOp.obj x_1)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj x_1)
        (s.π.app (unop x_1)))
    (((Equiv.symm adj₂.homEquiv :
            Equiv.{v_2 + 1, v_3 + 1}
              (s.pt ⟶
                (G.obj (op (P.leftOp.obj x))).obj
                  (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) x))
              ((F.obj (P.leftOp.obj x)).obj s.pt ⟶
                Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) x)) :
          (a : s.pt ⟶ (G.obj (op (P.leftOp.obj x))).obj (((Functor.const Jᵒᵖ).obj X₃).obj x)) →
            (F.obj (P.leftOp.obj x)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj x)
        (s.π.app (unop x)) ≫
      Functor.map (Functor.obj (Functor.const Jᵒᵖ) X₃) f)

Tactic:
simp [← s.w f.unop, dsimp% adj₂.homEquiv_symm_naturality_one (P.map f.unop).unop]

Premises used: CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one, Quiver.Hom.unop, CategoryTheory.Functor.map, CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ C₃
G : C₁ᵒᵖ ⥤ Functor.{v_3, v_2, u_3, u_2} C₃ C₂
adj₂ : F ⊣₂ G
J : Type u_4
inst_3 : Category.{v_4, u_4} J
P : Functor.{v_4, v_1, u_4, u_1} J C₁ᵒᵖ
inst_4 : ∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)
X₃ : C₃
c : Cone P
hc : IsLimit c
cocone : (s : Cone (P ⋙ G.flip.obj X₃)) → Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦
    { pt := X₃,
      ι :=
        {
          app := fun (j : Jᵒᵖ) ↦
            ((Equiv.symm adj₂.homEquiv :
                  Equiv.{v_2 + 1, v_3 + 1}
                    (s.pt ⟶
                      (G.obj (op (P.leftOp.obj j))).obj
                        (Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j))
                    ((F.obj (P.leftOp.obj j)).obj s.pt ⟶
                      Functor.obj.{v_4, v_3, u_4, u_3} (Functor.obj (Functor.const Jᵒᵖ) X₃) j)) :
                (a : s.pt ⟶ (G.obj (op (P.leftOp.obj j))).obj (((Functor.const Jᵒᵖ).obj X₃).obj j)) →
                  (F.obj (P.leftOp.obj j)).obj s.pt ⟶ ((Functor.const Jᵒᵖ).obj X₃).obj j)
              (s.π.app (unop j)),
          naturality := ⋯ } }
hc' : (s : Cone (P ⋙ G.flip.obj X₃)) → IsColimit ((F.flip.obj s.pt).mapCocone (coconeLeftOpOfCone c)) :=
  fun (s : Cone (P ⋙ G.flip.obj X₃)) ↦ isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone P hc)
s : Cone (P ⋙ G.flip.obj X₃)
j : J
dsimp :
  ((adj₂.homEquiv :
            Equiv.{v_3 + 1, v_2 + 1} ((F.obj (unop c.1)).obj s.pt ⟶ X₃) (s.pt ⟶ (G.obj (op (unop c.1))).obj X₃)) :
          (a : (F.obj (unop c.1)).obj s.pt ⟶ X₃) → s.pt ⟶ (G.obj c.1).obj X₃)
        ((hc' s).desc (cocone s)) ≫
      (G.map (c.π.app j)).app X₃ =
    s.π.app j
⊢ ((adj₂.homEquiv :
            Equiv.{v_3 + 1, v_2 + 1} ((F.obj (unop c.1)).obj s.pt ⟶ X₃) (s.pt ⟶ (G.obj (op (unop c.1))).obj X₃)) :
          (a : (F.obj (unop c.1)).obj s.pt ⟶ X₃) → s.pt ⟶ (G.obj (op (unop c.1))).obj X₃)
        ((hc' s).desc (cocone s)) ≫
      ((G.flip.obj X₃).mapCone c).π.app j =
    s.π.app j

Tactic:
dsimp