awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃)
vcompd :
  adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d) =
    adj₂.unit.app (R₁.obj d) ≫
      R₂.map (α.app (R₁.obj d)) ≫
        R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d)
w w₁ :
  adj₂.unit.app (R₁.obj d) ≫
      R₂.map (α.app (R₁.obj d)) ≫
        R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d) =
    adj₂.unit.app (R₁.obj d) ≫
      R₂.map (α.app (R₁.obj d)) ≫
        R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d)
⊢ adj₂.unit.app (R₁.obj d) ≫
      R₂.map (α.app (R₁.obj d)) ≫
        R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d) =
    adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d)

Tactic:
rw [vcompd]
-- 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₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
rw :
  CategoryStruct.comp (Y := R₂)
      ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α))
      ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃)
        (((conjugateEquiv adj₂ adj₃).symm : (a : R₂ ⟶ R₃) → L₃ ⟶ L₂) β)) =
    α ≫ β
⊢ Eq (α := L₃ ⟶ L₁)
    (CategoryStruct.comp (Y := L₂) (((conjugateEquiv adj₂ adj₃).symm : (a : R₂ ⟶ R₃) → L₃ ⟶ L₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) :
      L₃ ⟶ L₁)
    (((conjugateEquiv adj₁ adj₃).symm : (a : R₁ ⟶ R₃) → L₃ ⟶ L₁) (α ≫ β) : L₃ ⟶ L₁)

Tactic:
rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]

Premises used: CategoryTheory.conjugateEquiv_comp, Equiv.eq_symm_apply
-- 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₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ CategoryStruct.comp (Y := R₂)
      ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α))
      ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃)
        (((conjugateEquiv adj₂ adj₃).symm : (a : R₂ ⟶ R₃) → L₃ ⟶ L₂) β)) =
    α ≫ β

Tactic:
simp only [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- 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₁
β : L₁ ⟶ L₂
βα : β ≫ α = 𝟙 L₁
rw : Eq (α := R₁ ⟶ R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (β ≫ α) : R₁ ⟶ R₁) (𝟙 R₁ : R₁ ⟶ R₁)
rw₁ : Eq (α := R₁ ⟶ R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁) : R₁ ⟶ R₁) (𝟙 R₁ : R₁ ⟶ R₁)
rw₂ rw₃ : 𝟙 R₁ = 𝟙 R₁
⊢ 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₁)
    (𝟙 R₁ : R₁ ⟶ R₁)

Tactic:
rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

Premises used: CategoryTheory.conjugateEquiv_id, CategoryTheory.conjugateEquiv_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₂
α : R₁ ⟶ R₂
β : R₂ ⟶ R₁
αβ : α ≫ β = 𝟙 R₁
rw : Eq (α := L₁ ⟶ L₁) (((conjugateEquiv adj₁ adj₁).symm : (a : R₁ ⟶ R₁) → L₁ ⟶ L₁) (α ≫ β) : L₁ ⟶ L₁) (𝟙 L₁ : L₁ ⟶ L₁)
rw₁ : Eq (α := L₁ ⟶ L₁) (((conjugateEquiv adj₁ adj₁).symm : (a : R₁ ⟶ R₁) → L₁ ⟶ L₁) (𝟙 R₁) : L₁ ⟶ L₁) (𝟙 L₁ : L₁ ⟶ L₁)
rw₂ rw₃ : 𝟙 L₁ = 𝟙 L₁
⊢ Eq (α := L₁ ⟶ L₁)
    (CategoryStruct.comp (Y := L₂) (((conjugateEquiv adj₂ adj₁).symm : (a : R₂ ⟶ R₁) → L₁ ⟶ L₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) :
      L₁ ⟶ L₁)
    (𝟙 L₁ : L₁ ⟶ L₁)

Tactic:
rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

Premises used: CategoryTheory.conjugateEquiv_symm_id, CategoryTheory.conjugateEquiv_symm_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₁
inst_2 : IsIso α
⊢ inv α ≫ α = 𝟙 L₁

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₁
inst_2 : IsIso α
⊢ α ≫ inv α = 𝟙 L₂

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₂
inst_2 : IsIso α
⊢ inv α ≫ α = 𝟙 R₂

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₂
inst_2 : IsIso α
⊢ α ≫ inv α = 𝟙 R₁

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₁
inst_2 : IsIso (X := R₁) ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α : R₁ ⟶ R₂)
this :
  IsIso (C := Functor.{v₁, v₂, u₁, u₂} C D) (X := L₂) (Y := L₁)
    (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁)
        ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α) :
      L₂ ⟶ L₁)
⊢ IsIso α

Tactic:
simpa using 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₁
inst_2 : IsIso (X := R₁) ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α : R₁ ⟶ R₂)
suffices :
  IsIso (C := Functor.{v₁, v₂, u₁, u₂} C D) (X := L₂) (Y := L₁)
    (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁)
        ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α) :
      L₂ ⟶ L₁)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α)) by simpa using 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₁
inst_2 : IsIso (X := R₁) ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α : R₁ ⟶ R₂)
⊢ IsIso (C := Functor.{v₁, v₂, u₁, u₂} C D) (X := L₂) (Y := L₁)
    (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁)
        ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) α) :
      L₂ ⟶ L₁)

Tactic:
infer_instance
-- 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₂
inst_2 : IsIso (X := L₂) (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α : L₂ ⟶ L₁)
this :
  IsIso (C := Functor.{v₂, v₁, u₂, u₁} D C) (X := R₁) (Y := R₂)
    ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) :
      R₁ ⟶ R₂)
⊢ IsIso α

Tactic:
simpa using 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₂
α : R₁ ⟶ R₂
inst_2 : IsIso (X := L₂) (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α : L₂ ⟶ L₁)
suffices :
  IsIso (C := Functor.{v₂, v₁, u₂, u₁} D C) (X := R₁) (Y := R₂)
    ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) :
      R₁ ⟶ R₂)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa using 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₂
α : R₁ ⟶ R₂
inst_2 : IsIso (X := L₂) (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α : L₂ ⟶ L₁)
⊢ IsIso (C := Functor.{v₂, v₁, u₂, u₁} D C) (X := R₁) (Y := R₂)
    ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : R₁ ⟶ R₂) → L₂ ⟶ L₁) α) :
      R₁ ⟶ R₂)

Tactic:
infer_instance
-- 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
F₁ : Functor.{v₁, v₃, u₁, u₃} A C
U₁ : Functor.{v₃, v₁, u₃, u₁} C A
F₂ : Functor.{v₂, v₄, u₂, u₄} B D
U₂ : Functor.{v₄, v₂, u₄, u₂} D B
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₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
w :
  ∀ (d : D),
    Eq.{v₁ + 1} (α := (U₂ ⋙ R₁).obj d ⟶ (R₂ ⋙ U₁).obj d)
      (app
        (natTrans
          ((mateEquiv adj₄ adj₃ : (a : TwoSquare R₁ F₂ F₁ R₂) → TwoSquare U₂ R₂ R₁ U₁)
            ((mateEquiv adj₁ adj₂ : (a : TwoSquare F₁ L₁ L₂ F₂) → TwoSquare R₁ F₂ F₁ R₂) α)))
        d)
      (app ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) : (a : F₁ ⋙ L₂ ⟶ L₁ ⋙ F₂) → U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) α) d)
⊢ Eq (α := U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁)
    (natTrans
      ((mateEquiv adj₄ adj₃ : (a : TwoSquare R₁ F₂ F₁ R₂) → TwoSquare U₂ R₂ R₁ U₁)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare F₁ L₁ L₂ F₂) → TwoSquare R₁ F₂ F₁ R₂) α)))
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) : (a : F₁ ⋙ L₂ ⟶ L₁ ⋙ F₂) → U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) α)

Tactic:
ext d
-- 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
F₁ : Functor.{v₁, v₃, u₁, u₃} A C
U₁ : Functor.{v₃, v₁, u₃, u₁} C A
F₂ : Functor.{v₂, v₄, u₂, u₄} B D
U₂ : Functor.{v₄, v₂, u₄, u₂} D B
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₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
d : D
⊢ Eq.{v₁ + 1} (α := (U₂ ⋙ R₁).obj d ⟶ (R₂ ⋙ U₁).obj d)
    (app
      (natTrans
        ((mateEquiv adj₄ adj₃ : (a : TwoSquare R₁ F₂ F₁ R₂) → TwoSquare U₂ R₂ R₁ U₁)
          ((mateEquiv adj₁ adj₂ : (a : TwoSquare F₁ L₁ L₂ F₂) → TwoSquare R₁ F₂ F₁ R₂) α)))
      d)
    (app ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) : (a : F₁ ⋙ L₂ ⟶ L₁ ⋙ F₂) → U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) α) d)

Tactic:
simp
-- 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
F₁ : Functor.{v₁, v₃, u₁, u₃} A C
U₁ : Functor.{v₃, v₁, u₃, u₁} C A
F₂ : Functor.{v₂, v₄, u₂, u₄} B D
U₂ : Functor.{v₄, v₂, u₄, u₂} D B
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₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare U₂ R₂ R₁ U₁
h :
  ∀ (X : A),
    Eq.{v₄ + 1} (α := (F₁ ⋙ L₂).obj X ⟶ (L₁ ⋙ F₂).obj X)
      (app
        (natTrans
          ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ F₂ F₁ R₂) → TwoSquare F₁ L₁ L₂ F₂)
            ((Equiv.symm (mateEquiv adj₄ adj₃) : (a : TwoSquare U₂ R₂ R₁ U₁) → TwoSquare R₁ F₂ F₁ R₂) α)))
        X)
      (app
        (natTrans
          (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm :
              (a : U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) → TwoSquare F₁ L₁ L₂ F₂)
            α))
        X)
⊢ Eq (α := TwoSquare F₁ L₁ L₂ F₂)
    ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ F₂ F₁ R₂) → TwoSquare F₁ L₁ L₂ F₂)
        ((Equiv.symm (mateEquiv adj₄ adj₃) : (a : TwoSquare U₂ R₂ R₁ U₁) → TwoSquare R₁ F₂ F₁ R₂) α) :
      TwoSquare F₁ L₁ L₂ F₂)
    (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm :
          (a : U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) → TwoSquare F₁ L₁ L₂ F₂)
        α :
      TwoSquare F₁ L₁ L₂ F₂)

Tactic:
ext
-- 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
F₁ : Functor.{v₁, v₃, u₁, u₃} A C
U₁ : Functor.{v₃, v₁, u₃, u₁} C A
F₂ : Functor.{v₂, v₄, u₂, u₄} B D
U₂ : Functor.{v₄, v₂, u₄, u₂} D B
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₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare U₂ R₂ R₁ U₁
X : A
⊢ Eq.{v₄ + 1} (α := (F₁ ⋙ L₂).obj X ⟶ (L₁ ⋙ F₂).obj X)
    (app
      (natTrans
        ((Equiv.symm (mateEquiv adj₁ adj₂) : (a : TwoSquare R₁ F₂ F₁ R₂) → TwoSquare F₁ L₁ L₂ F₂)
          ((Equiv.symm (mateEquiv adj₄ adj₃) : (a : TwoSquare U₂ R₂ R₁ U₁) → TwoSquare R₁ F₂ F₁ R₂) α)))
      X)
    (app
      (natTrans
        (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm :
            (a : U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁) → TwoSquare F₁ L₁ L₂ F₂)
          α))
      X)

Tactic:
simp
-- 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₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
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₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
h :
  ∀ (b : 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₃) (α.whiskerRight β))) b)
      (app
        (natTrans
          (TwoSquare.whiskerBottom (B := R₂) ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)
            ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃) β)))
        b)
⊢ Eq (α := TwoSquare R₁ H G R₃)
    ((mateEquiv adj₁ adj₃ : (a : TwoSquare G L₁ L₃ H) → TwoSquare R₁ H G R₃) (α.whiskerRight β) : TwoSquare R₁ H G R₃)
    (TwoSquare.whiskerBottom (B := R₂) ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : L₃ ⟶ L₂) → R₂ ⟶ R₃) β) :
      TwoSquare R₁ H G R₃)

Tactic:
ext 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₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
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₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃ : (a : TwoSquare (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)) → TwoSquare R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
            (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)) =
    TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
      ((R₁.associator G (𝟭 C)).inv ≫
        whiskerRight (natTrans ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)) (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).hom ≫
            H.whiskerLeft
                (natTrans
                  ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
                    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))) ≫
              (H.associator (𝟭 D) R₃).inv)
⊢ app
      ((mateEquiv adj₁ adj₃ : (a : TwoSquare (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)) → TwoSquare R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃)
        (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
          ((G.associator (𝟭 C) L₃).hom ≫
            G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
              (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)))
      b =
    (TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
          ((R₁.associator G (𝟭 C)).inv ≫
            whiskerRight (natTrans ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)) (𝟭 C) ≫
              (H.associator R₂ (𝟭 C)).hom ≫
                H.whiskerLeft
                    (natTrans
                      ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
                        (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))) ≫
                  (H.associator (𝟭 D) R₃).inv)).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₄} C D
R₂ : Functor.{v₄, v₃, u₄, u₃} D C
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₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃ : (a : TwoSquare (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)) → TwoSquare R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
            (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)) =
    TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
      ((R₁.associator G (𝟭 C)).inv ≫
        whiskerRight (natTrans ((mateEquiv adj₁ adj₂ : (a : TwoSquare G L₁ L₂ H) → TwoSquare R₁ H G R₂) α)) (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).hom ≫
            H.whiskerLeft
                (natTrans
                  ((mateEquiv adj₂ adj₃ : (a : TwoSquare (𝟭 C) L₂ L₃ (𝟭 D)) → TwoSquare R₂ (𝟭 D) (𝟭 C) R₃)
                    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))) ≫
              (H.associator (𝟭 D) R₃).inv)
vcompb :
  adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.app (G.obj (R₁.obj b))) ≫ R₃.map (α.natTrans.app (R₁.obj b)) ≫ R₃.map (H.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)) ≫
          adj₃.unit.app (R₂.obj (H.obj b)) ≫ R₃.map (β.app (R₂.obj (H.obj b))) ≫ R₃.map (adj₂.counit.app (H.obj 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₃) (α.whiskerRight β))) b)
    (app
      (natTrans
        (TwoSquare.whiskerBottom (B := 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
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
h :
  ∀ (b : 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)
⊢ Eq (α := TwoSquare R₁ H G R₃)
    ((mateEquiv adj₁ adj₃ : (a : TwoSquare G L₁ L₃ H) → TwoSquare R₁ H G R₃) (β.whiskerLeft α) : TwoSquare R₁ H G R₃)
    (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₂) α) :
      TwoSquare R₁ H G R₃)

Tactic:
ext 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
⊢ Eq (α := TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
    ((mateEquiv adj₁ adj₃ : (a : TwoSquare (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)) → TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
        ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ β) :
      TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)
    (vComp (B := R₂)
        ((mateEquiv adj₁ adj₂ : (a : TwoSquare (𝟭 A) L₁ L₂ (𝟭 B)) → TwoSquare R₁ (𝟭 B) (𝟭 A) R₂)
          (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv))
        ((mateEquiv adj₂ adj₃ : (a : TwoSquare G L₂ L₃ H) → TwoSquare R₂ H G R₃) β) :
      TwoSquare R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃)

Tactic:
have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β