awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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_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_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₃₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
obtain :
  ∀ (τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃),
    F₀₁.whiskerLeft
          (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
            ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
        adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
      ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
          (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
        (τ₀₁₃ ≫
          whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀)
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀)

Tactic:
obtain ⟨τ₁₂₃, rfl⟩ := (conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)).surjective τ₁₂₃

Premises used: Equiv.surjective, CategoryTheory.conjugateEquiv, CategoryTheory.Adjunction.comp, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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_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_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₃₀
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
obtain :
  ∀ (τ₀₁₃ : F₀₁ ⋙ F₁₃ ⟶ F₀₃),
    F₀₁.whiskerLeft
          (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
            ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
        adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃
          ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → 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₁₀) τ₀₁₃)
          (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀))
⊢ F₀₁.whiskerLeft
        (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
          ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₁₃ ≫
        whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀)

Tactic:
obtain ⟨τ₀₁₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)).surjective τ₀₁₃

Premises used: Equiv.surjective, CategoryTheory.conjugateEquiv, CategoryTheory.Adjunction.comp, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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_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_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₃₀
τ₁₂₃ : 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₀₁.whiskerLeft
            (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
              ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
          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₁₀) τ₀₁₃)
            (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)
              G₁₀))) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
⊢ F₀₁.whiskerLeft
        (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
          ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃
        ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → 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₁₀) τ₀₁₃)
        (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀))

Tactic:
apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective

Premises used: Equiv.injective, CategoryTheory.conjugateEquiv, CategoryTheory.Adjunction.comp
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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_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_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₃₀
τ₁₂₃ : 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₀₁.whiskerLeft
            (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
              ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
          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₁₀) τ₀₁₃)
            (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)
              G₁₀))) :
      G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)

Tactic:
simp [leftAdjointCompNatTrans, ← conjugateEquiv_whiskerLeft _ _ adj₀₁]

Premises used: CategoryTheory.Adjunction.leftAdjointCompNatTrans, CategoryTheory.conjugateEquiv_whiskerLeft
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
obtain :
  ∀ (τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂),
    (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₁₂.comp adj₂₃))).symm :
          (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
        (τ₀₂₃ ≫
          G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
            (G₃₂.associator G₂₁ G₁₀).inv)
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ ≫ (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
obtain ⟨τ₀₁₂, rfl⟩ := (conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).surjective τ₀₁₂

Premises used: Equiv.surjective, CategoryTheory.conjugateEquiv, CategoryTheory.Adjunction.comp, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₃₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
obtain :
  ∀ (τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃),
    (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₂₀) τ₀₂₃) =
      ((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))
⊢ (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₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₂₃ ≫
        G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
obtain ⟨τ₀₂₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)).surjective τ₀₂₃

Premises used: Equiv.surjective, CategoryTheory.conjugateEquiv, CategoryTheory.Adjunction.comp, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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
              (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₁₀)
⊢ (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₂₀) τ₀₂₃) =
    ((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))

Tactic:
apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective

Premises used: Equiv.injective, CategoryTheory.conjugateEquiv, CategoryTheory.Adjunction.comp
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₃₀ ⟶ (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₁₀)
⊢ 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₁₀)

Tactic:
simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, leftAdjointCompNatTrans]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_apply, CategoryTheory.Adjunction.leftAdjointCompNatTrans
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
h : τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ = τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫ adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃

Tactic:
simp [leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm,
    leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm, reassoc_of% h]

Premises used: CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm, CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀₁₃
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
⊢ 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₀₂₃

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀₁₃
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
⊢ (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:
dsimp [leftAdjointCompIso_hom]

Premises used: CategoryTheory.Adjunction.leftAdjointCompIso_hom