awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
refine_2 :
  CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
          (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
        (prod.lift s.fst (s.snd ≫ prod.snd))
        (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)))
      prod.fst =
    s.snd ≫ prod.fst
refine_2₁ :
  CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
          (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
        (prod.lift s.fst (s.snd ≫ prod.snd))
        (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)))
      prod.snd =
    s.snd ≫ prod.snd
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.snd

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
⊢ CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
          (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
        (prod.lift s.fst (s.snd ≫ prod.snd))
        (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)))
      prod.fst =
    s.snd ≫ prod.fst

Tactic:
simp [PullbackCone.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
⊢ CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
          (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
        (prod.lift s.fst (s.snd ≫ prod.snd))
        (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)))
      prod.snd =
    s.snd ≫ prod.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
m :
  s.pt ⟶
    Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
      (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)
h₁ : m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst
h₂ : m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.snd
refine_3 : m = prod.lift s.fst (s.snd ≫ prod.snd)
⊢ m = prod.lift s.fst (s.snd ≫ prod.snd)

Tactic:
dsimp at m h₁ h₂ ⊢
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
m : s.pt ⟶ Limits.prod.{v₁, u₁} A X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
refine_3 :
  m ≫ prod.fst = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.fst
refine_3₁ :
  m ≫ prod.snd = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.snd
⊢ m = prod.lift s.fst (s.snd ≫ prod.snd)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
m : s.pt ⟶ Limits.prod.{v₁, u₁} A X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.fst = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.fst

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
m : s.pt ⟶ Limits.prod.{v₁, u₁} A X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.snd = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.snd

