awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : 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
G : Functor.{v₁, v₄, u₁, u₄} A D
H : Functor.{v₂, v₅, u₂, u₅} B E
K : Functor.{v₃, v₆, u₃, u₆} C F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₄, v₅, u₄, u₅} D E
R₂ : Functor.{v₅, v₄, u₅, u₄} E D
L₃ : Functor.{v₂, v₃, u₂, u₃} B C
R₃ : Functor.{v₃, v₂, u₃, u₂} C B
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ Eq (α := G.obj (R₁.obj (R₃.obj c)) ⟶ R₂.obj (R₄.obj (K.obj c)))
    (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))))
    (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      (R₂.map
            (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
              R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c))))
have h : Eq (α := G.obj (R₁.obj (R₃.obj c)) ⟶ R₂.obj (R₄.obj (K.obj c)))
  (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
    R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
      R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))))
  (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
    ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c)))))) ≫
        R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
      R₂.map (R₄.map (K.map (adj₃.counit.app c))))
Tactic: rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : 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
G : Functor.{v₁, v₄, u₁, u₄} A D
H : Functor.{v₂, v₅, u₂, u₅} B E
K : Functor.{v₃, v₆, u₃, u₆} C F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₄, v₅, u₄, u₅} D E
R₂ : Functor.{v₅, v₄, u₅, u₄} E D
L₃ : Functor.{v₂, v₃, u₂, u₃} B C
R₃ : Functor.{v₃, v₂, u₃, u₂} C B
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
| R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))
have a : R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))) ≫ (L₃ ⋙ K).map (adj₁.counit.app (R₃.obj c))))
Tactic: rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄, β.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (goal)
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : 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
G : Functor.{v₁, v₄, u₁, u₄} A D
H : Functor.{v₂, v₅, u₂, u₅} B E
K : Functor.{v₃, v₆, u₃, u₆} C F
L₁ : Functor.{v₁, v₂, u₁, u₂} A B
R₁ : Functor.{v₂, v₁, u₂, u₁} B A
L₂ : Functor.{v₄, v₅, u₄, u₅} D E
R₂ : Functor.{v₅, v₄, u₅, u₄} E D
L₃ : Functor.{v₂, v₃, u₂, u₃} B C
R₃ : Functor.{v₃, v₂, u₃, u₂} C B
L₄ : Functor.{v₅, v₆, u₅, u₆} E F
R₄ : Functor.{v₆, v₅, u₆, u₅} F E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ Eq (α := G.obj (R₁.obj (R₃.obj c)) ⟶ R₂.obj (R₄.obj (K.obj c)))
    (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))))
    (adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
              R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c)))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c))))
have h : adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
    R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
      R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
  adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
    R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
      R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))) ≫ (L₃ ⋙ K).map (adj₁.counit.app (R₃.obj c)))) ≫
          R₂.map (R₄.map (K.map (adj₃.counit.app c)))
Tactic: slice_rhs 4 5 =>
    rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄, β.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Mates (hypothesis)
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₂
⊢ 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₅))
have 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₅))
Tactic: have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.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₁
c : 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)
have 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)
Tactic: dsimp [conjugateEquiv]
-- 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₁
c : 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)
have 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)
Tactic: rw [id_comp, comp_id]
-- 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₂ : 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
⊢ 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)
have this : 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
-- 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₁
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₁.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)
have rw : adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)
Tactic: rw [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₂
c : C
| adj₁.unit.app c ≫ α.app (L₁.obj c)
have rw : adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c)
Tactic: rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
-- 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₂
c : 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)
have 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)
Tactic: conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
-- 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₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
⊢ Eq (α := R₁ ⟶ R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁) : R₁ ⟶ R₁) (𝟙 R₁ : R₁ ⟶ R₁)
have w : ∀ (x : D), app ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁)) x = app (𝟙 R₁) x
Tactic: ext
-- 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₁ : Functor.{v₁, v₂, u₁, u₂} C D
R₁ : Functor.{v₂, v₁, u₂, u₁} D C
adj₁ : L₁ ⊣ R₁
⊢ Eq (α := L₁ ⟶ L₁) (((conjugateEquiv adj₁ adj₁).symm : (a : R₁ ⟶ R₁) → L₁ ⟶ L₁) (𝟙 R₁) : L₁ ⟶ L₁) (𝟙 L₁ : L₁ ⟶ L₁)
have rw : Eq (α := R₁ ⟶ R₁) (𝟙 R₁) ((conjugateEquiv adj₁ adj₁ : (a : L₁ ⟶ L₁) → R₁ ⟶ R₁) (𝟙 L₁))
Tactic: rw [Equiv.symm_apply_eq]
-- 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₂
⊢ 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₃)
have 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)
Tactic: ext 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
⊢ 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)
have 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)
Tactic: dsimp [conjugateEquiv, mateEquiv]
-- 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
⊢ (𝟙 (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 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₃)
Tactic: have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃
    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)
    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)