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 (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.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:
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₄ ⟶ 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₄)

Tactic:
pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_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₂)
⊢ 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₄)

Tactic:
exact pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_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₂)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
    (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₄))
rw₁ rw₂ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₂)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd 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.snd f₁ f₂))
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄)

Tactic:
rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_fst]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.pullbackAssoc_hom_snd_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₃) (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄)
    (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₄))
rw₁ rw₂ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ X₃) (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄)
    (pullback.snd (pullback.snd f₁ 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.snd (pullback.snd f₁ f₂ ≫ f₃) f₄))
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄)

Tactic:
rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.pullbackAssoc_hom_snd_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
apply :
  IsColimit (F := span (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    ((PushoutCocone.mk («W» := Y₂) (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) ⋯).pasteVert (i₂ :=
      (PushoutCocone.mk («W» := Y₂) (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) ⋯).inl)
      (PushoutCocone.mk («W» := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
          (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
        ⋯)
      ⋯)
⊢ IsColimit (F := span (Y := Y₁) (Z := Y₂) (pushout.inr g₁ g₂) (pushout.inl g₃ g₄))
    (PushoutCocone.mk («W» := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
      ⋯)

Tactic:
apply botSquareIsPushout _ rfl (pushoutIsPushout _ g₄)

Premises used: CategoryTheory.Limits.botSquareIsPushout, CategoryTheory.Limits.pushoutIsPushout, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ IsColimit (F := span (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    ((PushoutCocone.mk («W» := Y₂) (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) ⋯).pasteVert (i₂ :=
      (PushoutCocone.mk («W» := Y₂) (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) ⋯).inl)
      (PushoutCocone.mk («W» := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
          (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
        ⋯)
      ⋯)

Tactic:
simpa [PushoutCocone.pasteVert] using
    PushoutCocone.mkSelfIsColimit (pushoutIsPushout (g₃ ≫ f₂) g₄)

Premises used: CategoryTheory.Limits.PushoutCocone.pasteVert
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
rw :
  Eq (α := Z₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₁ ≫ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₂ ≫
      CategoryStruct.comp (Y := Y₂) (pushout.inl g₃ g₄)
        (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
          (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
rw₁ :
  Eq (α := Z₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₁ ≫ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₂ ≫ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
rw₂ rw₃ :
  Eq (α := Z₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₂ ≫ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₂ ≫ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
⊢ Eq (α := Z₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (g₁ ≫ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (g₂ ≫ pushout.inl g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))

Tactic:
rw [Category.assoc, pushout.inl_desc, pushout.condition_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.inl_desc, CategoryTheory.Limits.pushout.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ IsColimit (F := span (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (PushoutCocone.mk («W» := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯)
      ⋯)

Tactic:
simpa using pasteHorizIsPushout rfl (pushoutIsPushout g₁ g₂)
    (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄)

Premises used: CategoryTheory.Limits.pushoutPushoutLeftIsPushout, CategoryTheory.Limits.pasteHorizIsPushout, CategoryTheory.Limits.pushoutIsPushout, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
⟨⟨⟨_, pushoutAssocIsPushout g₁ g₂ g₃ g₄⟩⟩⟩

Premises used: CategoryTheory.Limits.pushoutAssocIsPushout, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
apply :
  IsColimit (F := span (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    ((PushoutCocone.mk («W» := Y₁) (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) ⋯).pasteHoriz (i₂ :=
      (PushoutCocone.mk («W» := Y₁) (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) ⋯).inr)
      (PushoutCocone.mk («W» := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
          (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      ⋯)
⊢ IsColimit (F := span (Y := Y₁) (Z := Y₂) (pushout.inr g₁ g₂) (pushout.inl g₃ g₄))
    (PushoutCocone.mk («W» := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)

Tactic:
apply rightSquareIsPushout _ rfl (pushoutIsPushout _ _)

Premises used: CategoryTheory.Limits.rightSquareIsPushout, CategoryTheory.Limits.pushoutIsPushout, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ IsColimit (F := span (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    ((PushoutCocone.mk («W» := Y₁) (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) ⋯).pasteHoriz (i₂ :=
      (PushoutCocone.mk («W» := Y₁) (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) ⋯).inr)
      (PushoutCocone.mk («W» := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
          (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      ⋯)

Tactic:
simpa [PushoutCocone.pasteHoriz] using PushoutCocone.mkSelfIsColimit (pushoutIsPushout _ _)

Premises used: CategoryTheory.Limits.PushoutCocone.pasteHoriz, CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.PushoutCocone.mkSelfIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
⟨⟨⟨_, pushoutAssocSymmIsPushout g₁ g₂ g₃ g₄⟩⟩⟩

Premises used: CategoryTheory.Limits.pushoutAssocSymmIsPushout, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
trans :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
trans₁ :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
    (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
⊢ Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))

Tactic:
trans f₁ ≫ l₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
e_a :
  Eq (α := Y₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
⊢ Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := Y₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)

Tactic:
(pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _
        WalkingCospan.left

Premises used: CategoryTheory.Limits.pushoutPushoutLeftIsPushout, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := Y₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)

Tactic:
exact
      (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _
        WalkingCospan.left

Premises used: CategoryTheory.Limits.pushoutPushoutLeftIsPushout, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
    (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))

Tactic:
pushout.inl_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inl g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
    (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))

Tactic:
exact pushout.inl_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
trans :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
trans₁ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
⊢ Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))

Tactic:
trans f₂ ≫ l₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
e_a :
  Eq (α := Y₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
⊢ Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))

Tactic:
pushout.inr_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inr_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))

Tactic:
exact pushout.inr_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inr_desc