mathlib-initiative/mathlib-tactics huggingface dataset:
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:
hf

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.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✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝ : X
⊢ { fst := whiskerRight (f✝ ≫ g✝).fst ψ.left, snd := whiskerRight (f✝ ≫ g✝).snd ψ.right, w := ⋯ }.fst.app x✝ =
    ({ fst := whiskerRight f✝.fst ψ.left, snd := whiskerRight f✝.snd ψ.right, w := ⋯ } ≫
            { fst := whiskerRight g✝.fst ψ.left, snd := whiskerRight g✝.snd ψ.right, 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
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✝
x✝ : X
⊢ { fst := whiskerRight (f✝ ≫ g✝).fst ψ.left, snd := whiskerRight (f✝ ≫ g✝).snd ψ.right, w := ⋯ }.snd.app x✝ =
    ({ fst := whiskerRight f✝.fst ψ.left, snd := whiskerRight f✝.snd ψ.right, w := ⋯ } ≫
            { fst := whiskerRight g✝.fst ψ.left, snd := whiskerRight g✝.snd ψ.right, w := ⋯ }).snd.app
      x✝

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

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
⊢ L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
      LaxMonoidal.μ L' X (Y ⊗ Z) ≫
        L'.map (α_ X Y Z).inv ≫
          OplaxMonoidal.δ L' (X ⊗ Y) Z ≫
            OplaxMonoidal.δ L' X Y ▷ L'.obj Z ≫
              ((((LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
                        LaxMonoidal.μ L' (X ⊗ Y) Z ≫ L'.map (β_ (X ⊗ Y) Z).hom ≫ OplaxMonoidal.δ L' Z (X ⊗ Y)) ≫
                      LaxMonoidal.μ L' Z (X ⊗ Y)) ≫
                    L'.map (α_ Z X Y).inv) ≫
                  OplaxMonoidal.δ L' (Z ⊗ X) Y) ≫
                OplaxMonoidal.δ L' Z X ▷ L'.obj Y =
    ((((L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
              L'.obj X ◁ L'.map (β_ Y Z).hom ≫
                L'.obj X ◁ OplaxMonoidal.δ L' Z Y ≫ L'.obj X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (Z ⊗ Y)) ≫
            L'.map (α_ X Z Y).inv) ≫
          OplaxMonoidal.δ L' (X ⊗ Z) Y) ≫
        OplaxMonoidal.δ L' X Z ▷ L'.obj Y) ≫
      ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X) ▷ L'.obj Y

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
X✝ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                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 := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    ((𝟙
                {
                  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 := ⋯ }).app
            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
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₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                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 := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    ((𝟙
                {
                  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 := ⋯ }).app
            x✝¹).snd.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
F₁ F₂ : C ⥤ E
F₁' F₂' : D ⥤ E
inst✝² : Lifting L W F₁ F₁'
inst✝¹ : Lifting L W F₂ F₂'
inst✝ : HasZeroMorphisms E
⊢ ∀ (X : C), (liftNatTrans L W F₁ F₂ F₁' F₂' 0).app (L.obj X) = NatTrans.app 0 (L.obj X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Preadditive E
F₁ F₂ : C ⥤ E
F₁' F₂' : D ⥤ E
inst✝¹ : Lifting L W F₁ F₁'
inst✝ : Lifting L W F₂ F₂'
τ τ' : F₁ ⟶ F₂
⊢ ∀ (X : C),
    (liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ')).app (L.obj X) =
      (liftNatTrans L W F₁ F₂ F₁' F₂' τ + liftNatTrans L W F₁ F₂ F₁' F₂' τ').app (L.obj 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
X✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                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
            x✝¹).fst.app
      x✝ =
    (({
                  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 := ⋯ }).app
            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
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✝
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                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
            x✝¹).snd.app
      x✝ =
    (({
                  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 := ⋯ }).app
            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
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₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x y : CatCommSqOver F G X
f : x ⟶ y
x✝ : X
⊢ (((transform X).obj (ψ.comp ψ')).map f ≫
            (mkIso (y.fst.associator ψ.left ψ'.left).symm (y.snd.associator ψ.right ψ'.right).symm ⋯).hom).fst.app
      x✝ =
    ((mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯).hom ≫
            ((transform X).obj ψ ⋙ (transform X).obj ψ').map f).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₁
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₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x y : CatCommSqOver F G X
f : x ⟶ y
x✝ : X
⊢ (((transform X).obj (ψ.comp ψ')).map f ≫
            (mkIso (y.fst.associator ψ.left ψ'.left).symm (y.snd.associator ψ.right ψ'.right).symm ⋯).hom).snd.app
      x✝ =
    ((mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯).hom ≫
            ((transform X).obj ψ ⋙ (transform X).obj ψ').map f).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
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₁
φ φ' : CatCospanTransform F₁ G₁ F₂ G₂
α : φ ⟶ φ'
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (ψ ◁ α)).app x✝¹).fst.app x✝ =
    (((transformObjComp X ψ φ).hom ≫
                ((transform X).obj ψ).whiskerLeft ((transform X).map α) ≫ (transformObjComp X ψ φ').inv).app
            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
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₁
φ φ' : CatCospanTransform F₁ G₁ F₂ G₂
α : φ ⟶ φ'
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (ψ ◁ α)).app x✝¹).snd.app x✝ =
    (((transformObjComp X ψ φ).hom ≫
                ((transform X).obj ψ).whiskerLeft ((transform X).map α) ≫ (transformObjComp X ψ φ').inv).app
            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
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₁
α : ψ ⟶ ψ'
φ : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (α ▷ φ)).app x✝¹).fst.app x✝ =
    (((transformObjComp X ψ φ).hom ≫
                whiskerRight ((transform X).map α) ((transform X).obj φ) ≫ (transformObjComp X ψ' φ).inv).app
            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
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₁
α : ψ ⟶ ψ'
φ : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (α ▷ φ)).app x✝¹).snd.app x✝ =
    (((transformObjComp X ψ φ).hom ≫
                whiskerRight ((transform X).map α) ((transform X).obj φ) ≫ (transformObjComp X ψ' φ).inv).app
            x✝¹).snd.app
      x✝

Tactic:
simp

Goal state after: