mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
X₃ : C₃
⊢ ((bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫ { app := fun X₃ ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ } ≫ (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map ψ)).app X₃ ≫ (G.map ((F₁₂.map φ).app Y₂)).app X₃ =
    (G.map ((F₁₂.map φ).app X₂)).app X₃ ≫ (G.map ((F₁₂.obj Y₁).map ψ)).app X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
          { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj Y₂)).app X₃, naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ } ≫
          ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ (φ.app ((F₁₂.obj X₁).obj Y₂)).app X₃ =
    (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫ (G'.map ((F₁₂.obj X₁).map f)).app X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (((bifunctorComp₁₂ F₁₂ G).map f ≫
              { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj Y₁).obj X₂)).app X₃, naturality := ⋯ },
                naturality := ⋯ }).app
          X₂).app
      X₃ =
    (({ app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
              (bifunctorComp₁₂ F₁₂ G').map f).app
          X₂).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ (φ.app ((F₁₂.obj Y₁).obj X₂)).app X₃ =
    (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫ (G'.map ((F₁₂.map f).app X₂)).app X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ ((((bifunctorComp₁₂FunctorObj F₁₂).obj G).obj X₁).map f ≫
          { app := fun X₃ ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ } ≫
          (((bifunctorComp₁₂FunctorObj F₁₂').obj G).obj X₁).map f).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ (G.map ((φ.app X₁).app Y₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.obj X₁).map f)).app X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ ((((bifunctorComp₁₂FunctorObj F₁₂).obj G).map f ≫
              { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
                naturality := ⋯ }).app
          X₂).app
      X₃ =
    (({ app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
              ((bifunctorComp₁₂FunctorObj F₁₂').obj G).map f).app
          X₂).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ (G.map ((φ.app Y₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.map f).app X₂)).app X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ C₃ ⥤ C₄
f : G ⟶ G'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ ((((bifunctorComp₁₂FunctorObj F₁₂).map f ≫
                  {
                    app := fun X₁ ↦
                      { app := fun X₂ ↦ { app := fun X₃ ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                        naturality := ⋯ },
                    naturality := ⋯ }).app
              X₁).app
          X₂).app
      X₃ =
    ((({
                    app := fun X₁ ↦
                      { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                        naturality := ⋯ },
                    naturality := ⋯ } ≫
                  (bifunctorComp₁₂FunctorObj F₁₂').map f).app
              X₁).app
          X₂).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ C₃ ⥤ C₄
f : G ⟶ G'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (f.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫ (G'.map ((φ.app X₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (f.app ((F₁₂'.obj X₁).obj X₂)).app X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ✝ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
⊢ { obj := fun X₃ ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃), map := fun {X Y} φ ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ),
            map_id := ⋯, map_comp := ⋯ }.map
        φ ≫
      (F.obj X₁).map ((G₂₃.map φ✝).app Y₃) =
    (F.obj X₁).map ((G₂₃.map φ✝).app X₃) ≫
      { obj := fun X₃ ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃), map := fun {X Y} φ ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ),
            map_id := ⋯, map_comp := ⋯ }.map
        φ

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ✝ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
⊢ (F.obj X₁).map ((G₂₃.obj X₂).map φ) ≫ (F.obj X₁).map ((G₂₃.map φ✝).app Y₃) =
    (F.obj X₁).map ((G₂₃.map φ✝).app X₃) ≫ (F.obj X₁).map ((G₂₃.obj Y₂).map φ)
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f : X₃ ⟶ Y₃
⊢ (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂).map f ≫ (F.obj X₁).map ((φ.app X₂).app Y₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂).map f

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f : X₃ ⟶ Y₃
⊢ (F.obj X₁).map ((G₂₃.obj X₂).map f) ≫ (F.obj X₁).map ((φ.app X₂).app Y₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.obj X₂).map f)
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫ { app := fun X₃ ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ } ≫
          ((bifunctorComp₂₃ F G₂₃').obj X₁).map f).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (F.obj X₁).map ((G₂₃.map f).app X₃) ≫ (F.obj X₁).map ((φ.app Y₂).app X₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.map f).app X₃)
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂₃ ⥤ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ ((((bifunctorComp₂₃FunctorObj F).obj G₂₃).map f ≫
              { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ },
                naturality := ⋯ }).app
          X₂).app
      X₃ =
    (({ app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } ≫
              ((bifunctorComp₂₃FunctorObj F').obj G₂₃).map f).app
          X₂).app
      X₃

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂₃ ⥤ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (F.map f).app ((G₂₃.obj X₂).obj X₃) ≫ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃) =
    (φ.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫ (F'.map f).app ((G₂₃.obj X₂).obj X₃)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ ε (𝟭 C) ≫ adj.unit.app (𝟙_ C) = ε (F ⋙ G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ 𝟙 (𝟙_ C) ≫ adj.unit.app (𝟙_ C) = ε G ≫ G.map (ε F)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C) ≫ 𝟙 (G.obj (F.obj (𝟙_ C)))

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = adj.unit.app (𝟙_ C) ≫ 𝟙 (G.obj (F.obj (𝟙_ C)))
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ μ (𝟭 C) X Y ≫ adj.unit.app (X ⊗ Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ (F ⋙ G) X Y

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ 𝟙 (X ⊗ Y) ≫ adj.unit.app (X ⊗ Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ ε (G ⋙ F) ≫ adj.counit.app (𝟙_ D) = ε (𝟭 D)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ (ε F ≫ F.map (ε G)) ≫ adj.counit.app (𝟙_ D) = 𝟙 (𝟙_ D)
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ μ (G ⋙ F) X Y ≫ adj.counit.app (X ⊗ Y) = (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ μ (𝟭 D) X Y

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ (μ F (G.obj X) (G.obj Y) ≫ F.map (μ G X Y)) ≫ adj.counit.app (X ⊗ Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (X ⊗ Y)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, ((tensorLeft X).mapBicone b).π j ≫ ((tensorLeft X).mapBicone b).ι j = 𝟙 ((tensorLeft X).mapBicone b).pt

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, X ◁ b.π j ≫ X ◁ b.ι j = 𝟙 (X ⊗ b.pt)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, ((tensorRight X).mapBicone b).π j ≫ ((tensorRight X).mapBicone b).ι j = 𝟙 ((tensorRight X).mapBicone b).pt

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, b.π j ▷ X ≫ b.ι j ▷ X = 𝟙 (b.pt ⊗ X)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ (F ⋙ G).obj x✝ ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ (F ⋙ G).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((F ⋙ G).obj x✝²) ((F ⋙ G).obj x✝¹) ((F ⋙ G).obj x✝)).hom ≫
      (F ⋙ G).obj x✝² ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ G.obj (F.obj x✝) ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
⊢ (G.map (δ F X X') ≫ δ G (F.obj X) (F.obj X')) ≫ (F ⋙ G).map f ▷ (F ⋙ G).obj X' =
    (F ⋙ G).map (f ▷ X') ≫ G.map (δ F Y X') ≫ δ G (F.obj Y) (F.obj X')

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
⊢ (G.map (δ F X X') ≫ δ G (F.obj X) (F.obj X')) ≫ G.map (F.map f) ▷ G.obj (F.obj X') =
    G.map (F.map (f ▷ X')) ≫ G.map (δ F Y X') ≫ δ G (F.obj Y) (F.obj X')