mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
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₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (α_ ψ φ τ).hom).app x✝¹).fst.app x✝ =
    (((transformObjComp X (ψ.comp φ) τ).hom ≫
                whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
                  (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
                    ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫
                      (transformObjComp X ψ (φ.comp τ)).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₂
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₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (α_ ψ φ τ).hom).app x✝¹).snd.app x✝ =
    (((transformObjComp X (ψ.comp φ) τ).hom ≫
                whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
                  (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
                    ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫
                      (transformObjComp X ψ (φ.comp τ)).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₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (λ_ ψ).hom).app x✝¹).fst.app x✝ =
    (((transformObjComp X (CatCospanTransform.id F G) ψ).hom ≫
                whiskerRight (transformObjId X F G).hom ((transform X).obj ψ) ≫
                  ((transform X).obj ψ).leftUnitor.hom).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
ψ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (λ_ ψ).hom).app x✝¹).snd.app x✝ =
    (((transformObjComp X (CatCospanTransform.id F G) ψ).hom ≫
                whiskerRight (transformObjId X F G).hom ((transform X).obj ψ) ≫
                  ((transform X).obj ψ).leftUnitor.hom).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₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (ρ_ ψ).hom).app x✝¹).fst.app x✝ =
    (((transformObjComp X ψ (CatCospanTransform.id F₁ G₁)).hom ≫
                ((transform X).obj ψ).whiskerLeft (transformObjId X F₁ G₁).hom ≫
                  ((transform X).obj ψ).rightUnitor.hom).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
ψ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (ρ_ ψ).hom).app x✝¹).snd.app x✝ =
    (((transformObjComp X ψ (CatCospanTransform.id F₁ G₁)).hom ≫
                ((transform X).obj ψ).whiskerLeft (transformObjId X F₁ G₁).hom ≫
                  ((transform X).obj ψ).rightUnitor.hom).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
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
x✝ : X
⊢ { fst := U.whiskerLeft (𝟙 X✝).fst, snd := U.whiskerLeft (𝟙 X✝).snd, w := ⋯ }.fst.app x✝ =
    (𝟙
            { fst := U ⋙ X✝.fst, snd := U ⋙ X✝.snd,
              iso := U.associator X✝.fst F ≪≫ U.isoWhiskerLeft X✝.iso ≪≫ (U.associator X✝.snd 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₄
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
x✝ : X
⊢ { fst := U.whiskerLeft (𝟙 X✝).fst, snd := U.whiskerLeft (𝟙 X✝).snd, w := ⋯ }.snd.app x✝ =
    (𝟙
            { fst := U ⋙ X✝.fst, snd := U ⋙ X✝.snd,
              iso := U.associator X✝.fst F ≪≫ U.isoWhiskerLeft X✝.iso ≪≫ (U.associator X✝.snd 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₄
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✝
x✝ : X
⊢ { fst := U.whiskerLeft (f✝ ≫ g✝).fst, snd := U.whiskerLeft (f✝ ≫ g✝).snd, w := ⋯ }.fst.app x✝ =
    ({ fst := U.whiskerLeft f✝.fst, snd := U.whiskerLeft f✝.snd, w := ⋯ } ≫
            { fst := U.whiskerLeft g✝.fst, snd := U.whiskerLeft g✝.snd, 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₄
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✝
x✝ : X
⊢ { fst := U.whiskerLeft (f✝ ≫ g✝).fst, snd := U.whiskerLeft (f✝ ≫ g✝).snd, w := ⋯ }.snd.app x✝ =
    ({ fst := U.whiskerLeft f✝.fst, snd := U.whiskerLeft f✝.snd, w := ⋯ } ≫
            { fst := U.whiskerLeft g✝.fst, snd := U.whiskerLeft g✝.snd, 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    ((𝟙
                {
                  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 := ⋯ }).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
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
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    ((𝟙
                {
                  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 := ⋯ }).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
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✝
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (f✝ ≫ g✝) x.fst, snd := whiskerRight (f✝ ≫ g✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    (({ 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 := ⋯ }).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
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✝
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (f✝ ≫ g✝) x.fst, snd := whiskerRight (f✝ ≫ g✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    (({ 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 := ⋯ }).app
            x✝¹).snd.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).unit ≫ (pullback (𝟙 I)).whiskerLeft (pushforwardId I).hom =
    (pullbackPushforwardAdj (𝟙 I)).unit

Tactic:
pushforwardId,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).unit ≫
      (pullback (𝟙 I)).whiskerLeft
        ((pullbackPushforwardAdj (𝟙 I)).rightAdjointUniq (pullbackPushforwardAdj (𝟙 I))).hom =
    (pullbackPushforwardAdj (𝟙 I)).unit
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ Functor.whiskerRight (pushforwardId I).hom (pullback (𝟙 I)) ≫ (pullbackPushforwardAdj (𝟙 I)).counit =
    (pullbackPushforwardAdj (𝟙 I)).counit

Tactic:
pushforwardId,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ Functor.whiskerRight ((pullbackPushforwardAdj (𝟙 I)).rightAdjointUniq (pullbackPushforwardAdj (𝟙 I))).hom
        (pullback (𝟙 I)) ≫
      (pullbackPushforwardAdj (𝟙 I)).counit =
    (pullbackPushforwardAdj (𝟙 I)).counit
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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
V W : Y ⥤ Z
α : V ⟶ W
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (U.whiskerLeft α)).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U V).hom ≫
                whiskerRight ((precompose F G).map α) ((precompose F G).obj U) ≫ (precomposeObjComp F G U W).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
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
V W : Y ⥤ Z
α : V ⟶ W
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (U.whiskerLeft α)).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U V).hom ≫
                whiskerRight ((precompose F G).map α) ((precompose F G).obj U) ≫ (precomposeObjComp F G U W).inv).app
            x✝¹).snd.app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).unit ≫ (pullback (f ≫ g)).whiskerLeft (pushforwardComp f g).hom =
    (pullbackPushforwardAdj (f ≫ g)).unit

Tactic:
rw [pushforwardComp, Adjunction.unit_rightAdjointUniq_hom]

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (whiskerRight α W)).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U W).hom ≫
                ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).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
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 V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((precompose F G).map (whiskerRight α W)).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U W).hom ≫
                ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
x✝¹ : CatCommSqOver F G T
x✝ : X
⊢ (((precompose F G).map (U.associator V W).hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
x✝¹ : CatCommSqOver F G T
x✝ : X
⊢ (((precompose F G).map (U.associator V W).hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).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
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.leftUnitor.hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G (𝟭 X) U).hom ≫
                ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫
                  ((precompose F G).obj U).rightUnitor.hom).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
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.leftUnitor.hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G (𝟭 X) U).hom ≫
                ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫
                  ((precompose F G).obj U).rightUnitor.hom).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
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.rightUnitor.hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫
                  ((precompose F G).obj U).leftUnitor.hom).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
X : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((precompose F G).map U.rightUnitor.hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫
                  ((precompose F G).obj U).leftUnitor.hom).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₁
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
x y : CatCommSqOver F G Y
f : x ⟶ y
x✝ : X
⊢ (((precompose F G).obj U ⋙ (transform X).obj ψ).map f ≫
            (mkIso (U.associator y.fst ψ.left) (U.associator y.snd ψ.right) ⋯).hom).fst.app
      x✝ =
    ((mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯).hom ≫
            ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f).fst.app
      x✝

Tactic:
simp

Goal state after: