awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      snd (g ≫ f) f =
    CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (snd (g ≫ f) f)

Tactic:
simp [e, i]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w :
  autoParam
    (Eq (α := Y ⟶ diagonalObj f) (g ≫ diagonal f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)))
    CommSq.w._autoParam
⊢ CommSq (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w :
  CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (fst f f) =
    CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) (fst f f)
w₁ :
  CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (snd f f) =
    CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) (snd f f)
⊢ autoParam
    (Eq (α := Y ⟶ diagonalObj f) (g ≫ diagonal f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)))
    CommSq.w._autoParam

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (fst f f) =
    CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) (fst f f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (snd f f) =
    CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) (snd f f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst_2 : Mono i₃
⊢ Eq (α := pullback f g ⟶ pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂ : pullback f g ⟶ pullback f' g')
    (CategoryStruct.comp (Y :=
        pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
          pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂))
        (Iso.inv (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂) :
          pullback f g ⟶
            pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂))
        (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂ :
          pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂) ⟶
            pullback f' g') :
      pullback f g ⟶ pullback f' g')

Tactic:
simp only [pullbackFstFstIso_inv, lift_snd_assoc, lift_fst]

Premises used: CategoryTheory.Limits.pullback.lift_snd_assoc, CategoryTheory.Limits.pullback.lift_fst, CategoryTheory.Limits.pullbackFstFstIso_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst_2 : Mono i₃
rw :
  Eq (α := pullback f g ⟶ pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂)
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (snd f' g') i₂)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) (fst (snd f' g') i₂))
rw₁ rw₂ : Eq (α := pullback f g ⟶ pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f g f' g' i₁ i₂ i₃ e₁ e₂)
⊢ Eq (α := pullback f g ⟶ pullback f' g')
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (fst f' g') i₁)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (fst (fst f' g') i₁))
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (snd f' g') i₂)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) (fst (snd f' g') i₂))

Tactic:
rw [lift_fst, lift_fst]

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst_2 : Mono i₃
⊢ Eq (α := pullback f g ⟶ pullback (X := pullback f' g') (fst f' g') i₁)
    (CategoryStruct.comp (Y :=
        pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
          pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂))
        (Iso.hom (Iso.symm (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂)) :
          pullback f g ⟶
            pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂))
        (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) :
          pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂) ⟶
            pullback (X := pullback f' g') (fst f' g') i₁) :
      pullback f g ⟶ pullback (X := pullback f' g') (fst f' g') i₁)
    (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ : pullback f g ⟶ pullback (X := pullback f' g') (fst f' g') i₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst_2 : Mono i₃
⊢ Eq (α := pullback f g ⟶ pullback (X := pullback f' g') (snd f' g') i₂)
    (CategoryStruct.comp (Y :=
        pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
          pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂))
        (Iso.hom (Iso.symm (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂)) :
          pullback f g ⟶
            pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂))
        (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) :
          pullback (X := pullback (X := pullback f' g') (fst f' g') i₁) (Y :=
              pullback (X := pullback f' g') (snd f' g') i₂) (fst (fst f' g') i₁) (fst (snd f' g') i₂) ⟶
            pullback (X := pullback f' g') (snd f' g') i₂) :
      pullback f g ⟶ pullback (X := pullback f' g') (snd f' g') i₂)
    (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ : pullback f g ⟶ pullback (X := pullback f' g') (snd f' g') i₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ Eq (α := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h) ⟶ Y)
    (CategoryStruct.comp (Y := pullback g h) (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst g h))
    (fst (fst f g) (fst f h) ≫ snd f g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
refine_1 :
  (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)) →
    s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
refine_2 :
  ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) =
      s.fst
refine_3 :
  ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) =
      s.snd
refine_4 :
  ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g))
    (m : s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯
⊢ IsPullback (P := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)) (X := pullback g h)
    (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)

Tactic:
refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
refine_1 : (c.snd ≫ fst f g) ≫ f = (c.fst ≫ snd g h) ≫ h
refine_1₁ :
  c.snd ≫ fst f g = CategoryStruct.comp (Y := pullback f h) (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) (fst f h)
⊢ c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)

Tactic:
refine pullback.lift c.snd
        (pullback.lift (c.snd ≫ pullback.fst _ _) (c.fst ≫ pullback.snd _ _) ?_) ?_

Premises used: CategoryTheory.Limits.pullback.lift, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ (c.snd ≫ fst f g) ≫ f = (c.fst ≫ snd g h) ≫ h

Tactic:
simp [pullback.condition, ← c.condition_assoc]

Premises used: CategoryTheory.Limits.PullbackCone.condition_assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ c.snd ≫ fst f g = CategoryStruct.comp (Y := pullback f h) (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) (fst f h)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
refine_2 :
  CategoryStruct.comp (Y := pullback g h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯))
      (fst g h) =
    c.fst ≫ fst g h
refine_2₁ :
  CategoryStruct.comp (Y := pullback g h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯))
      (snd g h) =
    c.fst ≫ snd g h
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
      (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) =
    c.fst

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ CategoryStruct.comp (Y := pullback g h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯))
      (fst g h) =
    c.fst ≫ fst g h

Tactic:
simp [c.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ CategoryStruct.comp (Y := pullback g h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯))
      (snd g h) =
    c.fst ≫ snd g h

Tactic:
simp [c.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
refine_3 :
  CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) ≫
      fst f g =
    c.snd ≫ fst f g
refine_3₁ :
  CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) ≫
      snd f g =
    c.snd ≫ snd f g
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) =
    c.snd

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) ≫
      fst f g =
    c.snd ≫ fst f g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) ≫
      snd f g =
    c.snd ≫ snd f g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m ≫ fst (fst f g) (fst f h) =
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
refine_4 :
  m ≫ snd (fst f g) (fst f h) =
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h))
⊢ m = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯

Tactic:
refine pullback.hom_ext (by simpa) ?_

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
refine_4 :
  (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    CategoryStruct.comp (Y := pullback f h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h)))
      (fst f h)
refine_4₁ :
  (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
    CategoryStruct.comp (Y := pullback f h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h)))
      (snd f h)
⊢ m ≫ snd (fst f g) (fst f h) =
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    CategoryStruct.comp (Y := pullback f h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h)))
      (fst f h)

Tactic:
simp [← hsnd, pullback.condition, ← hfst]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
    CategoryStruct.comp (Y := pullback f h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (snd (fst f g) (fst f h)))
      (snd f h)

Tactic:
simp [← hsnd, pullback.condition, ← hfst]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ CategoryStruct.comp (Y := pushout f f) (inl f f) (codiagonal f) = 𝟙 Y

Tactic:
pushout.inl_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.codiagonal, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.pushout.inl_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPushout f f
⊢ CategoryStruct.comp (Y := pushout f f) (inr f f) (codiagonal f) = 𝟙 Y

Tactic:
pushout.inr_desc _ _ _

Premises used: CategoryTheory.Limits.pushout.inr_desc, CategoryTheory.Limits.pushout.codiagonal, CategoryTheory.Limits.colimit.desc