mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
⊢ (toCatCommSqOver F G X).map
        ((NatIso.ofComponents
                (fun x ↦
                  NatIso.ofComponents
                    (fun x_1 ↦
                      mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                        (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                    ⋯)
                ⋯).hom.app
          X✝) ≫
      (NatIso.ofComponents
              (fun x ↦
                CatCommSqOver.mkIso
                  (NatIso.ofComponents
                    (fun x_1 ↦
                      Iso.refl
                        (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).fst.obj
                          x_1))
                    ⋯)
                  (NatIso.ofComponents
                    (fun x_1 ↦
                      Iso.refl
                        (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).snd.obj
                          x_1))
                    ⋯)
                  ⋯)
              ⋯).hom.app
        ((toCatCommSqOver F G X).obj X✝) =
    𝟙 ((toCatCommSqOver F G X).obj X✝)

Tactic:
ext <;> 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
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
⊢ (toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh) = CatCommSqOver.mkIso e₁ e₂ ⋯

Tactic:
ext <;> 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
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
⊢ mkNatIso e₁ e₂ coh =
    {
          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))

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

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
t : X ⟶ Y
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
⊢ motive t

Tactic:
by
  induction t using Quotient.inductionOn with | _ f
  induction f with
  | id X => exact id X
  | α_hom X Y Z => exact α_hom X Y Z
  | α_inv X Y Z => exact α_inv X Y Z
  | l_hom X => exact l_hom X
  | l_inv X => exact l_inv X
  | ρ_hom X => exact ρ_hom X
  | ρ_inv X => exact ρ_inv X
  | comp f g hf hg => exact comp _ _ hf hg
  | whiskerLeft X f hf => exact whiskerLeft X _ hf
  | whiskerRight f X hf => exact whiskerRight _ X hf
  | @tensor W X Y Z f g hf hg =>
      have : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
        Quotient.sound (HomEquiv.tensorHom_def f g)
      change motive (homMk f ⊗ₘ homMk g)
      rw [this]
      exact comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)

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

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

Tactic:
ext <;> 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
X✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ {
      app := fun S ↦
        { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
      naturality := ⋯ } =
    {
        app := fun S ↦
          { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } ≫
      {
        app := fun S ↦
          { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ }

Tactic:
ext <;> 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₁
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
⊢ ((transform X).obj (ψ.comp ψ')).map f ≫
      (mkIso (y.fst.associator ψ.left ψ'.left).symm (y.snd.associator ψ.right ψ'.right).symm ⋯).hom =
    (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯).hom ≫
      ((transform X).obj ψ ⋙ (transform X).obj ψ').map f

Tactic:
ext <;> 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₁
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₂
α : φ ⟶ φ'
⊢ (transform X).map (ψ ◁ α) =
    (transformObjComp X ψ φ).hom ≫
      ((transform X).obj ψ).whiskerLeft ((transform X).map α) ≫ (transformObjComp X ψ φ').inv

Tactic:
ext <;> 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₁
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₂
⊢ (transform X).map (α ▷ φ) =
    (transformObjComp X ψ φ).hom ≫
      whiskerRight ((transform X).map α) ((transform X).obj φ) ≫ (transformObjComp X ψ' φ).inv

Tactic:
ext <;> 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₁
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₃
⊢ (transform X).map (α_ ψ φ τ).hom =
    (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

Tactic:
ext <;> 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₁
⊢ (transform X).map (λ_ ψ).hom =
    (transformObjComp X (CatCospanTransform.id F G) ψ).hom ≫
      whiskerRight (transformObjId X F G).hom ((transform X).obj ψ) ≫ ((transform X).obj ψ).leftUnitor.hom

Tactic:
ext <;> 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₁
⊢ (transform X).map (ρ_ ψ).hom =
    (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)).hom ≫
      ((transform X).obj ψ).whiskerLeft (transformObjId X F₁ G₁).hom ≫ ((transform X).obj ψ).rightUnitor.hom

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

Tactic:
ext <;> 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
X✝ Y✝ Z✝ : CatCommSqOver F G Y
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := U.whiskerLeft (f✝ ≫ g✝).fst, snd := U.whiskerLeft (f✝ ≫ g✝).snd, w := ⋯ } =
    { fst := U.whiskerLeft f✝.fst, snd := U.whiskerLeft f✝.snd, w := ⋯ } ≫
      { fst := U.whiskerLeft g✝.fst, snd := U.whiskerLeft g✝.snd, w := ⋯ }

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

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

Tactic:
ext <;> 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₄
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
⊢ (precompose F G).map (U.whiskerLeft α) =
    (precomposeObjComp F G U V).hom ≫
      whiskerRight ((precompose F G).map α) ((precompose F G).obj U) ≫ (precomposeObjComp F G U W).inv

Tactic:
ext <;> 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₄
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
⊢ (precompose F G).map (whiskerRight α W) =
    (precomposeObjComp F G U W).hom ≫
      ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv

Tactic:
ext <;> 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)
⊢ Functor.whiskerRight (pushforwardComp f g).hom (pullback (f ≫ g)) ≫ (pullbackPushforwardAdj (f ≫ g)).counit =
    (pullbackPushforwardAdj (f ≫ g)).counit

Tactic:
by
  rw [pushforwardComp, Adjunction.rightAdjointUniq_hom_counit]

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₄
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
⊢ (precompose F G).map (U.associator V W).hom =
    (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

Tactic:
ext <;> 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₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
⊢ (precompose F G).map U.leftUnitor.hom =
    (precomposeObjComp F G (𝟭 X) U).hom ≫
      ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫ ((precompose F G).obj U).rightUnitor.hom

Tactic:
ext <;> 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₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
⊢ (precompose F G).map U.rightUnitor.hom =
    (precomposeObjComp F G U (𝟭 Y)).hom ≫
      whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫ ((precompose F G).obj U).leftUnitor.hom

Tactic:
ext <;> 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₇
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
⊢ ((precompose F G).obj U ⋙ (transform X).obj ψ).map f ≫
      (mkIso (U.associator y.fst ψ.left) (U.associator y.snd ψ.right) ⋯).hom =
    (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯).hom ≫
      ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f

Tactic:
ext <;> 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₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U V : X ⥤ Y
α : U ⟶ V
⊢ 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 =
    (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 α)

Tactic:
ext <;> 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₁
ψ : CatCospanTransform F G F₁ G₁
X : Type u₇
inst✝ : Category.{v₇, u₇} 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 =
    whiskerRight (precomposeObjId F G X).hom ((transform X).obj ψ) ≫
      ((transform X).obj ψ).leftUnitor.hom ≫ ((transform X).obj ψ).rightUnitor.inv

Tactic:
ext <;> simp

Goal state after: