mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ ((λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      (enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      (enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂ ≫ end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫
        (end_.π (diagram V F₁ F₁) j ▷ end_ (diagram V F₁ F₂) ≫
            ((diagram V F₁ F₁).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₁ F₂) j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫
        end_.π (diagram V F₁ F₁) j ▷ end_ (diagram V F₁ F₂) ≫
          ((diagram V F₁ F₁).obj (Opposite.op j)).obj j ◁ end_.π (diagram V F₁ F₂) j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      ((λ_ (enrichedHom V F₁ F₂)).hom ≫
          end_.π (diagram V F₁ F₂) j ≫ (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv) ≫
        eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      (λ_ (enrichedHom V F₁ F₂)).hom ≫
        (end_.π (diagram V F₁ F₂) j ≫ (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv) ≫
          eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      (λ_ (enrichedHom V F₁ F₂)).hom ≫
        (end_.π (diagram V F₁ F₂) j ≫ (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv) ≫
          eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫
      (λ_ (enrichedHom V F₁ F₂)).hom ≫
        end_.π (diagram V F₁ F₂) j ≫
          (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv ≫
            eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
              eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ ((ρ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      (enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂) ≫ end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      (enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂) ≫ end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂ ≫ end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫
        (end_ (diagram V F₁ F₂) ◁ end_.π (diagram V F₂ F₂) j ≫
            end_.π (diagram V F₁ F₂) j ▷ ((diagram V F₂ F₂).obj (Opposite.op j)).obj j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫
        end_ (diagram V F₁ F₂) ◁ end_.π (diagram V F₂ F₂) j ≫
          end_.π (diagram V F₁ F₂) j ▷ ((diagram V F₂ F₂).obj (Opposite.op j)).obj j ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      ((ρ_ (enrichedHom V F₁ F₂)).hom ≫
          end_.π (diagram V F₁ F₂) j ≫ (ρ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv) ≫
        ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ eId V (F₂.obj j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      (ρ_ (enrichedHom V F₁ F₂)).hom ≫
        (end_.π (diagram V F₁ F₂) j ≫ (ρ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv) ≫
          ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ eId V (F₂.obj j) ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      (ρ_ (enrichedHom V F₁ F₂)).hom ≫
        (end_.π (diagram V F₁ F₂) j ≫ (ρ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv) ≫
          ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ eId V (F₂.obj j) ≫
            eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫
      (ρ_ (enrichedHom V F₁ F₂)).hom ≫
        end_.π (diagram V F₁ F₂) j ≫
          (ρ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv ≫
            ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ◁ eId V (F₂.obj j) ≫
              eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| ((α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
      enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄) ≫
    end_.π (diagram V F₁ F₄) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄) ≫ end_.π (diagram V F₁ F₄) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄) ≫ end_.π (diagram V F₁ F₄) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
    enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄ ≫ end_.π (diagram V F₁ F₄) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| (enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄) ≫ end_.π (diagram V F₁ F₄) j

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₃
inst✝³ : HasEnrichedHom V F₁ F₄
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasEnrichedHom V F₂ F₄
inst✝ : HasEnrichedHom V F₃ F₄
j : J
| enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄ ≫ end_.π (diagram V F₁ F₄) j
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst✝¹ : p.IsStronglyCocartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ map p f φ H φ' ≫ map p f' φ' H' φ'' = map p f φ ⋯ φ''

Tactic:
by
  apply map_uniq p f φ
  simp only [fac_assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ (enrichedHomπ V F₁ F₂ (G.obj i) ≫
        eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫ eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i)) ≫
      eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    (enrichedHomπ V F₁ F₂ (G.obj j) ≫
        eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
      eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      (eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫ eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    (enrichedHomπ V F₁ F₂ (G.obj j) ≫
        eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
      eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      (eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫ eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    (enrichedHomπ V F₁ F₂ (G.obj j) ≫
        eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
      eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i) ≫ eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    (enrichedHomπ V F₁ F₂ (G.obj j) ≫
        eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
      eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i) ≫ eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    (enrichedHomπ V F₁ F₂ (G.obj j) ≫
        eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
      eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i) ≫ eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      (eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
        eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i) ≫ eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      (eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
        eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
assoc,

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫
        eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i) ≫ eHomWhiskerLeft V (F₁'.obj i) (F₂'.map f) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j) ≫ eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)