awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ Eq (α := G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
        ((F₀₁.associator F₁₂ F₂₃).inv ≫
          whiskerRight
              (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂
                ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂))
              F₂₃ ≫
            adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃
              ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
        (((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
            (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
          (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
            ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
            (G₃₂.whiskerLeft
                ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
              (G₃₂.associator G₂₁ G₁₀).inv))) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
have a : Eq (α := G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
      ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) :
    G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
  (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
      ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
      (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
        (G₃₂.associator G₂₁ G₁₀).inv) :
    G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
Tactic: simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, leftAdjointCompNatTrans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ Eq (α := G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
        ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
    (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
        ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
        (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
have a : Eq (α := G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
        ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom :
    G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
  (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
        ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
        (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv) ≫
      (G₃₂.associator G₂₁ G₁₀).hom :
    G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
Tactic: rw [← cancel_mono (associator G₃₂ G₂₁ G₁₀).hom, Category.assoc, Category.assoc,
    Iso.inv_hom_id, Category.comp_id, ← conjugateEquiv_associator_hom adj₀₁ adj₁₂ adj₂₃,
    ← conjugateEquiv_whiskerRight _ _ adj₂₃, conjugateEquiv_comp, Iso.hom_inv_id_assoc,
    conjugateEquiv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
a :
  Eq (α := G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
          ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
        (G₃₂.associator G₂₁ G₁₀).hom :
      G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
    (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
          ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
          (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
            (G₃₂.associator G₂₁ G₁₀).inv) ≫
        (G₃₂.associator G₂₁ G₁₀).hom :
      G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
⊢ Eq (α := G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
        ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
    (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
        ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
        (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
have a₁ : Eq (α := G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
        ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom :
    G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
  (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
      ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
      ((G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv) ≫
        (G₃₂.associator G₂₁ G₁₀).hom) :
    G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
Tactic: rw [← cancel_mono (associator G₃₂ G₂₁ G₁₀).hom, Category.assoc, Category.assoc,
    Iso.inv_hom_id, Category.comp_id, ← conjugateEquiv_associator_hom adj₀₁ adj₁₂ adj₂₃,
    ← conjugateEquiv_whiskerRight _ _ adj₂₃, conjugateEquiv_comp, Iso.hom_inv_id_assoc,
    conjugateEquiv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ =
    (F₀₁.associator F₁₂ F₂₃).symm ≪≫
      isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫ adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃
have w : (F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃).hom =
  ((F₀₁.associator F₁₂ F₂₃).symm ≪≫
      isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫ adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃).hom
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ (F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃).hom =
    ((F₀₁.associator F₁₂ F₂₃).symm ≪≫
        isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫
          adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃).hom
have w : F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ e₁₂₃.inv) ≫
    adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ e₀₁₃.inv =
  (F₀₁.associator F₁₂ F₂₃).inv ≫
    whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ e₀₁₂.inv) F₂₃ ≫
      adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ e₀₂₃.inv
Tactic: dsimp [leftAdjointCompIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
x d₂ : D
f : x ⟶ d₂
X Y : C
f_1 : X ⟶ Y
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom.{v₂, u₂} (V := D)
      (Functor.obj.{v₁, v₂, u₁, u₂}
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ t) ↦ x,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ }
        X)
      (Functor.obj.{v₁, v₂, u₁, u₂}
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ t) ↦ d₂,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ }
        Y))
    (Functor.map
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ t) ↦ x,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }
        f_1 ≫
      Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h)
    ((Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h) ≫
      Functor.map
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ t) ↦ d₂,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }
        f_1)
have dsimp : Eq.{v₂ + 1} (α :=
  Quiver.Hom.{v₂, u₂} (V := D) (sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
    (sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂))
  (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
    (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
    (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h))
  (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
    (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
    (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
x d₂ : D
f : x ⟶ d₂
X Y : C
f_1 : X ⟶ Y
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
      (sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂))
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
      (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
      (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h))
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
      (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
      (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1)))
have h : ∀ (b : c ⟶ X),
  Eq.{v₂ + 1} (α := x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
        (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ X) ↦ x) b)
        (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
          (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
          (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h)) :
      x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
        (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ X) ↦ x) b)
        (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
          (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
          (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1))) :
      x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
⊢ (fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
        ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := ⋯ } :
          NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
      ((fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
          Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
        f) =
    f
have w : ∀ (x : C),
  NatTrans.app
      ((fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
          ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := sorry } :
            NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
        ((fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
            Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
          f))
      x =
    f.app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
x : C
⊢ NatTrans.app
      ((fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
          ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := ⋯ } :
            NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
        ((fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
            Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
          f))
      x =
    f.app x
have w : (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) = f.app x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
x : C
⊢ (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    f.app x
have w : ∀ (g : c ⟶ x),
  CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ x) ↦ d)
      (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ x) ↦ d) g)
      (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ x) ↦ d) g ≫ f.app x
Tactic: ext g
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
⊢ Mono η ↔ ∀ (c : C), Mono (η.app c)
have mp : Mono η → ∀ (c : C), Mono (η.app c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
mp : Mono η → ∀ (c : C), Mono (η.app c)
⊢ Mono η ↔ ∀ (c : C), Mono (η.app c)
have mpr : (∀ (c : C), Mono (η.app c)) → Mono η
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
⊢ (fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
        ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := ⋯ } :
          NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
      ((fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) f) =
    f
have w : ∀ (x : C),
  NatTrans.app
      ((fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
          ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := sorry } :
            NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
        ((fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) f))
      x =
    f.app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
x : C
⊢ NatTrans.app
      ((fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
          ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := ⋯ } :
            NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
        ((fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) f))
      x =
    f.app x
have w : (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) = f.app x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
x : C
⊢ (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) = f.app x
have w : ∀ (g : x ⟶ c),
  CategoryStruct.comp (Y := piObj.{v₁, v₂, u₂} fun (x : x ⟶ c) ↦ d)
      (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) (Pi.π (fun (x : x ⟶ c) ↦ d) g) =
    f.app x ≫ Pi.π (fun (x : x ⟶ c) ↦ d) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)
have mp : Epi η → ∀ (c : C), Epi (η.app c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Evaluation (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
mp : Epi η → ∀ (c : C), Epi (η.app c)
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)
have mpr : (∀ (c : C), Epi (η.app c)) → Epi η
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f = g
have a : f ≫ h.unit.app Y = g ≫ h.unit.app Y
Tactic: apply Mono.right_cancellation (f := h.unit.app Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.FullyFaithful (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f ≫ h.unit.app Y = g ≫ h.unit.app Y
have a : Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
  (((Equiv.symm (h.homEquiv X (L.obj Y)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ R.obj (L.obj Y)) (L.obj X ⟶ L.obj Y)) :
        (a : X ⟶ R.obj (L.obj Y)) → L.obj X ⟶ L.obj Y)
      (f ≫ h.unit.app Y) :
    L.obj X ⟶ L.obj Y)
  (((Equiv.symm (h.homEquiv X (L.obj Y)) : Equiv.{v₁ + 1, v₂ + 1} (X ⟶ R.obj (L.obj Y)) (L.obj X ⟶ L.obj Y)) :
        (a : X ⟶ R.obj (L.obj Y)) → L.obj X ⟶ L.obj Y)
      (g ≫ h.unit.app Y) :
    L.obj X ⟶ L.obj Y)
Tactic: apply (h.homEquiv X (L.obj Y)).symm.injective