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₃ 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₄)
⊢ 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₄)
have 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₄)
Tactic: rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 := 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₂))
have 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₄) sorry)
    (pullback.fst f₁ f₂))
Tactic: trans l₁' ≫ pullback.fst _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₂))
⊢ 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₂))
have 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₄) sorry)
    (pullback.fst f₁ f₂))
  (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
Tactic: trans l₁' ≫ pullback.fst _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 := 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₂))
have 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₄) sorry)
    (pullback.fst f₁ f₂))
Tactic: rw [← Category.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₃ 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₁)
      (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₂))
have 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₄) 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₃ 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 := 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₂)
have 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₂))
Tactic: rw [← Iso.eq_inv_comp, pullbackAssoc_inv_fst_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₂))
⊢ 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₂)
have 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₂))
Tactic: rw [← Iso.eq_inv_comp, pullbackAssoc_inv_fst_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 := 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₂)
have 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₄) sorry)
    (pullback.fst f₃ f₄))
Tactic: trans l₂ ≫ pullback.fst _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄))
⊢ 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₂)
have 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₄) sorry)
    (pullback.fst f₃ f₄))
  (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
Tactic: trans l₂ ≫ pullback.fst _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 := 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₄))
have 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₄) sorry)
    (pullback.fst f₃ f₄))
Tactic: rw [← Category.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₃ 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₂)
      (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₄))
have 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₄) 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₃ 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 := 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₄)
have 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₄) sorry)
    (pullback.snd f₃ f₄))
Tactic: trans l₂ ≫ pullback.snd _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄))
⊢ 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₄)
have 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₄) sorry)
    (pullback.snd f₃ f₄))
  (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄)
Tactic: trans l₂ ≫ pullback.snd _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 := 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₄))
have 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₄) sorry)
    (pullback.snd f₃ f₄))
Tactic: rw [← Category.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₃ 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₂)
      (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₄))
have 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₄) 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₃ 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 := 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₄)
have 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₄))
Tactic: rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄))
⊢ 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₄)
have 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₂)
Tactic: rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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 := 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₄)
have 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₄))
Tactic: rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
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₄))
⊢ 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₄)
have 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₄)
Tactic: rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]