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₄
E : Type u₅
F : Type u₆
X : Type u₇
Y : Type u₈
Z : 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
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
inst_8 : Category.{v₉, u₉} Z
G₁ : Functor.{v₁, v₄, u₁, u₄} A D
H₁ : Functor.{v₂, v₅, u₂, u₅} B E
K₁ : Functor.{v₃, v₆, u₃, u₆} C F
G₂ : Functor.{v₄, v₇, u₄, u₇} D X
H₂ : Functor.{v₅, v₈, u₅, u₈} E Y
K₂ : Functor.{v₆, v₉, u₆, u₉} F Z
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₅} D E
R₃ : Functor.{v₅, v₄, u₅, u₄} E D
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
L₅ : Functor.{v₇, v₈, u₇, u₈} X Y
R₅ : Functor.{v₈, v₇, u₈, u₇} Y X
L₆ : Functor.{v₈, v₉, u₈, u₉} Y Z
R₆ : Functor.{v₉, v₈, u₉, u₈} Z Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
vcomp :
  Eq (α := TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a : TwoSquare (G₁ ⋙ G₂) (L₁ ⋙ L₂) (L₅ ⋙ L₆) (K₁ ⋙ K₂)) → TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
        ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    (vComp (B := R₄ ⋙ R₃)
        ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
            (a : TwoSquare G₁ (L₁ ⋙ L₂) (L₃ ⋙ L₄) K₁) → TwoSquare (R₂ ⋙ R₁) K₁ G₁ (R₄ ⋙ R₃))
          (α ≫ᵥ β))
        ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) :
            (a : TwoSquare G₂ (L₃ ⋙ L₄) (L₅ ⋙ L₆) K₂) → TwoSquare (R₄ ⋙ R₃) K₂ G₂ (R₆ ⋙ R₅))
          (γ ≫ᵥ δ)) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
⊢ Eq (α := TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a : TwoSquare (G₁ ⋙ G₂) (L₁ ⋙ L₂) (L₅ ⋙ L₆) (K₁ ⋙ K₂)) → TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
        ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    (vComp (B := R₄ ⋙ R₃)
        (hComp (R := H₁) ((mateEquiv adj₂ adj₄ : (a : TwoSquare H₁ L₂ L₄ K₁) → TwoSquare R₂ K₁ H₁ R₄) β)
          ((mateEquiv adj₁ adj₃ : (a : TwoSquare G₁ L₁ L₃ H₁) → TwoSquare R₁ H₁ G₁ R₃) α))
        (hComp (R := H₂) ((mateEquiv adj₄ adj₆ : (a : TwoSquare H₂ L₄ L₆ K₂) → TwoSquare R₄ K₂ H₂ R₆) δ)
          ((mateEquiv adj₃ adj₅ : (a : TwoSquare G₂ L₃ L₅ H₂) → TwoSquare R₃ H₂ G₂ R₅) γ)) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))

Tactic:
simp only [mateEquiv_hcomp] at vcomp

Premises used: CategoryTheory.mateEquiv_hcomp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
X : Type u₇
Y : Type u₈
Z : 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
inst_4 : Category.{v₅, u₅} E
inst_5 : Category.{v₆, u₆} F
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
inst_8 : Category.{v₉, u₉} Z
G₁ : Functor.{v₁, v₄, u₁, u₄} A D
H₁ : Functor.{v₂, v₅, u₂, u₅} B E
K₁ : Functor.{v₃, v₆, u₃, u₆} C F
G₂ : Functor.{v₄, v₇, u₄, u₇} D X
H₂ : Functor.{v₅, v₈, u₅, u₈} E Y
K₂ : Functor.{v₆, v₉, u₆, u₉} F Z
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₅} D E
R₃ : Functor.{v₅, v₄, u₅, u₄} E D
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
L₅ : Functor.{v₇, v₈, u₇, u₈} X Y
R₅ : Functor.{v₈, v₇, u₈, u₇} Y X
L₆ : Functor.{v₈, v₉, u₈, u₉} Y Z
R₆ : Functor.{v₉, v₈, u₉, u₈} Z Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
vcomp :
  Eq (α := TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a : TwoSquare (G₁ ⋙ G₂) (L₁ ⋙ L₂) (L₅ ⋙ L₆) (K₁ ⋙ K₂)) → TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
        ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    (vComp (B := R₄ ⋙ R₃)
        (hComp (R := H₁) ((mateEquiv adj₂ adj₄ : (a : TwoSquare H₁ L₂ L₄ K₁) → TwoSquare R₂ K₁ H₁ R₄) β)
          ((mateEquiv adj₁ adj₃ : (a : TwoSquare G₁ L₁ L₃ H₁) → TwoSquare R₁ H₁ G₁ R₃) α))
        (hComp (R := H₂) ((mateEquiv adj₄ adj₆ : (a : TwoSquare H₂ L₄ L₆ K₂) → TwoSquare R₄ K₂ H₂ R₆) δ)
          ((mateEquiv adj₃ adj₅ : (a : TwoSquare G₂ L₃ L₅ H₂) → TwoSquare R₃ H₂ G₂ R₅) γ)) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
⊢ Eq (α := TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a : TwoSquare (G₁ ⋙ G₂) (L₁ ⋙ L₂) (L₅ ⋙ L₆) (K₁ ⋙ K₂)) → TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
        ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))
    (vComp (B := R₄ ⋙ R₃)
        (hComp (R := H₁) ((mateEquiv adj₂ adj₄ : (a : TwoSquare H₁ L₂ L₄ K₁) → TwoSquare R₂ K₁ H₁ R₄) β)
          ((mateEquiv adj₁ adj₃ : (a : TwoSquare G₁ L₁ L₃ H₁) → TwoSquare R₁ H₁ G₁ R₃) α))
        (hComp (R := H₂) ((mateEquiv adj₄ adj₆ : (a : TwoSquare H₂ L₄ L₆ K₂) → TwoSquare R₄ K₂ H₂ R₆) δ)
          ((mateEquiv adj₃ adj₅ : (a : TwoSquare G₂ L₃ L₅ H₂) → TwoSquare R₃ H₂ G₂ R₅) γ)) :
      TwoSquare (R₂ ⋙ R₁) (K₁ ⋙ K₂) (G₁ ⋙ G₂) (R₆ ⋙ R₅))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map (app ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α) d) ≫ adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
dsimp :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        (𝟙 (R₁.obj (L₁.obj c)) ≫
            adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                        R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c))) ≫
          𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)
⊢ adj₁.unit.app c ≫ app ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α) (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
dsimp [conjugateEquiv]

Premises used: CategoryTheory.conjugateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
rw :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)
⊢ adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        (𝟙 (R₁.obj (L₁.obj c)) ≫
            adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                        R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c))) ≫
          𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
rw [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
⊢ map (𝟭 C) (adj₁.unit.app c) ≫
      app
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 C) L₁ L₂ (𝟭 D)) → TwoSquare R₁ (𝟭 D) (𝟭 C) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        (L₁.obj c) =
    adj₂.unit.app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c)) ≫
      R₂.map ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app (obj.{v₁, v₁, u₁, u₁} (𝟭 C) c))

Tactic:
have := unit_mateEquiv adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) c
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
this :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
rw : adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)
⊢ adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
this :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
rw : adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c)
| adj₁.unit.app c ≫ α.app (L₁.obj c)

Tactic:
rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Premises used: Equiv.right_inv, CategoryTheory.conjugateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
conv_lhs :
  adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (app (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) c)
⊢ adj₁.unit.app c ≫ α.app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (app (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) c)

Tactic:
conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]

Premises used: Equiv.right_inv, CategoryTheory.conjugateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (app (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) c)

Tactic:
(unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

Premises used: CategoryTheory.unit_conjugateEquiv, CategoryTheory.conjugateEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (app (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) c)

Tactic:
exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

Premises used: CategoryTheory.unit_conjugateEquiv, CategoryTheory.conjugateEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
w : ∀ (x : D), app ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁)) x = app (𝟙 R₁) x
⊢ Eq (α := R₁ ⟶ R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁) : R₁ ⟶ R₁) (𝟙 R₁ : R₁ ⟶ R₁)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
x : D
⊢ app ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁)) x = app (𝟙 R₁) x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
rw : Eq (α := R₁ ⟶ R₁) (𝟙 R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁))
⊢ Eq (α := L₁ ⟶ L₁) (((conjugateEquiv adj₁ adj₁).symm : (a : R₁ ⟶ R₁) → L₁ ⟶ L₁) (𝟙 R₁) : L₁ ⟶ L₁) (𝟙 L₁ : L₁ ⟶ L₁)

Tactic:
rw [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
⊢ Eq (α := R₁ ⟶ R₁) (𝟙 R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁))

Tactic:
simp only [conjugateEquiv_id]

Premises used: CategoryTheory.conjugateEquiv_id
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
L R : Functor.{v₁, v₁, u₁, u₁} C C
adj : L ⊣ R
α : 𝟭 C ⟶ L
c : C
⊢ app ((conjugateEquiv adj Adjunction.id : (a : 𝟭 C ⟶ L) → R ⟶ 𝟭 C) α) c = α.app (R.obj c) ≫ adj.counit.app c

Tactic:
simp [conjugateEquiv, mateEquiv, Adjunction.id]

