mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ } =
    { fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
      { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ } =
    { fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
      { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : CatCommSqOver F G X
⊢ { app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    𝟙
      { obj := fun x ↦ { fst := X✝.fst.obj x, snd := X✝.snd.obj x, iso := X✝.iso.app x },
        map := fun {x y} f ↦ { fst := X✝.fst.map f, snd := X✝.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : CatCommSqOver F G X
⊢ { app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    𝟙
      { obj := fun x ↦ { fst := X✝.fst.obj x, snd := X✝.snd.obj x, iso := X✝.iso.app x },
        map := fun {x y} f ↦ { fst := X✝.fst.map f, snd := X✝.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    { app := fun x ↦ { fst := f✝.fst.app x, snd := f✝.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := g✝.fst.app x, snd := g✝.snd.app x, w := ⋯ }, naturality := ⋯ }

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    { app := fun x ↦ { fst := f✝.fst.app x, snd := f✝.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := g✝.fst.app x, snd := g✝.snd.app x, w := ⋯ }, naturality := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (X ⥤ F ⊡ G)).map f✝ ≫
      (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).snd) ⋯)
          ⋯).hom =
    (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).snd) ⋯)
          ⋯).hom ≫
      (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f✝

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (X ⥤ F ⊡ G)).map f✝ ≫
      (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).snd) ⋯)
          ⋯).hom =
    (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).snd) ⋯)
          ⋯).hom ≫
      (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
X✝ Y✝ : X
f✝ : X✝ ⟶ Y✝
⊢ ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.map f✝ ≫
      (Iso.refl
          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj Y✝)).hom =
    (Iso.refl (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj X✝)).hom ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).fst.map f✝

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
X✝ Y✝ : X
f✝ : X✝ ⟶ Y✝
⊢ ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.map f✝ ≫
      (Iso.refl
          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj Y✝)).hom =
    (Iso.refl (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj X✝)).hom ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).fst.map f✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
X✝ Y✝ : X
f✝ : X✝ ⟶ Y✝
⊢ ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.map f✝ ≫
      (Iso.refl
          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj Y✝)).hom =
    (Iso.refl (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj X✝)).hom ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).snd.map f✝

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
X✝ Y✝ : X
f✝ : X✝ ⟶ Y✝
⊢ ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.map f✝ ≫
      (Iso.refl
          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj Y✝)).hom =
    (Iso.refl (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj X✝)).hom ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).snd.map f✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (whiskerRight
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl
                    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).fst.obj x))
                ⋯).hom
            F ≫
          ((𝟭 (CatCommSqOver F G X)).obj x✝¹).iso.hom).app
      x✝ =
    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).iso.hom ≫
          whiskerRight
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl
                    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).snd.obj x))
                ⋯).hom
            G).app
      x✝

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (whiskerRight
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl
                    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).fst.obj x))
                ⋯).hom
            F ≫
          ((𝟭 (CatCommSqOver F G X)).obj x✝¹).iso.hom).app
      x✝ =
    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).iso.hom ≫
          whiskerRight
            (NatIso.ofComponents
                (fun x ↦
                  Iso.refl
                    (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝¹).snd.obj x))
                ⋯).hom
            G).app
      x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
