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_1 Y : X ⥤ F ⊡ G} (f : X_1 ⟶ 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_1).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X_1).obj x).snd) ⋯)
            ⋯).hom ≫
        (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f

Tactic:
intros

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_1 Y : X} (f : X_1 ⟶ 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_1)).hom ≫
        ((𝟭 (CatCommSqOver F G X)).obj x✝).fst.map f

Tactic:
intros

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_1 Y : X} (f : X_1 ⟶ 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_1)).hom ≫
        ((𝟭 (CatCommSqOver F G X)).obj x✝).snd.map f

Tactic:
intros

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_1 : 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_1) ≫
        (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_1) =
      𝟙 ((toCatCommSqOver F G X).obj X_1)

Tactic:
intros

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_1 : CatCommSqOver F G X),
    { fst := whiskerRight (𝟙 X_1).fst ψ.left, snd := whiskerRight (𝟙 X_1).snd ψ.right, w := ⋯ } =
      𝟙
        { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
          iso :=
            X_1.fst.associator ψ.left F₁ ≪≫
              X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                (X_1.fst.associator F ψ.base).symm ≪≫
                  isoWhiskerRight X_1.iso ψ.base ≪≫
                    X_1.snd.associator G ψ.base ≪≫
                      X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                        (X_1.snd.associator ψ.right G₁).symm }

Tactic:
intros

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_1 Y Z : CatCommSqOver F G X} (f : X_1 ⟶ 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:
intros

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.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
⊢ ∀ (X_1 : CatCospanTransform F G F₁ G₁),
    {
        app := fun S ↦
          { fst := { app := fun y ↦ (𝟙 X_1).left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ (𝟙 X_1).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } =
      𝟙
        {
          obj := fun S ↦
            { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
              iso :=
                S.fst.associator X_1.left F₁ ≪≫
                  S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                    (S.fst.associator F X_1.base).symm ≪≫
                      isoWhiskerRight S.iso X_1.base ≪≫
                        S.snd.associator G X_1.base ≪≫
                          S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                            (S.snd.associator X_1.right G₁).symm },
          map := fun {x y} f ↦ { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
          map_id := ⋯, map_comp := ⋯ }

Tactic:
intros

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
X✝ : CatCospanTransform F G F₁ G₁
⊢ {
      app := fun S ↦
        { fst := { app := fun y ↦ (𝟙 X✝).left.app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun y ↦ (𝟙 X✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
      naturality := ⋯ } =
    𝟙
      {
        obj := fun S ↦
          { fst := S.fst ⋙ X✝.left, snd := S.snd ⋙ X✝.right,
            iso :=
              S.fst.associator X✝.left F₁ ≪≫
                S.fst.isoWhiskerLeft (CatCommSq.iso F X✝.left X✝.base F₁).symm ≪≫
                  (S.fst.associator F X✝.base).symm ≪≫
                    isoWhiskerRight S.iso X✝.base ≪≫
                      S.snd.associator G X✝.base ≪≫
                        S.snd.isoWhiskerLeft (CatCommSq.iso G X✝.right X✝.base G₁) ≪≫
                          (S.snd.associator X✝.right G₁).symm },
        map := fun {x y} f ↦ { fst := whiskerRight f.fst X✝.left, snd := whiskerRight f.snd X✝.right, 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
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_1 Y Z : CatCospanTransform F G F₁ G₁} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    {
        app := fun S ↦
          { fst := { app := fun y ↦ (f ≫ g).left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ (f ≫ g).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } =
      {
          app := fun S ↦
            { fst := { app := fun y ↦ f.left.app (S.fst.obj y), naturality := ⋯ },
              snd := { app := fun y ↦ f.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
          naturality := ⋯ } ≫
        {
          app := fun S ↦
            { fst := { app := fun y ↦ g.left.app (S.fst.obj y), naturality := ⋯ },
              snd := { app := fun y ↦ g.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
          naturality := ⋯ }

Tactic:
intros

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
X✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ {
      app := fun S ↦
        { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
      naturality := ⋯ } =
    {
        app := fun S ↦
          { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } ≫
      {
        app := fun S ↦
          { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
⊢ ∀ (X_1 : CatCommSqOver F G Y),
    { fst := U.whiskerLeft (𝟙 X_1).fst, snd := U.whiskerLeft (𝟙 X_1).snd, w := ⋯ } =
      𝟙
        { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
          iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm }

Tactic:
intros

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ : CatCommSqOver F G Y
⊢ { fst := U.whiskerLeft (𝟙 X✝).fst, snd := U.whiskerLeft (𝟙 X✝).snd, w := ⋯ } =
    𝟙
      { fst := U ⋙ X✝.fst, snd := U ⋙ X✝.snd,
        iso := U.associator X✝.fst F ≪≫ U.isoWhiskerLeft X✝.iso ≪≫ (U.associator X✝.snd 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
⊢ ∀ {X_1 Y_1 Z : CatCommSqOver F G Y} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { fst := U.whiskerLeft (f ≫ g).fst, snd := U.whiskerLeft (f ≫ g).snd, w := ⋯ } =
      { fst := U.whiskerLeft f.fst, snd := U.whiskerLeft f.snd, w := ⋯ } ≫
        { fst := U.whiskerLeft g.fst, snd := U.whiskerLeft g.snd, w := ⋯ }

Tactic:
intros

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ Y✝ Z✝ : CatCommSqOver F G Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := U.whiskerLeft (f✝ ≫ g✝).fst, snd := U.whiskerLeft (f✝ ≫ g✝).snd, w := ⋯ } =
    { fst := U.whiskerLeft f✝.fst, snd := U.whiskerLeft f✝.snd, w := ⋯ } ≫
      { fst := U.whiskerLeft g✝.fst, snd := U.whiskerLeft g✝.snd, 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
⊢ ∀ (X_1 : X ⥤ Y),
    { app := fun x ↦ { fst := whiskerRight (𝟙 X_1) x.fst, snd := whiskerRight (𝟙 X_1) x.snd, w := ⋯ },
        naturality := ⋯ } =
      𝟙
        {
          obj := fun S ↦
            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
              iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm },
          map := fun {S S'} φ ↦ { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ }

Tactic:
intros

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
⊢ { app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ }, naturality := ⋯ } =
    𝟙
      {
        obj := fun S ↦
          { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
            iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
        map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, w := ⋯ }, map_id := ⋯,
        map_comp := ⋯ }
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ F.CoreMonoidal

Tactic:
refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.firstMap (curriedTensorPreIsoPost L W F G).hom =
    LaxMonoidal.ofBifunctor.secondMap (curriedTensorPreIsoPost L W F G).hom

case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapₗ F =
    LaxMonoidal.ofBifunctor.topMapₗ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      (curriedTensorPreIsoPost L W F G).hom.app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapₗ F

case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
⊢ ∀ {X_1 Y_1 Z : X ⥤ Y} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { app := fun x ↦ { fst := whiskerRight (f ≫ g) x.fst, snd := whiskerRight (f ≫ g) x.snd, w := ⋯ },
        naturality := ⋯ } =
      { app := fun x ↦ { fst := whiskerRight f x.fst, snd := whiskerRight f x.snd, w := ⋯ }, naturality := ⋯ } ≫
        { app := fun x ↦ { fst := whiskerRight g x.fst, snd := whiskerRight g x.snd, w := ⋯ }, naturality := ⋯ }

Tactic:
intros

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ Y✝ Z✝ : X ⥤ Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := whiskerRight (f✝ ≫ g✝) x.fst, snd := whiskerRight (f✝ ≫ g✝) x.snd, w := ⋯ },
      naturality := ⋯ } =
    { app := fun x ↦ { fst := whiskerRight f✝ x.fst, snd := whiskerRight f✝ x.snd, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := whiskerRight g✝ x.fst, snd := whiskerRight g✝ x.snd, w := ⋯ }, naturality := ⋯ }