Tactic:
simp [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryFan.{v₁, u₁} X Y
hc : IsLimit c
T : C
hT : IsTerminal.{v₁, u₁} T
⊢ ∀
    (s :
      PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
        Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
        (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
        (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))),
    (fun
              (s :
                PullbackCone (X :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
                  (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
                  (hT.from
                    (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
            BinaryFan.IsLimit.lift hc s.fst s.snd)
          s ≫
        c.fst =
      s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryFan.{v₁, u₁} X Y
hc : IsLimit c
T : C
hT : IsTerminal.{v₁, u₁} T
⊢ ∀
    (s :
      PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
        Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
        (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
        (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))),
    (fun
              (s :
                PullbackCone (X :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
                  Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
                  (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
                  (hT.from
                    (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
            BinaryFan.IsLimit.lift hc s.fst s.snd)
          s ≫
        c.snd =
      s.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryFan.{v₁, u₁} X Y
hc : IsLimit c
T : C
hT : IsTerminal.{v₁, u₁} T
s :
  PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
m :
  s.pt ⟶
    Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
h₃ :
  m ≫ c.fst =
    (fun
            (s :
              PullbackCone (X :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
                (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
                (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
          BinaryFan.IsLimit.lift hc s.fst s.snd)
        s ≫
      c.fst
h₄ :
  m ≫ c.snd =
    (fun
            (s :
              PullbackCone (X :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
                (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
                (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
          BinaryFan.IsLimit.lift hc s.fst s.snd)
        s ≫
      c.snd
⊢ m =
    (fun
          (s :
            PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
        BinaryFan.IsLimit.lift hc s.fst s.snd)
      s

Tactic:
apply BinaryFan.IsLimit.hom_ext hc

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
w : fst ≫ f = snd ≫ g
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄, φ ≫ fst = φ' ≫ fst → φ ≫ snd = φ' ≫ snd → φ = φ'
exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y), a ≫ f = b ≫ g → ∃ (l : T ⟶ P), l ≫ fst = a ∧ l ≫ snd = b
l : ∀ (s : PullbackCone f g), ∃ (l : s.pt ⟶ P), l ≫ fst = s.fst ∧ l ≫ snd = s.snd := ⋯
⊢ Nonempty (IsLimit (PullbackCone.mk fst snd w))

Tactic:
⟨PullbackCone.IsLimit.mk _
      (fun s ↦ (l s).choose)
      (fun s ↦ (l s).choose_spec.1)
      (fun s ↦ (l s).choose_spec.2)
      (fun s m h₁ h₂ ↦ hom_ext
        (h₁.trans (l s).choose_spec.1.symm)
        (h₂.trans (l s).choose_spec.2.symm))⟩

Premises used: Exists.choose_spec, CategoryTheory.Limits.PullbackCone.IsLimit.mk, Nonempty.intro, And.right, And.left, Exists.choose, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
w : fst ≫ f = snd ≫ g
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄, φ ≫ fst = φ' ≫ fst → φ ≫ snd = φ' ≫ snd → φ = φ'
exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y), a ≫ f = b ≫ g → ∃ (l : T ⟶ P), l ≫ fst = a ∧ l ≫ snd = b
l : ∀ (s : PullbackCone f g), ∃ (l : s.pt ⟶ P), l ≫ fst = s.fst ∧ l ≫ snd = s.snd := ⋯
⊢ Nonempty (IsLimit (PullbackCone.mk fst snd w))

Tactic:
exact ⟨PullbackCone.IsLimit.mk _
      (fun s ↦ (l s).choose)
      (fun s ↦ (l s).choose_spec.1)
      (fun s ↦ (l s).choose_spec.2)
      (fun s m h₁ h₂ ↦ hom_ext
        (h₁.trans (l s).choose_spec.1.symm)
        (h₂.trans (l s).choose_spec.2.symm))⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback t sndsndfgr sndfi rZ

Tactic:
.of_right ?_ ht₂ hfi

Premises used: CategoryTheory.IsPullback.of_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
refine : IsPullback (t ≫ fstfi) sndsndfgr f (rZ ≫ i)
⊢ IsPullback t sndsndfgr sndfi rZ

Tactic:
refine .of_right ?_ ht₂ hfi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
rw : IsPullback (fstsndfgr ≫ fstfg) sndsndfgr f (rY ≫ g)
⊢ IsPullback (t ≫ fstfi) sndsndfgr f (rZ ≫ i)

Tactic:
rw [← hrw, ht₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback (fstsndfgr ≫ fstfg) sndsndfgr f (rY ≫ g)

Tactic:
.paste_horiz hsndfgr hfg

Premises used: CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback (fstsndfgr ≫ fstfg) sndsndfgr f (rY ≫ g)

Tactic:
exact .paste_horiz hsndfgr hfg
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X_1 Y_1 Z_1 : C
fst : P ⟶ X_1
snd : P ⟶ Y_1
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst_1 : HasPullback i g
h : U ⟶ pullback i g
inst_2 : HasPullback f g
inst_3 : HasPullback (X := pullback f g) (pullback.snd f g) (h ≫ pullback.snd i g)
inst_4 : HasPullback f i
⊢ (h ≫ pullback.snd i g) ≫ g = (h ≫ pullback.fst i g) ≫ i

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst_1 : HasPullback i g
h : U ⟶ pullback i g
inst_2 : HasPullback f g
inst_3 : HasPullback (X := pullback f g) (pullback.snd f g) (h ≫ pullback.snd i g)
inst_4 : HasPullback f i
⊢ (h ≫ pullback.snd i g) ≫ g = (h ≫ pullback.fst i g) ≫ i

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst_1 : HasPullback i g
h : U ⟶ pullback i g
inst_2 : HasPullback f g
inst_3 : HasPullback (X := pullback f g) (pullback.snd f g) (h ≫ pullback.snd i g)
inst_4 : HasPullback f i
⊢ Eq (α := pullback (X := pullback f g) (pullback.snd f g) (h ≫ pullback.snd i g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f i)
      (pullback.map (pullback.snd f g) (h ≫ pullback.snd i g) f i (pullback.fst f g) (h ≫ pullback.fst i g) g ⋯ ⋯)
      (pullback.fst f i))
    (pullback.fst (pullback.snd f g) (h ≫ pullback.snd i g) ≫ pullback.fst f g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z U S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
inst_1 : HasPullback i g
h : U ⟶ pullback i g
inst_2 : HasPullback f g
inst_3 : HasPullback (X := pullback f g) (pullback.snd f g) (h ≫ pullback.snd i g)
inst_4 : HasPullback f i
⊢ Eq (α := pullback (X := pullback f g) (pullback.snd f g) (h ≫ pullback.snd i g) ⟶ Z)
    (CategoryStruct.comp (Y := pullback f i)
      (pullback.map (pullback.snd f g) (h ≫ pullback.snd i g) f i (pullback.fst f g) (h ≫ pullback.fst i g) g ⋯ ⋯)
      (pullback.snd f i))
    (pullback.snd (pullback.snd f g) (h ≫ pullback.snd i g) ≫ h ≫ pullback.fst i g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan.{v₁, u₁} X Y
h : IsColimit c
t : IsInitial.{v₁, u₁} Z
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v₁, 0, u₁} (F := pair X Y)
        (BinaryCofan.mk (P := c.1) (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })))
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    (NatTrans.app
      (Cocone.ι (BinaryCofan.mk (P := c.1) (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })))
      { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan.{v₁, u₁} X Y
h : IsColimit c
t : IsInitial.{v₁, u₁} Z
⊢ Eq (α :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v₁, 0, u₁} (F := pair X Y)
        (BinaryCofan.mk (P := c.1) (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })))
    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    (NatTrans.app
      (Cocone.ι (BinaryCofan.mk (P := c.1) (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })))
      { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
inl : X ⟶ P
inr : Y ⟶ P
h : IsColimit (BinaryCofan.mk inl inr)
t : IsInitial.{v₁, u₁} Z
⊢ IsPushout (t.to X) (t.to Y) inl inr

Tactic:
of_is_coproduct h t

Premises used: CategoryTheory.IsPushout.of_is_coproduct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} X Y
inst_2 : HasInitial.{v₁, u₁} C
⊢ IsPushout.{v₁, u₁} (Z := initial.{v₁, u₁} C) (P := coprod.{v₁, u₁} X Y) (initial.to X) (initial.to Y) coprod.inl
    coprod.inr

Tactic:
of_is_coproduct (colimit.isColimit _) initialIsInitial

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.colimit.desc, CategoryTheory.IsPushout.of_is_coproduct, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : CommSq f g inl inr
inst_1 : HasPushout f g
i : P ≅ pushout f g
w₁ : inl ≫ i.hom = pushout.inl f g
w₂ : inr ≫ i.hom = pushout.inr f g
⊢ IsPushout f g inl inr

Tactic:
of_isColimit' h
    (Limits.IsColimit.ofIsoColimit (colimit.isColimit _)
      (PushoutCocone.ext (s := PushoutCocone.mk ..) i w₁ w₂).symm)

Premises used: CategoryTheory.IsPushout.of_isColimit', CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.PushoutCocone.ext, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₁ : f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₂ : f ≫ inl ≫ e₄.hom = e₁.hom ≫ g' ≫ inr'
rw₃ : f ≫ inl ≫ e₄.hom = g ≫ e₃.hom ≫ inr'
rw₄ : f ≫ inl ≫ e₄.hom = g ≫ inr ≫ e₄.hom
rw₅ rw₆ : g ≫ inr ≫ e₄.hom = g ≫ inr ≫ e₄.hom
⊢ f' ≫ inl' = g' ≫ inr'

Tactic:
rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
commf₁ : f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'
commg₁ : g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'
comminl₁ : inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'
comminr₁ : inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'
⊢ IsPushout f' g' inl' inr'

Tactic:
apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm

Premises used: CategoryTheory.IsPushout.of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commf, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc