awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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₃))
⊢ 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)
have vcompb : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₃₂
⊢ (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
have 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
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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
⊢ 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
have 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)))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁
⊢ 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)
have 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)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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 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)
have 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))))
Tactic: have h₁ := congr_map (R₂ ⋙ R) (τ.naturality (adj.counit.app (R₁.obj X)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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₁ ⋙ 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)
have 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))))
Tactic: have h₂ := congr_map R (adj₂.unit_naturality (adj.counit.app (R₁.obj X)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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₁ ⋙ 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)
have 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))))
Tactic: simp only [comp_obj, id_obj, Functor.map_comp] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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₁ ⋙ 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)
have 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)))
Tactic: simp only [comp_obj, id_obj, Functor.map_comp] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁
⊢ 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₂)
have 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)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Opposites (goal)
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
⊢ a.leftOp = comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op
have h : ∀ (X : D),
  a.leftOp.unit.app X =
    NatTrans.app (unit (comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op)) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Opposites (goal)
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
⊢ a.rightOp = comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op
have h : ∀ (X : D),
  a.rightOp.unit.app X =
    NatTrans.app (unit (comp (Equivalence.toAdjunction (Equivalence.symm (opOpEquivalence D))) a.op)) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Parametrized (goal)
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₁
⊢ (adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁)) = (adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)
have 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₂
Tactic: ext X₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Parametrized (hypothesis)
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₃
⊢ 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₃)
have this : ((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₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Parametrized (goal)
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₁
⊢ (G.obj (op Y₁)).whiskerLeft (F.map f) ≫ (adj₂.adj Y₁).counit =
    whiskerRight (G.map f.op) (F.obj X₁) ≫ (adj₂.adj X₁).counit
have 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₃
Tactic: ext X₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Parametrized (goal)
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₃
⊢ ((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₃
have 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₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Parametrized (goal)
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₃
⊢ (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₃
have 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₃)
Tactic: apply adj₂.homEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Parametrized (goal)
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 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₃)
have 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₃)
Tactic: rw [homEquiv_naturality_one, homEquiv_naturality_two]