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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 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
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
                    ((transform X).obj (CatCospanTransform.id F G))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
                ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.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
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
                    ((transform X).obj (CatCospanTransform.id F G))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
                ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.inv).app
            x✝¹).snd.app
      x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ Hom.left
      (homMk
        ((β_ A I).hom ≫
          uncurry
            (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫
              ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)))
        ⋯) =
    Hom.left u

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₁₀
Y : Type u₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
                    ((transform X).obj (ψ.comp ψ'))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
                (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
                  ((transform Y).obj ψ).whiskerLeft
                      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                          ((transform X).obj ψ')).hom ≫
                    (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                              ((transform X).obj ψ)).hom
                          ((transform X).obj ψ') ≫
                        (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).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₁
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
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
                    ((transform X).obj (ψ.comp ψ'))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
                (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
                  ((transform Y).obj ψ).whiskerLeft
                      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                          ((transform X).obj ψ')).hom ≫
                    (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                              ((transform X).obj ψ)).hom
                          ((transform X).obj ψ') ≫
                        (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom).app
            x✝¹).snd.app
      x✝

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom) =
    (ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g) ≫
      ChosenPullbacksAlong.snd ((ihom I).map X.hom) (curry (ρ_ I).hom)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ lift (Over.Hom.left u) (Over.Hom.left v) ⋯ ≫ (binaryFan Y Z).pt.hom = T✝.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
x y : D
f : x ⟶ y
⊢ 𝟙_ C ⊴ₗ f = (𝟙_ C ⊴ₗ f ≫ (λₗ y).hom) ≫ (λₗ y).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ 𝟙 (x ⊗ y) ⊙ₗₘ f = (((𝟙 x ⊗ₘ 𝟙 y) ⊙ₗₘ f) ≫ (αₗ x y z').hom) ≫ (αₗ x y z').inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalLeftAction C D
x : C
y z : D
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ₗ f ≫ x ⊴ₗ inv f = 𝟙 (x ⊙ₗ y) ∧ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (x ⊙ₗ z)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalLeftAction C D
x y : C
f : x ⟶ y
inst✝ : IsIso f
z : D
⊢ f ⊵ₗ z ≫ inv f ⊵ₗ z = 𝟙 (x ⊙ₗ z) ∧ inv f ⊵ₗ z ≫ f ⊵ₗ z = 𝟙 (y ⊙ₗ z)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
c₁ c₂ c₃ : C
⊢ { app := fun x ↦ (αᵣ x c₁ c₂).inv, naturality := ⋯ } ▷ (curriedAction C D).obj c₃ ≫
      { app := fun x ↦ (αᵣ x (c₁ ⊗ c₂) c₃).inv, naturality := ⋯ } ≫ (curriedAction C D).map (α_ c₁ c₂ c₃).hom =
    (α_ ((curriedAction C D).obj c₁) ((curriedAction C D).obj c₂) ((curriedAction C D).obj c₃)).hom ≫
      (curriedAction C D).obj c₁ ◁ { app := fun x ↦ (αᵣ x c₂ c₃).inv, naturality := ⋯ } ≫
        { app := fun x ↦ (αᵣ x c₁ (c₂ ⊗ c₃)).inv, naturality := ⋯ }

Tactic:
ext d
    simpa [-actionHom_associator] using
      (IsIso.inv_eq_inv.mpr <| actionHom_associator c₁ c₂ c₃ d).symm =≫
        d ⊴ᵣ (α_ c₁ c₂ c₃).hom

Goal state after: