-- 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₁₀)
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₁₀)
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₁₀)
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₃₂ ⋙ G₂₁ ⋙ G₁₀)) :
      G₃₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
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₃₀ ⟶ 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₁₀)
  (CategoryStruct.comp (Y := (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₂₃ ≫ τ₀₂₃))
      ((conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃) :
          (a : (F₀₁ ⋙ F₁₂) ⋙ F₂₃ ⟶ F₀₁ ⋙ F₁₂ ⋙ F₂₃) → (G₃₂ ⋙ G₂₁) ⋙ G₁₀ ⟶ G₃₂ ⋙ G₂₁ ⋙ G₁₀)
        (F₀₁.associator F₁₂ F₂₃).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₃₀ ⟶ 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]