awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
rw :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (snd f f))
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
have rw₁ : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    CategoryStruct.comp (Y := diagonalObj f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry)
      (snd f f))
Tactic: rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
rw :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (snd f f))
rw₁ :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) (snd f f))
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
have rw₂ : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
    snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i)
Tactic: rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      pullback f i)
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁)
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂)
have h₀ : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    X)
  (((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁) ≫
    fst f i)
  (((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂) ≫
    fst f i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
h₀ :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      X)
    (((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₁) ≫
      fst f i)
    (((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₂) ≫
      fst f i)
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      pullback f i)
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁)
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂)
have h₁ : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    U)
  (((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁) ≫
    snd f i)
  (((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂) ≫
    snd f i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ diagonalObj f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
have h₀ : Eq (α := pullback i₁ i₂ ⟶ X)
  (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (fst f f))
  (CategoryStruct.comp (Y := pullback f f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) sorry sorry)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
    (fst f f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
h₀ :
  Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (fst f f))
    (CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
        (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
      (fst f f))
⊢ Eq (α := pullback i₁ i₂ ⟶ diagonalObj f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
have h₁ : Eq (α := pullback i₁ i₂ ⟶ X)
  (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (snd f f))
  (CategoryStruct.comp (Y := pullback f f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) sorry sorry)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
    (snd f f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      V₁)
    (CategoryStruct.comp (Y := pullback i₁ i₂)
        (Iso.hom (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            pullback i₁ i₂)
        (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₁)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₁)
have delta : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    V₁)
  (CategoryStruct.comp (Y := pullback i₁ i₂)
      (Iso.hom { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := sorry, inv_hom_id := sorry } :
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
          pullback i₁ i₂)
      (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁) :
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
      V₁)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
      V₁)
Tactic: delta pullbackDiagonalMapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      V₂)
    (CategoryStruct.comp (Y := pullback i₁ i₂)
        (Iso.hom (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            pullback i₁ i₂)
        (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)
have delta : Eq (α :=
  pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
    V₂)
  (CategoryStruct.comp (Y := pullback i₁ i₂)
      (Iso.hom { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := sorry, inv_hom_id := sorry } :
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
          pullback i₁ i₂)
      (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂) :
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
      V₂)
  (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
      V₂)
Tactic: delta pullbackDiagonalMapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            X) :
      pullback i₁ i₂ ⟶ X)
    (fst i₁ i₂ ≫ i₁ ≫ fst f i : pullback i₁ i₂ ⟶ X)
have delta : Eq (α := pullback i₁ i₂ ⟶ X)
  (CategoryStruct.comp (Y :=
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
      (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := sorry, inv_hom_id := sorry } :
        pullback i₁ i₂ ⟶
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
      (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) :
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
          X) :
    pullback i₁ i₂ ⟶ X)
  (fst i₁ i₂ ≫ i₁ ≫ fst f i : pullback i₁ i₂ ⟶ X)
Tactic: delta pullbackDiagonalMapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ V₁)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₁) :
      pullback i₁ i₂ ⟶ V₁)
    (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁)
have delta : Eq (α := pullback i₁ i₂ ⟶ V₁)
  (CategoryStruct.comp (Y :=
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
      (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := sorry, inv_hom_id := sorry } :
        pullback i₁ i₂ ⟶
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
      (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
          V₁) :
    pullback i₁ i₂ ⟶ V₁)
  (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁)
Tactic: delta pullbackDiagonalMapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ V₂)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₂) :
      pullback i₁ i₂ ⟶ V₂)
    (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂)
have delta : Eq (α := pullback i₁ i₂ ⟶ V₂)
  (CategoryStruct.comp (Y :=
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
      (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := sorry, inv_hom_id := sorry } :
        pullback i₁ i₂ ⟶
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
      (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
            (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry) ⟶
          V₂) :
    pullback i₁ i₂ ⟶ V₂)
  (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂)
Tactic: delta pullbackDiagonalMapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ diagonalObj f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
have h₀ : Eq (α := pullback i₁ i₂ ⟶ X)
  (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (fst f f))
  (CategoryStruct.comp (Y := pullback f f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) sorry sorry)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
    (fst f f))
Tactic: ext