awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₁, v₃, u₁, u₃} A C
H : Functor.{v₂, v₄, u₂, u₄} B D
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₁, v₂, u₁, u₂} A B
R₂ : Functor.{v₂, v₁, u₂, u₁} B A
L₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃ : Functor.{v₄, v₃, u₄, u₃} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)) → TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (Iso.hom (associator (𝟭 A) G L₃) ≫
          whiskerLeft (𝟭 A) β.natTrans ≫
            Iso.inv (associator (𝟭 A) L₂ H) ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight
            (natTrans
              ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 A) L₁ L₂ (𝟭 B)) → TwoSquare R₁ (𝟭 B) (𝟭 A) R₂)
                (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)))
            G ≫
          Iso.hom (associator (𝟭 B) R₂ G) ≫
            whiskerLeft (𝟭 B) (natTrans ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)) ≫
              Iso.inv (associator (𝟭 B) H R₃))
⊢ app
      ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)) → TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
        (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
          (Iso.hom (associator (𝟭 A) G L₃) ≫
            whiskerLeft (𝟭 A) β.natTrans ≫
              Iso.inv (associator (𝟭 A) L₂ H) ≫
                whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)))
      b =
    (TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
          ((R₁.associator (𝟭 A) G).inv ≫
            whiskerRight
                (natTrans
                  ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 A) L₁ L₂ (𝟭 B)) → TwoSquare R₁ (𝟭 B) (𝟭 A) R₂)
                    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)))
                G ≫
              Iso.hom (associator (𝟭 B) R₂ G) ≫
                whiskerLeft (𝟭 B)
                    (natTrans ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)) ≫
                  Iso.inv (associator (𝟭 B) H R₃))).app
      b

Tactic:
have vcompb := congr_app vcomp b
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₁, v₃, u₁, u₃} A C
H : Functor.{v₂, v₄, u₂, u₄} B D
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₁, v₂, u₁, u₂} A B
R₂ : Functor.{v₂, v₁, u₂, u₁} B A
L₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃ : Functor.{v₄, v₃, u₄, u₃} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)) → TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (Iso.hom (associator (𝟭 A) G L₃) ≫
          whiskerLeft (𝟭 A) β.natTrans ≫
            Iso.inv (associator (𝟭 A) L₂ H) ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight
            (natTrans
              ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 A) L₁ L₂ (𝟭 B)) → TwoSquare R₁ (𝟭 B) (𝟭 A) R₂)
                (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)))
            G ≫
          Iso.hom (associator (𝟭 B) R₂ G) ≫
            whiskerLeft (𝟭 B) (natTrans ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)) ≫
              Iso.inv (associator (𝟭 B) H R₃))
vcompb :
  adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) =
    G.map (adj₂.unit.app (R₁.obj b)) ≫
      G.map (R₂.map (α.app (R₁.obj b))) ≫
        G.map (R₂.map (adj₁.counit.app b)) ≫
          adj₃.unit.app (G.obj (R₂.obj b)) ≫ R₃.map (β.natTrans.app (R₂.obj b)) ≫ R₃.map (H.map (adj₂.counit.app b))
⊢ Eq.{v₃ + 1} (α := (R₁ ⋙ G).obj b ⟶ (H ⋙ R₃).obj b)
    (app (natTrans ((mateEquiv adj₁ adj₃ : (a : TwoSquare G L₁ L₃ H) → TwoSquare R₁ H G R₃) (β.whiskerLeft α))) b)
    (app
      (natTrans
        (TwoSquare.whiskerTop (T' := R₂) ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β)
          ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α)))
      b)

Tactic:
simpa [mateEquiv]

Premises used: CategoryTheory.mateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
L₀₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁₀ : Functor.{v₂, v₁, u₂, u₁} B A
L₁₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₂₁ : Functor.{v₃, v₂, u₃, u₂} C B
L₂₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃₂ : Functor.{v₄, v₃, u₄, u₃} D C
adj₀₁ : L₀₁ ⊣ R₁₀
adj₁₂ : L₁₂ ⊣ R₂₁
adj₂₃ : L₂₃ ⊣ R₃₂
w :
  ∀ (X : D),
    app
        ((conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃) :
            (a : (L₀₁ ⋙ L₁₂) ⋙ L₂₃ ⟶ L₀₁ ⋙ L₁₂ ⋙ L₂₃) → (R₃₂ ⋙ R₂₁) ⋙ R₁₀ ⟶ R₃₂ ⋙ R₂₁ ⋙ R₁₀)
          (L₀₁.associator L₁₂ L₂₃).hom)
        X =
      (R₃₂.associator R₂₁ R₁₀).hom.app X
⊢ (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃) :
        (a : (L₀₁ ⋙ L₁₂) ⋙ L₂₃ ⟶ L₀₁ ⋙ L₁₂ ⋙ L₂₃) → (R₃₂ ⋙ R₂₁) ⋙ R₁₀ ⟶ R₃₂ ⋙ R₂₁ ⋙ R₁₀)
      (L₀₁.associator L₁₂ L₂₃).hom =
    (R₃₂.associator R₂₁ R₁₀).hom

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
L₀₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁₀ : Functor.{v₂, v₁, u₂, u₁} B A
L₁₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₂₁ : Functor.{v₃, v₂, u₃, u₂} C B
L₂₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃₂ : Functor.{v₄, v₃, u₄, u₃} D C
adj₀₁ : L₀₁ ⊣ R₁₀
adj₁₂ : L₁₂ ⊣ R₂₁
adj₂₃ : L₂₃ ⊣ R₃₂
X : D
w :
  adj₀₁.unit.app (R₁₀.obj (R₂₁.obj (R₃₂.obj X))) ≫
      R₁₀.map
        (adj₁₂.unit.app (L₀₁.obj (R₁₀.obj (R₂₁.obj (R₃₂.obj X)))) ≫
          R₂₁.map
            (adj₂₃.unit.app (L₁₂.obj (L₀₁.obj (R₁₀.obj (R₂₁.obj (R₃₂.obj X))))) ≫
              R₃₂.map
                (L₂₃.map (L₁₂.map (adj₀₁.counit.app (R₂₁.obj (R₃₂.obj X)))) ≫
                  L₂₃.map (adj₁₂.counit.app (R₃₂.obj X)) ≫ adj₂₃.counit.app X))) =
    𝟙 (R₁₀.obj (R₂₁.obj (R₃₂.obj X)))
⊢ app
      ((conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃) :
          (a : (L₀₁ ⋙ L₁₂) ⋙ L₂₃ ⟶ L₀₁ ⋙ L₁₂ ⋙ L₂₃) → (R₃₂ ⋙ R₂₁) ⋙ R₁₀ ⟶ R₃₂ ⋙ R₂₁ ⋙ R₁₀)
        (L₀₁.associator L₁₂ L₂₃).hom)
      X =
    (R₃₂.associator R₂₁ R₁₀).hom.app X

Tactic:
simp only [comp_obj, conjugateEquiv_apply_app, Adjunction.comp_unit_app, id_obj,
    Functor.comp_map, Category.assoc, ← map_comp, associator_hom_app, map_id,
    Adjunction.comp_counit_app, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.conjugateEquiv_apply_app, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Adjunction.comp_counit_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp, CategoryTheory.Adjunction.comp_unit_app
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
inst_3 : Category.{v₄, u₄} D
L₀₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁₀ : Functor.{v₂, v₁, u₂, u₁} B A
L₁₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₂₁ : Functor.{v₃, v₂, u₃, u₂} C B
L₂₃ : Functor.{v₃, v₄, u₃, u₄} C D
R₃₂ : Functor.{v₄, v₃, u₄, u₃} D C
adj₀₁ : L₀₁ ⊣ R₁₀
adj₁₂ : L₁₂ ⊣ R₂₁
adj₂₃ : L₂₃ ⊣ R₃₂
X : D
⊢ adj₀₁.unit.app (R₁₀.obj (R₂₁.obj (R₃₂.obj X))) ≫
      R₁₀.map
        (adj₁₂.unit.app (L₀₁.obj (R₁₀.obj (R₂₁.obj (R₃₂.obj X)))) ≫
          R₂₁.map
            (adj₂₃.unit.app (L₁₂.obj (L₀₁.obj (R₁₀.obj (R₂₁.obj (R₃₂.obj X))))) ≫
              R₃₂.map
                (L₂₃.map (L₁₂.map (adj₀₁.counit.app (R₂₁.obj (R₃₂.obj X)))) ≫
                  L₂₃.map (adj₁₂.counit.app (R₃₂.obj X)) ≫ adj₂₃.counit.app X))) =
    𝟙 (R₁₀.obj (R₂₁.obj (R₃₂.obj X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₁ R₂ : Functor.{v₃, v₂, u₃, u₂} C B
L : Functor.{v₁, v₂, u₁, u₂} A B
R : Functor.{v₂, v₁, u₂, u₁} B A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
w :
  ∀ (X : C),
    Eq (α := (R₁ ⋙ R).obj X ⟶ (R₂ ⋙ R).obj X)
      (app
        ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂) : (a : L ⋙ L₂ ⟶ L ⋙ L₁) → R₁ ⋙ R ⟶ R₂ ⋙ R) (L.whiskerLeft τ))
        X)
      (app (whiskerRight ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) τ) R) X)
⊢ Eq (α := R₁ ⋙ R ⟶ R₂ ⋙ R)
    ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂) : (a : L ⋙ L₂ ⟶ L ⋙ L₁) → R₁ ⋙ R ⟶ R₂ ⋙ R) (L.whiskerLeft τ) :
      R₁ ⋙ R ⟶ R₂ ⋙ R)
    (whiskerRight ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) τ) R : R₁ ⋙ R ⟶ R₂ ⋙ R)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₁ R₂ : Functor.{v₃, v₂, u₃, u₂} C B
L : Functor.{v₁, v₂, u₁, u₂} A B
R : Functor.{v₂, v₁, u₂, u₁} B A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
⊢ Eq (α :=
    (R₂ ⋙ R).obj (L₂.obj ((R ⋙ L).obj (R₁.obj X))) ⟶ (R₂ ⋙ R).obj (L₁.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X))))

Tactic:
have h₁ := congr_map (R₂ ⋙ R) (τ.naturality (adj.counit.app (R₁.obj X)))
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₁ R₂ : Functor.{v₃, v₂, u₃, u₂} C B
L : Functor.{v₁, v₂, u₁, u₂} A B
R : Functor.{v₂, v₁, u₂, u₁} B A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  Eq (α :=
    (R₂ ⋙ R).obj (L₂.obj ((R ⋙ L).obj (R₁.obj X))) ⟶ (R₂ ⋙ R).obj (L₁.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X))))
⊢ Eq (α := R.obj ((R ⋙ L).obj (R₁.obj X)) ⟶ R.obj (R₂.obj (L₂.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X)))))
    (R.map (adj₂.unit.app ((R ⋙ L).obj (R₁.obj X)) ≫ R₂.map (L₂.map (adj.counit.app (R₁.obj X)))))
    (R.map (adj.counit.app (R₁.obj X) ≫ adj₂.unit.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))

Tactic:
have h₂ := congr_map R (adj₂.unit_naturality (adj.counit.app (R₁.obj X)))
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₁ R₂ : Functor.{v₃, v₂, u₃, u₂} C B
L : Functor.{v₁, v₂, u₁, u₂} A B
R : Functor.{v₂, v₁, u₂, u₁} B A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  Eq (α :=
    (R₂ ⋙ R).obj (L₂.obj ((R ⋙ L).obj (R₁.obj X))) ⟶ (R₂ ⋙ R).obj (L₁.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X))))
h₂ :
  Eq (α := R.obj ((R ⋙ L).obj (R₁.obj X)) ⟶ R.obj (R₂.obj (L₂.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X)))))
    (R.map (adj₂.unit.app ((R ⋙ L).obj (R₁.obj X)) ≫ R₂.map (L₂.map (adj.counit.app (R₁.obj X)))))
    (R.map (adj.counit.app (R₁.obj X) ≫ adj₂.unit.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
⊢ Eq (α := R.obj (R₂.obj (L₂.obj (L.obj (R.obj (R₁.obj X))))) ⟶ R.obj (R₂.obj (L₁.obj (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X))) ≫ (R₂ ⋙ R).map (τ.app (R₁.obj X)))
    ((R₂ ⋙ R).map (τ.app (L.obj (R.obj (R₁.obj X)))) ≫ (R₂ ⋙ R).map (L₁.map (adj.counit.app (R₁.obj X))))

Tactic:
simp only [comp_obj, id_obj, Functor.map_comp] at h₁ h₂

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₁ R₂ : Functor.{v₃, v₂, u₃, u₂} C B
L : Functor.{v₁, v₂, u₁, u₂} A B
R : Functor.{v₂, v₁, u₂, u₁} B A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  Eq (α :=
    (R₂ ⋙ R).obj (L₂.obj ((R ⋙ L).obj (R₁.obj X))) ⟶ (R₂ ⋙ R).obj (L₁.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
    ((R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X))))
h₂ :
  Eq (α := R.obj ((R ⋙ L).obj (R₁.obj X)) ⟶ R.obj (R₂.obj (L₂.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X)))))
    (R.map (adj₂.unit.app ((R ⋙ L).obj (R₁.obj X)) ≫ R₂.map (L₂.map (adj.counit.app (R₁.obj X)))))
    (R.map (adj.counit.app (R₁.obj X) ≫ adj₂.unit.app (obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R₁.obj X))))
h₃ :
  Eq (α := R.obj (R₂.obj (L₂.obj (L.obj (R.obj (R₁.obj X))))) ⟶ R.obj (R₂.obj (L₁.obj (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X))) ≫ (R₂ ⋙ R).map (τ.app (R₁.obj X)))
    ((R₂ ⋙ R).map (τ.app (L.obj (R.obj (R₁.obj X)))) ≫ (R₂ ⋙ R).map (L₁.map (adj.counit.app (R₁.obj X))))
⊢ Eq (α := R.obj (L.obj (R.obj (R₁.obj X))) ⟶ R.obj (R₂.obj (L₂.obj (R₁.obj X))))
    (R.map (adj₂.unit.app (L.obj (R.obj (R₁.obj X)))) ≫ R.map (R₂.map (L₂.map (adj.counit.app (R₁.obj X)))))
    (R.map (adj.counit.app (R₁.obj X)) ≫ R.map (adj₂.unit.app (R₁.obj X)))

Tactic:
simp only [comp_obj, id_obj, Functor.map_comp] at h₁ h₂

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₂, v₃, u₂, u₃} B C
R₁ R₂ : Functor.{v₃, v₂, u₃, u₂} C B
L : Functor.{v₁, v₂, u₁, u₂} A B
R : Functor.{v₂, v₁, u₂, u₁} B A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  Eq (α := R.obj (R₂.obj (L₂.obj (L.obj (R.obj (R₁.obj X))))) ⟶ R.obj (R₂.obj (L₁.obj (R₁.obj X))))
    ((R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X))) ≫ (R₂ ⋙ R).map (τ.app (R₁.obj X)))
    ((R₂ ⋙ R).map (τ.app (L.obj (R.obj (R₁.obj X)))) ≫ (R₂ ⋙ R).map (L₁.map (adj.counit.app (R₁.obj X))))
