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

Goal state after:
case e₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₁ F G)).app
      x✝

case e₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x✝ : X
⊢ (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x✝ =
    (whiskerRight
          ({
                  preimage := fun {X_1 Y} f ↦
                    (functorEquiv F G X).unitIso.hom.app X_1 ≫
                      (functorEquiv F G X).inverse.map f ≫ (functorEquiv F G X).unitIso.inv.app Y,
                  map_preimage := ⋯, preimage_map := ⋯ }.preimageIso
              ((toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh))).hom
          (π₂ F G)).app
      x✝
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

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

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✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case tensor
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)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f✝ ⊗ₘ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝

Tactic:
hfg,

Goal state after:
case tensor
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)
W✝ X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hfg : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hfg' : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g✝ = projectMapAux f✝¹ f'✝ ⊗ₘ projectMapAux f✝¹ g'✝
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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✝