Premises used: CategoryTheory.conjugateEquiv, CategoryTheory.mateEquiv, CategoryTheory.Adjunction.id
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
L R : Functor.{v₁, v₁, u₁, u₁} C C
adj : L ⊣ R
α : R ⟶ 𝟭 C
c : C
⊢ app (((conjugateEquiv adj Adjunction.id).symm : (a : R ⟶ 𝟭 C) → 𝟭 C ⟶ L) α) c = adj.unit.app c ≫ α.app (L.obj c)

Tactic:
simp [conjugateEquiv, mateEquiv, Adjunction.id]

Premises used: CategoryTheory.conjugateEquiv, CategoryTheory.mateEquiv, CategoryTheory.Adjunction.id
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ L₃ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ R₃ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
w :
  ∀ (d : D),
    Eq.{v₁ + 1} (α := R₁.obj d ⟶ R₃.obj d)
      (app
        (CategoryStruct.comp (Y := R₂) ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α)
          ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃) β))
        d)
      (app ((conjugateEquiv adj₁ adj₃ : (a : L₃ ⟶ L₁) → R₁ ⟶ R₃) (β ≫ α)) d)
⊢ Eq (α := R₁ ⟶ R₃)
    (CategoryStruct.comp (Y := R₂) ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃) β) :
      R₁ ⟶ R₃)
    ((conjugateEquiv adj₁ adj₃ : (a : L₃ ⟶ L₁) → R₁ ⟶ R₃) (β ≫ α) : R₁ ⟶ R₃)

Tactic:
ext d
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ L₃ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ R₃ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
w :
  (𝟙 (R₁.obj d) ≫
        (𝟙 (R₁.obj d) ≫
            adj₂.unit.app (R₁.obj d) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj d))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d) ≫ 𝟙 (R₂.obj d)) ≫
          𝟙 (R₂.obj d)) ≫
      𝟙 (R₂.obj d) ≫
        (𝟙 (R₂.obj d) ≫
            adj₃.unit.app (R₂.obj d) ≫
              𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                𝟙 (R₃.obj (L₃.obj (R₂.obj d))) ≫
                  R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫
                    𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫
                      𝟙 (R₃.obj (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
          𝟙 (R₃.obj d) =
    𝟙 (R₁.obj d) ≫
      (𝟙 (R₁.obj d) ≫
          adj₃.unit.app (R₁.obj d) ≫
            𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
              𝟙 (R₃.obj (L₃.obj (R₁.obj d))) ≫
                R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫
                  𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫
                    𝟙 (R₃.obj (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d) ≫ 𝟙 (R₃.obj d)) ≫
        𝟙 (R₃.obj d)
⊢ Eq.{v₁ + 1} (α := R₁.obj d ⟶ R₃.obj d)
    (app
      (CategoryStruct.comp (Y := R₂) ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃) β))
      d)
    (app ((conjugateEquiv adj₁ adj₃ : (a : L₃ ⟶ L₁) → R₁ ⟶ R₃) (β ≫ α)) d)

Tactic:
dsimp [conjugateEquiv, mateEquiv]

Premises used: CategoryTheory.conjugateEquiv, CategoryTheory.mateEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ L₃ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ R₃ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
⊢ Eq (α := TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
    ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 C ⋙ 𝟭 C) L₁ L₃ (𝟭 D ⋙ 𝟭 D)) → TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
        ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) :
      TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
    (vComp (B := R₂)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 C) L₁ L₂ (𝟭 D)) → TwoSquare R₁ (𝟭 D) (𝟭 C) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
          (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) :
      TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)

Tactic:
have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃
    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)
    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
-- Module: Mathlib.CategoryTheory.Adjunction.Mates
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L₁ L₂ L₃ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ R₂ R₃ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : L₃ ⟶ L₂
d : D
vcomp :
  Eq (α := TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
    ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 C ⋙ 𝟭 C) L₁ L₃ (𝟭 D ⋙ 𝟭 D)) → TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
        ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) :
      TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
    (vComp (B := R₂)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 C) L₁ L₂ (𝟭 D)) → TwoSquare R₁ (𝟭 D) (𝟭 C) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
          (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) :
      TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
⊢ Eq.{v₁ + 1} (α := (R₁ ⋙ 𝟭 C ⋙ 𝟭 C).obj d ⟶ ((𝟭 D ⋙ 𝟭 D) ⋙ R₃).obj d)
    (app
      ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 C ⋙ 𝟭 C) L₁ L₃ (𝟭 D ⋙ 𝟭 D)) → TwoSquare R₁ (𝟭 D ⋙ 𝟭 D) (𝟭 C ⋙ 𝟭 C) R₃)
        ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))
      d)
    (app
      (vComp (B := R₂)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 C) L₁ L₂ (𝟭 D)) → TwoSquare R₁ (𝟭 D) (𝟭 C) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
          (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)))
      d)

Tactic:
have vcompd := congr_app vcomp d