h₂ :
  Eq (α := R.obj (L.obj (R.obj (R₁.obj X))) ⟶ R.obj (R₂.obj (L₂.obj (R₁.obj X))))
    (R.map (adj₂.unit.app (L.obj (R.obj (R₁.obj X)))) ≫ R.map (R₂.map (L₂.map (adj.counit.app (R₁.obj X)))))
    (R.map (adj.counit.app (R₁.obj X)) ≫ R.map (adj₂.unit.app (R₁.obj X)))
⊢ Eq (α := (R₁ ⋙ R).obj X ⟶ (R₂ ⋙ R).obj X)
    (app ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂) : (a : L ⋙ L₂ ⟶ L ⋙ L₁) → R₁ ⋙ R ⟶ R₂ ⋙ R) (L.whiskerLeft τ))
      X)
    (app (whiskerRight ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) τ) R) X)

Tactic:
simp [← reassoc_of% h₁, reassoc_of% h₂]
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₂, v₃, u₂, u₃} B C
R : Functor.{v₃, v₂, u₃, u₂} C B
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
w :
  ∀ (X : C),
    Eq.{v₁ + 1} (α := (R ⋙ R₁).obj X ⟶ (R ⋙ R₂).obj X)
      (app
        ((conjugateEquiv (adj₁.comp adj) (adj₂.comp adj) : (a : L₂ ⋙ L ⟶ L₁ ⋙ L) → R ⋙ R₁ ⟶ R ⋙ R₂) (whiskerRight τ L))
        X)
      (app (R.whiskerLeft ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) τ)) X)
⊢ Eq (α := R ⋙ R₁ ⟶ R ⋙ R₂)
    ((conjugateEquiv (adj₁.comp adj) (adj₂.comp adj) : (a : L₂ ⋙ L ⟶ L₁ ⋙ L) → R ⋙ R₁ ⟶ R ⋙ R₂) (whiskerRight τ L) :
      R ⋙ R₁ ⟶ R ⋙ R₂)
    (R.whiskerLeft ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) τ) : R ⋙ R₁ ⟶ R ⋙ R₂)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₂, v₃, u₂, u₃} B C
R : Functor.{v₃, v₂, u₃, u₂} C B
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
w :
  adj₂.unit.app (R₁.obj (R.obj X)) ≫
      R₂.map
        (adj.unit.app (L₂.obj (R₁.obj (R.obj X))) ≫
          R.map (L.map (τ.app (R₁.obj (R.obj X))) ≫ L.map (adj₁.counit.app (R.obj X)) ≫ adj.counit.app X)) =
    adj₂.unit.app (R₁.obj (R.obj X)) ≫ R₂.map (τ.app (R₁.obj (R.obj X)) ≫ adj₁.counit.app (R.obj X))
⊢ Eq.{v₁ + 1} (α := (R ⋙ R₁).obj X ⟶ (R ⋙ R₂).obj X)
    (app ((conjugateEquiv (adj₁.comp adj) (adj₂.comp adj) : (a : L₂ ⋙ L ⟶ L₁ ⋙ L) → R ⋙ R₁ ⟶ R ⋙ R₂) (whiskerRight τ L))
      X)
    (app (R.whiskerLeft ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) τ)) X)

Tactic:
simp only [comp_obj, conjugateEquiv_apply_app, comp_unit_app, id_obj, Functor.whiskerRight_app,
    Functor.comp_map, comp_counit_app, ← map_comp, assoc, Functor.whiskerLeft_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.conjugateEquiv_apply_app, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Adjunction.comp_counit_app, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.comp_unit_app
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₂, v₃, u₂, u₃} B C
R : Functor.{v₃, v₂, u₃, u₂} C B
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
⊢ adj₂.unit.app (R₁.obj (R.obj X)) ≫
      R₂.map
        (adj.unit.app (L₂.obj (R₁.obj (R.obj X))) ≫
          R.map (L.map (τ.app (R₁.obj (R.obj X))) ≫ L.map (adj₁.counit.app (R.obj X)) ≫ adj.counit.app X)) =
    adj₂.unit.app (R₁.obj (R.obj X)) ≫ R₂.map (τ.app (R₁.obj (R.obj X)) ≫ adj₁.counit.app (R.obj X))

Tactic:
simp
-- 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
G : Functor.{v₂, v₁, u₂, u₁} D C
h : G ⊣ F
x : Cᵒᵖ
⊢ (F.op.map ((NatTrans.op h.counit).app x) ≫ (NatTrans.op h.unit).app (F.op.obj x)).unop =
    Quiver.Hom.unop (𝟙 (F.op.obj x))

Tactic:
simp
-- 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
G : Functor.{v₂, v₁, u₂, u₁} D C
h : G ⊣ F
x : Dᵒᵖ
⊢ ((NatTrans.op h.counit).app (G.op.obj x) ≫ G.op.map ((NatTrans.op h.unit).app x)).unop =
    Quiver.Hom.unop (𝟙 (G.op.obj x))

Tactic:
simp
-- 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ᵒᵖ
G : Functor.{v₂, v₁, u₂, u₁} D Cᵒᵖ
a : F ⊣ G.leftOp
h :
  ∀ (X : D),
    a.leftOp.unit.app X =
      NatTrans.app (unit (comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op)) X
⊢ a.leftOp = comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op

Tactic:
ext X
-- 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ᵒᵖ
G : Functor.{v₂, v₁, u₂, u₁} D Cᵒᵖ
a : F ⊣ G.leftOp
X : D
⊢ a.leftOp.unit.app X =
    NatTrans.app (unit (comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op)) X

Tactic:
simp [Equivalence.unit]

Premises used: CategoryTheory.Equivalence.unit
-- 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
G : Functor.{v₂, v₁, u₂, u₁} Dᵒᵖ C
a : F.rightOp ⊣ G
h :
  ∀ (X : D),
    a.rightOp.unit.app X =
      NatTrans.app (unit (comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op)) X
⊢ a.rightOp = comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op

Tactic:
ext X
-- 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
G : Functor.{v₂, v₁, u₂, u₁} Dᵒᵖ C
a : F.rightOp ⊣ G
X : D
⊢ a.rightOp.unit.app X =
    NatTrans.app (unit (comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op)) X

Tactic:
simp [Equivalence.unit]

Premises used: CategoryTheory.Equivalence.unit
-- 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.IsLeftAdjoint
⊢ F.op.IsRightAdjoint

Tactic:
⟨F.rightAdjoint.op, ⟨.op <| .ofIsLeftAdjoint _⟩⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.Adjunction.op, CategoryTheory.Adjunction.ofIsLeftAdjoint, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Functor.rightAdjoint
-- 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.op.IsLeftAdjoint

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

Premises used: CategoryTheory.Functor.op, CategoryTheory.Adjunction.op, Nonempty.intro, CategoryTheory.Functor.leftAdjoint, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Adjunction.ofIsRightAdjoint
-- 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.IsLeftAdjoint
⊢ F.leftOp.IsRightAdjoint

Tactic:
⟨F.rightAdjoint.rightOp, ⟨.leftOp <| .ofIsLeftAdjoint _⟩⟩

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Adjunction.leftOp, Nonempty.intro, Exists.intro, CategoryTheory.Functor.rightOp, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Functor.rightAdjoint
-- 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.leftOp.IsLeftAdjoint

Tactic:
inferInstanceAs (F.op ⋙ (opOpEquivalence D).functor).IsLeftAdjoint

Premises used: _private.0.CategoryTheory.Functor.IsRightAdjoint.leftOp._proof_1
-- 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.IsLeftAdjoint
⊢ F.rightOp.IsRightAdjoint

Tactic:
inferInstanceAs ((opOpEquivalence C).inverse ⋙ F.op).IsRightAdjoint

Premises used: _private.0.CategoryTheory.Functor.IsLeftAdjoint.rightOp._proof_1