⊢ (toCatCommSqOver F G X).map
        ((NatIso.ofComponents
                (fun x ↦
                  NatIso.ofComponents
                    (fun x_1 ↦
                      mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                        (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                    ⋯)
                ⋯).hom.app
          X✝) ≫
      (NatIso.ofComponents
              (fun x ↦
                CatCommSqOver.mkIso
                  (NatIso.ofComponents
                    (fun x_1 ↦
                      Iso.refl
                        (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).fst.obj
                          x_1))
                    ⋯)
                  (NatIso.ofComponents
                    (fun x_1 ↦
                      Iso.refl
                        (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).snd.obj
                          x_1))
                    ⋯)
                  ⋯)
              ⋯).hom.app
        ((toCatCommSqOver F G X).obj X✝) =
    𝟙 ((toCatCommSqOver F G X).obj X✝)

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
⊢ (toCatCommSqOver F G X).map
        ((NatIso.ofComponents
                (fun x ↦
                  NatIso.ofComponents
                    (fun x_1 ↦
                      mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                        (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                    ⋯)
                ⋯).hom.app
          X✝) ≫
      (NatIso.ofComponents
              (fun x ↦
                CatCommSqOver.mkIso
                  (NatIso.ofComponents
                    (fun x_1 ↦
                      Iso.refl
                        (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).fst.obj
                          x_1))
                    ⋯)
                  (NatIso.ofComponents
                    (fun x_1 ↦
                      Iso.refl
                        (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).snd.obj
                          x_1))
                    ⋯)
                  ⋯)
              ⋯).hom.app
        ((toCatCommSqOver F G X).obj X✝) =
    𝟙 ((toCatCommSqOver F G X).obj X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
X✝ : CatCommSqOver F G X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ } =
    𝟙
      { fst := X✝.fst ⋙ ψ.left, snd := X✝.snd ⋙ ψ.right,
        iso :=
          X✝.fst.associator ψ.left F₁ ≪≫
            X✝.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
              (X✝.fst.associator F ψ.base).symm ≪≫
                isoWhiskerRight X✝.iso ψ.base ≪≫
                  X✝.snd.associator G ψ.base ≪≫
                    X✝.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (X✝.snd.associator ψ.right G₁).symm }

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
X✝ : CatCommSqOver F G X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ } =
    𝟙
      { fst := X✝.fst ⋙ ψ.left, snd := X✝.snd ⋙ ψ.right,
        iso :=
          X✝.fst.associator ψ.left F₁ ≪≫
            X✝.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
              (X✝.fst.associator F ψ.base).symm ≪≫
                isoWhiskerRight X✝.iso ψ.base ≪≫
                  X✝.snd.associator G ψ.base ≪≫
                    X✝.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (X✝.snd.associator ψ.right G₁).symm }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
X✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := whiskerRight (f✝ ≫ g✝).fst ψ.left, snd := whiskerRight (f✝ ≫ g✝).snd ψ.right, w := ⋯ } =
    { fst := whiskerRight f✝.fst ψ.left, snd := whiskerRight f✝.snd ψ.right, w := ⋯ } ≫
      { fst := whiskerRight g✝.fst ψ.left, snd := whiskerRight g✝.snd ψ.right, w := ⋯ }

Tactic:
;

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
X✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := whiskerRight (f✝ ≫ g✝).fst ψ.left, snd := whiskerRight (f✝ ≫ g✝).snd ψ.right, w := ⋯ } =
    { fst := whiskerRight f✝.fst ψ.left, snd := whiskerRight f✝.snd ψ.right, w := ⋯ } ≫
      { fst := whiskerRight g✝.fst ψ.left, snd := whiskerRight g✝.snd ψ.right, w := ⋯ }
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g'✝

Tactic:
;

Goal state after:
case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ≫ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ≫ projectMapAux f✝¹ g'✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case whiskerLeft
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectObj f✝¹ X✝ ◁ projectMapAux f✝¹ f✝ = projectObj f✝¹ X✝ ◁ projectMapAux f✝¹ f'✝

Tactic:
;

Goal state after:
case whiskerLeft
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectObj f✝¹ X✝ ◁ projectMapAux f✝¹ f✝ = projectObj f✝¹ X✝ ◁ projectMapAux f✝¹ f'✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case whiskerRight
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectMapAux f✝¹ f✝ ▷ projectObj f✝¹ X✝ = projectMapAux f✝¹ f'✝ ▷ projectObj f✝¹ X✝

Tactic:
;

Goal state after:
case whiskerRight
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectMapAux f✝¹ f✝ ▷ projectObj f✝¹ X✝ = projectMapAux f✝¹ f'✝ ▷ projectObj f✝¹ X✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ⊗ₘ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝

Tactic:
;

Goal state after:
case tensor
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ⊗ₘ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