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 y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ (inv f).snd = inv f.snd

Tactic:
by
  symm
  apply IsIso.inv_eq_of_hom_inv_id
  simp [← comp_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
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
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝) (π₁ F G), snd := whiskerRight (𝟙 X✝) (π₂ F G), w := ⋯ }.fst.app x✝ =
    (𝟙
            { fst := X✝ ⋙ π₁ F G, snd := X✝ ⋙ π₂ F G,
              iso :=
                X✝.associator (π₁ F G) F ≪≫
                  X✝.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X✝.associator (π₂ F G) G).symm }).fst.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₂
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
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝) (π₁ F G), snd := whiskerRight (𝟙 X✝) (π₂ F G), w := ⋯ }.snd.app x✝ =
    (𝟙
            { fst := X✝ ⋙ π₁ F G, snd := X✝ ⋙ π₂ F G,
              iso :=
                X✝.associator (π₁ F G) F ≪≫
                  X✝.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X✝.associator (π₂ F G) G).symm }).snd.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
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✝
x✝ : X
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ }.fst.app x✝ =
    ({ fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
            { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }).fst.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₂
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✝
x✝ : X
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ }.snd.app x✝ =
    ({ fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
            { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }).snd.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hₗ
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
⊢ ({ app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).fst =
    ((𝟙
            { 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 := ⋯ }).app
        x✝).fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hᵣ
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
⊢ ({ app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).snd =
    ((𝟙
            { 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 := ⋯ }).app
        x✝).snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hₗ
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✝
x✝ : X
⊢ ({ app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).fst =
    (({ 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 := ⋯ }).app
        x✝).fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hᵣ
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✝
x✝ : X
⊢ ({ app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ }.app x✝).snd =
    (({ 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 := ⋯ }).app
        x✝).snd

Tactic:
simp

Goal state after:
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
x✝ : X
⊢ F.map (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).fst).hom ≫
      (((toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).obj x✝¹).obj x✝).iso.hom =
    (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).iso.hom ≫ G.map (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).snd).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hₗ
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✝ : X
⊢ (((𝟭 (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).app
        x✝).fst =
    (((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✝).app
        x✝).fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case hᵣ
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✝ : X
⊢ (((𝟭 (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).app
        x✝).snd =
    (((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✝).app
        x✝).snd

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
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
x✝ : X
⊢ ((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✝)).fst.app
      x✝ =
    (𝟙 ((toCatCommSqOver F G X).obj X✝)).fst.app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₂
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
x✝ : X
⊢ ((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✝)).snd.app
      x✝ =
    (𝟙 ((toCatCommSqOver F G X).obj X✝)).snd.app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh)).hom.fst.app x✝ = (CatCommSqOver.mkIso e₁ e₂ ⋯).hom.fst.app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₂
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh)).hom.snd.app x✝ = (CatCommSqOver.mkIso e₁ e₂ ⋯).hom.snd.app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
      LaxMonoidal.μ L' (X ⊗ Y) Z ≫
        L'.map (α_ X Y Z).hom ≫
          OplaxMonoidal.δ L' X (Y ⊗ Z) ≫
            L'.obj X ◁ OplaxMonoidal.δ L' Y Z ≫
              ((((L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
                        LaxMonoidal.μ L' X (Y ⊗ Z) ≫ L'.map (β_ X (Y ⊗ Z)).hom ≫ OplaxMonoidal.δ L' (Y ⊗ Z) X) ≫
                      LaxMonoidal.μ L' (Y ⊗ Z) X) ≫
                    L'.map (α_ Y Z X).hom) ≫
                  OplaxMonoidal.δ L' Y (Z ⊗ X)) ≫
                L'.obj Y ◁ OplaxMonoidal.δ L' Z X =
    ((((LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫ LaxMonoidal.μ L' (X ⊗ Y) Z ≫ L'.map ((β_ X Y).hom ▷ Z)) ≫
            L'.map (α_ Y X Z).hom) ≫
          OplaxMonoidal.δ L' Y (X ⊗ Z)) ≫
        L'.obj Y ◁ OplaxMonoidal.δ L' X Z) ≫
      L'.obj Y ◁ ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case e₁
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₁ F G)).app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case e₂
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
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₂ F G)).app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
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
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ }.fst.app x✝ =
    (𝟙
            { 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 }).fst.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₂
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
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ }.snd.app x✝ =
    (𝟙
            { 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 }).snd.app
      x✝

Tactic:
simp

Goal state after:
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:
hf

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'✝