awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₁) (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₄) ⋯)
      ⋯)
have apply : IsColimit (F := span (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
  ((PushoutCocone.mk («W» := Y₂) (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) sorry).pasteVert (i₂ :=
    (PushoutCocone.mk («W» := Y₂) (pushout.inl g₃ g₄) (pushout.inr g₃ g₄) sorry).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₄) sorry)
      sorry)
    sorry)
Tactic: apply botSquareIsPushout _ rfl (pushoutIsPushout _ g₄)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄
⊢ 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₄) ⋯))
have 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₄) sorry))
Tactic: rw [Category.assoc, pushout.inl_desc, pushout.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄) ⋯))
⊢ 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₄) ⋯))
have 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₄)
Tactic: rw [Category.assoc, pushout.inl_desc, pushout.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄)
⊢ 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₄) ⋯))
have 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₄)
Tactic: rw [Category.assoc, pushout.inl_desc, pushout.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 (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₄)) ⋯)
have apply : IsColimit (F := span (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
  ((PushoutCocone.mk («W» := Y₁) (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) sorry).pasteHoriz (i₂ :=
    (PushoutCocone.mk («W» := Y₁) (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) sorry).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₄)) sorry)
      (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) sorry)
    sorry)
Tactic: apply rightSquareIsPushout _ rfl (pushoutIsPushout _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₂)
      (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₄))
have 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₄)) sorry))
Tactic: trans f₁ ≫ l₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄)) ⋯))
⊢ 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₄))
have 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₄)) sorry))
  (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
Tactic: trans f₁ ≫ l₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₂)
      (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₄)) ⋯))
have 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₄))
    sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₂)
      (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₄))
have 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₄)) sorry))
Tactic: trans f₂ ≫ l₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄)) ⋯))
⊢ 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₄))
have 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₄)) sorry))
  (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
Tactic: trans f₂ ≫ l₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₂)
      (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₄)) ⋯))
have 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₄))
    sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)
have trans : Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
  (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
  (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
    (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) sorry))
Tactic: trans f₄ ≫ l₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
⊢ Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)
have trans₁ : Eq (α := X₃ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
  (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
    (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) sorry))
  (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)
Tactic: trans f₄ ≫ l₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (CategoryStruct.comp (Y := Y₂) (pushout.inr g₃ g₄)
      (pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯))
have e_a : Eq (α := Y₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
  (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (Iso.inv (pushoutAssoc g₁ 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₄)
    sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw : Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄)
rw :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
⊢ Eq (α := X₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw₁ : Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl 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₄))))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄)
rw :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
rw₁ :
  Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl 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₄))))
⊢ Eq (α := X₁ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw₂ : Eq (α := X₁ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
Tactic: rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inl g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw : Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
  (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
  (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, inr_inl_pushoutAssoc_hom]