awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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₃)
⊢ (𝟙 (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)
have vcompd : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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)
⊢ 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)
have 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)
Tactic: rw [vcompd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₃
⊢ 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₁)
have 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₂) β)) =
  α ≫ β
Tactic: rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁
⊢ 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₁)
have rw : Eq (α := R₁ ⟶ R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (β ≫ α) : R₁ ⟶ R₁) (𝟙 R₁ : R₁ ⟶ R₁)
Tactic: rw [conjugateEquiv_comp, βα, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁)
⊢ 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₁)
have rw₁ : Eq (α := R₁ ⟶ R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁) : R₁ ⟶ R₁) (𝟙 R₁ : R₁ ⟶ R₁)
Tactic: rw [conjugateEquiv_comp, βα, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁)
⊢ 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₁)
have rw₂ : 𝟙 R₁ = 𝟙 R₁
Tactic: rw [conjugateEquiv_comp, βα, conjugateEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁
⊢ 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₁)
have rw : Eq (α := L₁ ⟶ L₁) (((conjugateEquiv adj₁ adj₁).symm : (a : R₁ ⟶ R₁) → L₁ ⟶ L₁) (α ≫ β) : L₁ ⟶ L₁) (𝟙 L₁ : L₁ ⟶ L₁)
Tactic: rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁)
⊢ 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₁)
have rw₁ : Eq (α := L₁ ⟶ L₁) (((conjugateEquiv adj₁ adj₁).symm : (a : R₁ ⟶ R₁) → L₁ ⟶ L₁) (𝟙 R₁) : L₁ ⟶ L₁) (𝟙 L₁ : L₁ ⟶ L₁)
Tactic: rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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₁)
⊢ 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₁)
have rw₂ : 𝟙 L₁ = 𝟙 L₁
Tactic: rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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 α
have 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₁)
Tactic: suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α)) by simpa using this
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
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 α
have 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₂)
Tactic: suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa using this
-- 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
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₂
⊢ 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₁) α)
have 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)
Tactic: ext d
-- 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
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₁
⊢ 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₂)
have 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)
Tactic: ext
-- 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
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₂
⊢ 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₃)
have 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)
Tactic: ext b
-- 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₄} 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)
⊢ 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)
have vcompb : 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
-- 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
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
⊢ 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₃)
have 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)
Tactic: ext b
-- 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
⊢ 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 vcomp : 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) β