awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ IsLimit (F := cospan (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
    ((PullbackCone.mk («W» := Z₁) (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ⋯).pasteVert (i₂ :=
      (PullbackCone.mk («W» := Z₁) (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ⋯).snd)
      (PullbackCone.mk («W» := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
          (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)
      ⋯)

Tactic:
simpa [PullbackCone.pasteVert] using PullbackCone.mkSelfIsLimit (pullbackIsPullback _ _)

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.PullbackCone.mkSelfIsLimit, CategoryTheory.Limits.PullbackCone.pasteVert
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ≫ f₃)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
rw₁ :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ ≫ f₃)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
rw₂ :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ ≫ f₃)
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ ≫ f₄)
rw₃ rw₄ :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ ≫ f₄)
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ ≫ f₄)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ f₂ ≫ f₃))
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)

Tactic:
rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd_assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ IsLimit (F := cospan (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
    (PullbackCone.mk («W» := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ⋯)

Tactic:
simpa [PullbackCone.pasteHoriz] using pasteHorizIsPullback rfl
    (pullbackIsPullback f₃ f₄) (pullbackPullbackRightIsPullback _ _ _ _)

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.pullbackPullbackRightIsPullback, CategoryTheory.Limits.pasteHorizIsPullback, CategoryTheory.Limits.PullbackCone.pasteHoriz, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄

Tactic:
⟨⟨⟨_, pullbackAssocSymmIsPullback f₁ f₂ f₃ f₄⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.pullbackAssocSymmIsPullback, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
trans :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂))
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))
trans₁ :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))
    (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂))
    (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))

Tactic:
trans l₁' ≫ pullback.fst _ _

Premises used: CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := Z₁)
      (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
        (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄))
      (pullback.fst f₁ f₂))
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂))
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
e_a :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Z₁)
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄))
    (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := Z₁)
      (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
        (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄))
      (pullback.fst f₁ f₂))
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Z₁)
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄))
    (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Z₁)
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄))
    (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)

Tactic:
exact IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))
    (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.fst f₁ f₂))
    (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))

Tactic:
exact pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁) (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
    (CategoryStruct.comp (Y := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄) (Iso.inv (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂))
rw₁ rw₂ :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ X₁) (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
    (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₁)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)))
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂)

Tactic:
rw [← Iso.eq_inv_comp, pullbackAssoc_inv_fst_fst]

Premises used: CategoryTheory.Iso.eq_inv_comp, CategoryTheory.Limits.pullbackAssoc_inv_fst_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
trans :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))
trans₁ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄))
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)

Tactic:
trans l₂ ≫ pullback.fst _ _

Premises used: CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := Z₂)
      (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)))
      (pullback.fst f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
e_a :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Z₂)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)))
    (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
      (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := Z₂)
      (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)))
      (pullback.fst f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Z₂)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)))
    (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
      (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Z₂)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)))
    (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
      (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)

Tactic:
exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄))
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)

Tactic:
exact pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
trans :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₃)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.snd f₃ f₄))
trans₁ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₃)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.snd f₃ f₄))
    (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₃)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄))
    (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄)

Tactic:
trans l₂ ≫ pullback.snd _ _

Premises used: CategoryTheory.Limits.pullback.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
inst_4 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₃)
    (CategoryStruct.comp (Y := Z₂)
      (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)))
      (pullback.snd f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.snd f₃ f₄))
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₃)
    (CategoryStruct.comp (Y := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)) (Iso.hom (pullbackAssoc f₁ f₂ f₃ f₄))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄))
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.snd f₃ f₄))

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc